This Article 
 Bibliographic References 
 Add to: 
A Semantically Guided Deductive System for Automatic Theorem Proving
April 1976 (vol. 25 no. 4)
pp. 328-334
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.
Index Terms:
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
Usage of this product signifies your acceptance of the Terms of Use.