[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content

Search space pruning by checking dynamic term growth

  • Conference paper
  • First Online:
Logic Programming and Automated Reasoning (LPAR 1993)

Part of the book series: Lecture Notes in Computer Science ((LNAI,volume 698))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

Similar content being viewed by others

References

  1. 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.

    Google Scholar 

  2. P. Besnard: On infinite loops in logic programming, IRISA, Publication Interne No. 488, 1989.

    Google Scholar 

  3. E. W. Beth: Semantic entailment and formal derivability, Mededlingen der Koninklijke Nederlandse Akademie van Wetenschappen, 18(13), 1955.

    Google Scholar 

  4. W. Bibel: Automated Theorem Proving, Vieweg Verlag, Braunschweig, second edition, 1987.

    Google Scholar 

  5. W. Bibel: Deduktion, Automatisierung der Logik, Oldenbourg Verlag, München, 1992.

    Google Scholar 

  6. S. Brüning: Search Space Pruning by Checking Dynamic Term Growth, Technical Report AIDA-92-19, TH Darmstadt, 1992.

    Google Scholar 

  7. S. Brüning: On Search Space Pruning by Checking Dynamic Term Growth, Technical Report, TH Darmstadt, forthcoming.

    Google Scholar 

  8. J. E. Hopcroft and J. D. Ullman: Formal languages and their relation to automata, Addison-Wesley, 1969.

    Google Scholar 

  9. P. Hanschke and J. Würtz: Satisfiability of the smallest binary program, Information Processing Letters 45(5), 1993.

    Google Scholar 

  10. R. Letz and J. Schumann and S. Bayerl and W. Bibel: SETHEO: A High Performance Theorem Prover, Journal of Automated Reasoning 8, 1992.

    Google Scholar 

  11. L. Plümer: Termination proofs for Logic Programs, LNAI 446, 1990.

    Google Scholar 

  12. M. O. Rabin: Decidability of second order theories and automata on infinite trees, Trans. Amer. Math. Soc. 141, 1969.

    Google Scholar 

  13. J. A. Robinson: A machine-oriented logic based on the resolution principle, Journal of the ACM, 12(1), 23–41, 1965.

    Article  Google Scholar 

  14. G. Salzer: Solvable Classes of Cycle Unification Problems, Proc. IMYCS'92, 1992.

    Google Scholar 

  15. D. E. Smith and M. R. Genesereth and M. L. Ginsberg: Controlling recursive inference, Artificial Intelligence, 30, 343–389, 1986.

    Article  Google Scholar 

  16. R. M. Smullyan: First-Order Logic, Ergebnisse der Mathematik und ihrer Grenzgebiete, Springer-Verlag, 1971.

    Google Scholar 

  17. M. E. Stickel: A PROLOG technology theorem prover: implementation by an extended PROLOG compiler, Journal of Automated Reasoning, 4, 353–380, 1988.

    Article  Google Scholar 

  18. J. Würtz: Unifying Cycles, research report RR-92-22, DFKI, Saarbrücken, 1992.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Andrei Voronkov

Rights and permissions

Reprints 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

Publish with us

Policies and ethics