什么是证明等式的计算机辅助教学系统介绍

《证明等式的计算机辅助教学系统》是依托清华大学，由李大法担任项目负责人的面上项目。

项目摘要

本课题是证明等式的计算机辅助教学系统。它涉及的内容是怎样的在计算机上证明等式，怎样用于教学，理论上我们得到如下结果：

①我们提出01-paramodulation。给等式t=s和r=h，对项t和t的自变量位置上的项做等式替换，对更深入子项不做替换，我们证明了它是完备的，

②证明等式需要反身性、对称性和递性作为公理。使用我们的定理证明器发现用两个公理可代替上述三公理，

③虽然禁止Paramodulation into variables是完备的，我们指出这对Input paramodulation是不完备的，当变量在一个等式中只出现一次时，我们证明在input paramodulation中禁止Paramodulation into variasles是完备的。我们做了三个软件系统，

①受限制的Input paramodulation

②受限制Unitparamodulation

③01-paramodulation。打算将上述系统用于网络教学。