This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Deduction Plans: A Basis for Intelligent Backtracking
January 1981 (vol. 3 no. 1)
pp. 52-65
Philip T. Cox, Department of Computer Science, University of Waterloo, Waterloo, Ont., Canada; Department of Computer Science, Auckland University, Auckland, Australia.
Tomasz Pietrzykowski, School of Computer Science, Acadia University, Wolfville, N.S., Canada.
A proof procedure is described that relies on the construction of certain directed graphs called ``deduction plans.'' Plans represent the structure of proofs in such a way that problem reduction may be used without imposing any ordering on the solution of subproblems, as required by other systems. The structure also allows access to all clauses deduced in the course of a proof, which may then be used as lemmas. Economy of representation is the maximum attainable, consistent with this unrestricted availability of lemmas. Restricted versions of this deduction system correspond to existing linear deduction procedures, but do not suffer from some of their shortcomings, such as redundant representation, strict ordering of subproblems, and explicit substitution. One of the rules for constructing plans, however, allows a subproblem to be factored to a previously solved one: this has no equivalent in existing system. A further economy is obtained by making it unnecessary to perform substitutions and calculate most general unifiers. The source of unification failure can be located when a subproblem is found to be unsolvable, so that exact backtracking can be performed rather than the blind backtracking performed by existing systems. Therefore, a deduction system based on the construction of plans can avoid the wasteful search of irrelevant areas of the search space that results from the usual backtracking methods.
Citation:
Philip T. Cox, Tomasz Pietrzykowski, "Deduction Plans: A Basis for Intelligent Backtracking," IEEE Transactions on Pattern Analysis and Machine Intelligence, vol. 3, no. 1, pp. 52-65, Jan. 1981, doi:10.1109/TPAMI.1981.4767050
Usage of this product signifies your acceptance of the Terms of Use.