A Problem-Oriented Search Procedure for Theorem Proving
- 1 August 1976
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-25 (8) , 807-815
- https://doi.org/10.1109/tc.1976.1674699
Abstract
In, this paper we argue that if search procedures are to use problem-specific information to direct a search, then they must have complete control over the deductive process. This includes the freedom to select any pair of clauses to interact as well as the freedom to select the literals upon which to attempt the interaction. We give examples to indicate the nature of inference rules which are incompatible with such search procedures. We then present a framework for a search procedure to indicate where problem-specific information may be utilized. Finally, we augment the search procedure to prevent the generation of certain redundant inferences. The augmentation makes use of lemmas to avoid replicating deduction sequences in solving multiple instances of the same subproblem at distinct places in the search space.Keywords
This publication has 12 references indexed in Scilit:
- Automatic Deduction with Hyper-ResolutionPublished by Springer Nature ,1983
- A Hole in Goal Trees: Some Guidance from Resolution TheoryIEEE Transactions on Computers, 1976
- A Human Oriented Logic for Automatic Theorem-ProvingJournal of the ACM, 1974
- The Q∗ algorithm—a search strategy for a deductive question-answering systemArtificial Intelligence, 1974
- Planning in a hierarchy of abstraction spacesArtificial Intelligence, 1974
- Linear resolution with selection functionArtificial Intelligence, 1972
- A Simplified Format for the Model Elimination Theorem-Proving ProcedureJournal of the ACM, 1969
- Mechanical Theorem-Proving by Model EliminationJournal of the ACM, 1968
- 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