Proof: an implementation of theorem-proving with equality

[摘要] Mechanical theorem-proving has, in the past, been hindered by the lack of an efficient method of treating the equality relation. A system (developed by E. E. Sibert) of first-order logic has been defined based on the structure of the equality relation. The program PROOF implements this system on the Rice University Computer. The three rules of inference making up the system are presented, and modified to a more algorithmically suitable basis for PROOF. Certain heuristic additions to the system are presented, and examples are given. Finally, conclusions and suggestions for future applications of PROOF are discussed.

[发布机构] Rice University