Abstract
The paper presents a method of mechanical deduction along the lines indicated in [3]. Attempts to find refutation (s) are recorded in the form of triples: plan, constraints, conflicts. A plan corresponds to a portion of AND/OR graph search space and represents purely deductive structure of derivation. Constraints form a graph recording the attempts of unification, while con flicts identify minimal subset of the plan, removal of which restores unifiability.
This method can be applied to any initial base of (nonnecessarily Horn) clauses. Unlike the exhaustive (blind) backtracking which treats all the goals deduced in the course of proof as equally probable source of failure, this approach detects the exact source of failure.
In this method only a small fragment of solution space is kept on disk as as a collection of triples. The search strategy and the method of non-redundant processing of individual triples which leads to a solution (if it exists) is presented. This approach is compared — on a special case — with blind backtracking and an exponential improvement is demonstrated.
This work was supported by National Sciences and Engineering Research Council of Canada grants A5111 and E4450.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
Bibliography
M. Bruynooghe, L. M. Pereira, “Reivision of Top-Down Logical Reasoning Through Intelligent Backtracking”, Centre de Informatica da Universidade Nova de Lisboa, 1981.
C. L. Chang, R. C. T. Lee, “Symbolic Logic and Mechanical Theorem Proving”, New York, Academic Press, 1973.
P. T. Cox, T. Pietrzykowski, “Deduction Plans: A Basis for Intelligent Backtracking”, IEEE Trans. on Pattern Analysis and Machine Intelligence, Vol 3 N. 1, Jan. 1981.
P. T. Cox, “Representational Economy in Mechanical Theorem-Prover”, Proc. 4th Workshop Automat. Deduction, Austin TX Feb. 1979.
D. W. Loveland, “A Linear Format for Resolution”, Lect. Notes on Mathematics 125 (Symposium on Automatic Demonstration), Berlin, Spring Verlag 1970.
D. Luckham, “Refinement Theorems in Resolution Theory”, Lect. Notes on Mathematics 125 (Symposium on Automatic Demonstration), Berlin, Spring, Verlag 1970.
S. Matwin, T. Pietrzykowski,“Plan based Deduction: Data structure and Implementation”, this volume.
L. M. Pereira, F. C. N. Pereira, H. D. Warren, “User's Guide to DEC System-10 Proglog”, Laboratoria Nacional de Engenharia Civil, Lisbon.
L. M. Pereira, A. Porto, “Intelligent backtracking and Sidetracking in Horn clause programs — the theory”, Departmento de Informatica, Universidade Nova de Lisboa, 1979.
L. M. Pereira, A. Porto, “Selective Backtracking for Logic Programs”, Lect. Notes in Computer Science 81 (5th Conference on Automated Deduction), Springer-Verlag 1980.
T. Pietrzykowski, S. Matwin, “Linear Complexity of Efficient Backtracking in Plan-Based Deduction”, in preparation.
G. Roberts, “Waterloo Prolog User's Manual”, University of Waterloo, 1980.
P. Roussel, “Prolog: manuel de reference et d'utilisation”, Groupe d'Intelligence Artificielle, Marseille-Luminy, 1975.
D. H. D. Warren, “Implementing Prolog”, Department of Artificial Intelligence, Edinburgh University, 1976.
N. K. Zamov, V. I. Sharonov, “On a class of strategies which can be used to establish decidability of the resolution principle”, Issled po konstruktivnoye matematikye i matematicieskaye logikye III, vol 16, pp 54–64, 1969.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Pietrzykowski, T., Matwin, S. (1982). Exponential improvement of efficient backtracking. In: Loveland, D.W. (eds) 6th Conference on Automated Deduction. CADE 1982. Lecture Notes in Computer Science, vol 138. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0000062
Download citation
DOI: https://doi.org/10.1007/BFb0000062
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11558-8
Online ISBN: 978-3-540-39240-8
eBook Packages: Springer Book Archive