论文部分内容阅读
一个集合上的数学关系可以简化一个代数系统.所以它是形式化方法中的一个重要概念.HOL系统是基于传统高阶逻辑的交互式定理证明环境.在HOL中可以方便的对一个系统及系统的性质进行描述,但是证明结果的正确性需要用户参与.本文给出了等价性概念在高阶逻辑系统中的表示,并进一步探讨了有关well-founded关系的一些属性.