证明等式的计算机辅助教学系统

本课题是证明等式的计算机辅助教学系统。它涉及的内容是怎样的在计算机上证明等式，怎样用于教学，理论上我们得到如下结果：①我们提出01-paramodulation。给等式t=s和r=h，对项t和t的自变量位置上的项做等式替换，对更深入子项不做替换，我们证明了它是完备的，②证明等式需要反身性、对称性和递性作为公理。使用我们的定理证明器发现用两个公理可代替上述三公理，③虽然禁止Paramodulation into variables是完备的，我们指出这对Input paramodulation是不完备的，当变量在一个等式中只出现一次时，我们证明在input paramodulation中禁止Paramodulation into variasles是完备的。我们做了三个软件系统，①受限制的Input paramodulation②受限制Unitparamodulation③01-paramodulation。打算将上述系统用于网络教学。