Some Proof Procedures Based on Herbrand's Theorem
- 1 January 1973
- book chapter
- Published by Elsevier
Abstract
No abstract availableThis publication has 8 references indexed in Scilit:
- Theorem proving with variable-constrained resolutionInformation Sciences, 1972
- A Unifying View of Some Linear Herbrand ProceduresJournal of the ACM, 1972
- Finding resolution proofs and using duplicate goals in and/or treesInformation Sciences, 1971
- The utility of independent subgoals in theorem provingInformation and Control, 1971
- Splitting and reduction heuristics in automatic theorem provingArtificial Intelligence, 1971
- Mechanical Theorem-Proving by Model EliminationJournal of the ACM, 1968
- Completeness and Hauptsatz for second order logic1Theoria, 1967
- The Concept of Demodulation in Theorem ProvingJournal of the ACM, 1967