A Human Oriented Logic for Automatic Theorem-Proving
- 1 October 1974
- journal article
- Published by Association for Computing Machinery (ACM) in Journal of the ACM
- Vol. 21 (4), 606-621
- https://doi.org/10.1145/321850.321858
Abstract
A deductive system is described which combines aspects of resolution (e.g. unification and the use of Skolem functions) with that of natural deduction and whose performance compares favorably with the best predicate calculus theorem provers.Keywords
This publication has 10 references indexed in Scilit:
- Theorem proving with variable-constrained resolutionInformation Sciences, 1972
- A Unifying View of Some Linear Herbrand ProceduresJournal of the ACM, 1972
- Experiments with a heuristic theorem-proving program for predicate calculus with equalityArtificial Intelligence, 1972
- Linear resolution with selection functionArtificial Intelligence, 1972
- Computer proofs of limit theoremsArtificial Intelligence, 1972
- Splitting and reduction heuristics in automatic theorem provingArtificial Intelligence, 1971
- The Unit Proof and the Input Proof in Theorem ProvingJournal of the ACM, 1970
- Efficiency and Completeness of the Set of Support Strategy in Theorem ProvingJournal of the ACM, 1965
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- Theorem-Proving on the ComputerJournal of the ACM, 1963