Abstract
In this paper we present a method to detect non-terminating ox failing queries based on analyzing the dynamic growth of terms. It overcomes restrictions known from approaches to preclude infinite loops in the field of logic programming. The general idea is to predetermine what may happen to a term while performing inference steps. Various well-known techniques and results of the theory of formal languages are used. The strength of our technique is emphasized by the fact that using it we are able to decide Horn-formulas consisting of facts, two-literal clauses, and a goal literal all of them restricted to unary predicate and unary function symbols.
This research was supported by the Deutsche Forschungsgemeinschaft (DFG) within project KONNEKTIONSBEWEISER under grant no. Bi 228/6-1.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
K. R. Apt, R. N. Bol and J. W. Klop: On the safe termination of PROLOG programs, Proc. 6th Conf. on Logic Programming, G. Levi and M. Martelli (eds.), MIT Press, Cambridge MA, 1989.
P. Besnard: On infinite loops in logic programming, IRISA, Publication Interne No. 488, 1989.
E. W. Beth: Semantic entailment and formal derivability, Mededlingen der Koninklijke Nederlandse Akademie van Wetenschappen, 18(13), 1955.
W. Bibel: Automated Theorem Proving, Vieweg Verlag, Braunschweig, second edition, 1987.
W. Bibel: Deduktion, Automatisierung der Logik, Oldenbourg Verlag, München, 1992.
S. Brüning: Search Space Pruning by Checking Dynamic Term Growth, Technical Report AIDA-92-19, TH Darmstadt, 1992.
S. Brüning: On Search Space Pruning by Checking Dynamic Term Growth, Technical Report, TH Darmstadt, forthcoming.
J. E. Hopcroft and J. D. Ullman: Formal languages and their relation to automata, Addison-Wesley, 1969.
P. Hanschke and J. Würtz: Satisfiability of the smallest binary program, Information Processing Letters 45(5), 1993.
R. Letz and J. Schumann and S. Bayerl and W. Bibel: SETHEO: A High Performance Theorem Prover, Journal of Automated Reasoning 8, 1992.
L. Plümer: Termination proofs for Logic Programs, LNAI 446, 1990.
M. O. Rabin: Decidability of second order theories and automata on infinite trees, Trans. Amer. Math. Soc. 141, 1969.
J. A. Robinson: A machine-oriented logic based on the resolution principle, Journal of the ACM, 12(1), 23–41, 1965.
G. Salzer: Solvable Classes of Cycle Unification Problems, Proc. IMYCS'92, 1992.
D. E. Smith and M. R. Genesereth and M. L. Ginsberg: Controlling recursive inference, Artificial Intelligence, 30, 343–389, 1986.
R. M. Smullyan: First-Order Logic, Ergebnisse der Mathematik und ihrer Grenzgebiete, Springer-Verlag, 1971.
M. E. Stickel: A PROLOG technology theorem prover: implementation by an extended PROLOG compiler, Journal of Automated Reasoning, 4, 353–380, 1988.
J. Würtz: Unifying Cycles, research report RR-92-22, DFKI, Saarbrücken, 1992.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brüning, S. (1993). Search space pruning by checking dynamic term growth. In: Voronkov, A. (eds) Logic Programming and Automated Reasoning. LPAR 1993. Lecture Notes in Computer Science, vol 698. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56944-8_41
Download citation
DOI: https://doi.org/10.1007/3-540-56944-8_41
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56944-2
Online ISBN: 978-3-540-47830-0
eBook Packages: Springer Book Archive