Issue No.04 - April (1976 vol.25)
R. Reiter , Department of Computer Science, University ty of British Columbia
A semantic and deductive formal system for automatic theorem proving is presented. 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.
Natural deduction, semantics, theorem proving.
R. Reiter, "A Semantically Guided Deductive System for Automatic Theorem Proving", IEEE Transactions on Computers, vol.25, no. 4, pp. 328-334, April 1976, doi:10.1109/TC.1976.1674613