A Semantically Guided Deductive System for Automatic Theorem-Proving

Abstract

This paper presents a semantic and deductive formal system for automatic theorem-proving. The system has, as its deductive component, a form of natural deduction. Its semantic component relies on an underlying representation of a model. This model is invoked to prune subgoals generated by the deductive component, whenever such subgoals test false in the model. In addition, the model is used to suggest inferences to be made at the deductive level. Conversely, the current state of the proof suggests changes to be made to the model, e.g. when a construction is required as in geometry. The system is seen to possess a very smooth and transparent interface between its semantics and deductive syntax. These semantic and syntactic subsystems interact continuously during the search for a proof, each suggesting to the other how next to proceed. Particularly appealing is the naturalness of the system from a human point of view.