A Hole in Goal Trees: Some Guidance from Resolution Theory
- 1 April 1976
- journal article
- Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE Transactions on Computers
- Vol. C-25 (4), 335-341
- https://doi.org/10.1109/tc.1976.1674614
Abstract
The representation power of goal-subgoal trees and the adequacy of this form of problem reduction is considered. A number of inadequacies in the classical form are illustrated, and two versions of a syntactic procedure incorporating extensions are given. Although the form of the corrections are suggested from resolution theory results, and the value of this connection emphasized, the paper discusses the goal tree format and its extensions on an informal level.Keywords
This publication has 8 references indexed in Scilit:
- Machine-Generated Problem-Solving GraphsPublished by Springer Nature ,1983
- A Unifying View of Some Linear Herbrand ProceduresJournal of the ACM, 1972
- Linear resolution with selection functionArtificial Intelligence, 1972
- Computer proofs of limit theoremsArtificial Intelligence, 1972
- Two Results on Ordering for Resolution with Merging and Linear FormatJournal of the ACM, 1971
- A Simplified Format for the Model Elimination Theorem-Proving ProcedureJournal of the ACM, 1969
- A Machine-Oriented Logic Based on the Resolution PrincipleJournal of the ACM, 1965
- The unit preference strategy in theorem provingPublished by Association for Computing Machinery (ACM) ,1964