The Community for Technology Leaders
RSS Icon
Subscribe
Issue No.04 - April (1976 vol.25)
pp: 328-334
R. Reiter , Department of Computer Science, University ty of British Columbia
ABSTRACT
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.
CITATION
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
18 ms
(Ver 2.0)

Marketing Automation Platform Marketing Automation Tool