A Semantically Guided Deductive System for Automatic Theorem Proving
- 1 April 1976
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-25 (4), 328-334
- https://doi.org/10.1109/tc.1976.1674613
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.Keywords
This publication has 11 references indexed in Scilit:
- A Human Oriented Logic for Automatic Theorem-ProvingJournal of the ACM, 1974
- Computer proofs of limit theoremsArtificial Intelligence, 1972
- Splitting and reduction heuristics in automatic theorem provingArtificial Intelligence, 1971
- A linear format for resolutionPublished by Springer Nature ,1970
- Resolution With MergingJournal of the ACM, 1968
- The Concept of Demodulation in Theorem ProvingJournal of the ACM, 1967
- Automatic Theorem Proving With Renamable and Semantic ResolutionJournal of the ACM, 1967
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- A Computing Procedure for Quantification TheoryJournal of the ACM, 1960
- Toward Mechanical MathematicsIBM Journal of Research and Development, 1960