Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Theorem Proving with Analytic Tableaux and Related Methods

TABLEAUX 1995: Theorem Proving with Analytic Tableaux and Related Methods pp 201–216Cite as

Constraint model elimination and a PTTP-implementation

  • Classical Logic — Connection Method and Model Elimination
  • Conference paper
  • First Online:

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

Abstract

In constraint logic programming, proof procedures for Horn clauses are enhanced with an interface to efficient constraint solvers. The question arises whether it is possible to incorporate constraint processing into general, non-Horn theorem proving calculi. In this paper, a positive answer to this question will be given.

A framework for a new calculus is introduced which combines model elimination with constraint solving, following the lines of Bürckert (1991). A prototype system has been implemented rapidly by only combining a PROLOG technology implementation of model elimination and PROLOG with constraints. Some example studies, e.g. taxonomic reasoning, show the advantages and some problems with this procedure.

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

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Owen L. Astrachan and Mark E. Stickel. Caching and Lemmaizing in Model Elimination Theorem Provers. In D. Kapur, editor, Proceedings of the 11th International Conference on Automated Deduction (CADE-11), pages 224–238. Springer-Verlag, June 1992. LNAI 607.

    Google Scholar 

  2. Peter Baumgartner. Refinements of theory model elimination and a variant without contrapositives. Fachberichte Informatik 8/93, Universität Koblenz-Landau, Koblenz, 1993.

    Google Scholar 

  3. P. Baumgartner. Refinements of Theory Model Elimination and a Variant without Contrapositives. In A.G. Cohn, editor, 11th European Conference on Artificial Intelligence, ECAI94. Wiley, 1994.

    Google Scholar 

  4. Franz Baader, Hans-Jürgen Bürckert, Bernhard Hollunder, Werner Nutt, and Jörg H. Siekmann. Concept logics. Research Report RR-90-10, DFKI, Kaiserslautern, Saarbrücken, September 1990. Also in Proceedings of the Symposium on Computational Logics, Brüssel, Belgium, 1990.

    Google Scholar 

  5. Martin Buchheit, Franceso M. Donini, and Andrea Schaerf. Decidable reasoning in terminological knowledge systems. Journal of Artificial Intelligence Research, 1:109–138, 1993.

    Google Scholar 

  6. Peter Baumgartner and Ulrich Furbach. Protein: A PROver with a Theory Extension INterface. In Alan Bundy, editor, Proceedings of the 12th International Conference on Automated Deduction, Nancy, France, June/July 1994, pages 769–773. Springer, Berlin, Heidelberg, New York, 1994. LNAI 814.

    Google Scholar 

  7. Peter Baumgartner, Ulrich Furbach, and Uwe Petermann. A unified approach to theory reasoning. Fachberichte Informatik 15/92, Universität Koblenz-Landau, Koblenz, 1992.

    Google Scholar 

  8. Ronald J. Brachman, Victoria Pigman Gilbert, and Hector J. Levesque. An essential hybrid reasoning system: Knowledge and symbol level accounts of KRYPTON. In Aravind Joshi, editor, Proceedings of the 9th International Joint Conference on Artificial Intelligence, Los Angeles, CA, August 1985, pages 532–539. Morgan Kaufmann, Los Altos, CA, 1985. Volume 1.

    Google Scholar 

  9. Franz Baader and Bernhard Hollunder. A terminological knowledge representation system with complete inference algorithms. In Harold Boley and Michael M. Richter, editors, Proceedings of the International Workshop on Processing Declarative Knowledge, Kaiserslautem, Germany, July 1991, pages 67–86. Springer, Berlin, Heidelberg, New York, 1991. LNAI 567.

    Google Scholar 

  10. Ronald J. Brachman and J. G. Schmolze. An overview of the KL-ONE knowledge representation system. Cognitive Science, 9(2):171–216, 1985.

    Article  Google Scholar 

  11. Hans-Jürgen Bürckert. A Resolution Principle for a Logic with Restricted Quantifiers. LNAI 568. Springer, Berlin, Heidelberg, New York, 1991.

    Google Scholar 

  12. Hans-Jürgen Bürckert. A resolution principle for constrained logics. Artificial Intelligence, 66(2):235–271, 1994.

    Article  Google Scholar 

  13. Ricardo Caffera and Nicolas Zabel. A method for simultaneous search for refutations and models by equational constraint solving. Journal of Symbolic Computation, 13:613–641, 1992.

    Google Scholar 

  14. ECRC GmbH, München. ECLiPSe 3.4: User Manual — Extensions User Manual, January 1994.

    Google Scholar 

  15. Thom Frühwirth and Philipp Hanschke. Terminological reasoning with constraint handling rules. Technical Report ECRC-94-6, ECRC GmbH, München, 1994.

    Google Scholar 

  16. Alan M. Frisch. The substitutional framework for sorted deduction: fundamental results on hybrid reasoning. Artificial Intelligence, 49:161–198, 1991.

    Article  Google Scholar 

  17. Thom Frühwirth. Constraint simplification rules. Technical Report ECRC-92-18, ECRC GmbH, München, 1993. Revised version.

    Google Scholar 

  18. Markus Höhfeld and Gert Smolka. Definite relations over constraint languages. LILOG Report 53, IBM Deutschland, Stuttgart, October 1988.

    Google Scholar 

  19. Joxan Jaffar and Michael J. Mäher. Constraint logic programming: a survey. Journal of Logic Programming, 19, 20:503–581, 1994.

    Article  Google Scholar 

  20. John Wylie Lloyd. Foundations of Logic Programming. Springer, Berlin, Heidelberg, New York, 1987.

    Google Scholar 

  21. D. Loveland. Mechanical Theorem Proving by Model Elimination. JACM, 15(2), 1968.

    Google Scholar 

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

    Google Scholar 

  23. Richard A. O'Keefe. The Craft of Prolog. MIT Press, Cambridge, MA; London, England, 1990.

    Google Scholar 

  24. Hans Jürgen Ohlbach and Manfred Schmidt-Schauß. The lion and the unicorn. Journal of Automated Reasoning, 1(3):327–332, 1985.

    Google Scholar 

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

    Article  Google Scholar 

  26. Frieder Stolzenburg and Peter Baumgartner. Constraint model elimination and a PTTP-implementation. Fachberichte Informatik 10/94, Universität Koblenz-Landau, Koblenz, September 1994.

    Google Scholar 

  27. Raymond M. Smullyan. What is the name of this book? The riddle of Dracula and other logical puzzles. Prentice-Hall, Englewood Cliffs, NJ, 1978.

    Google Scholar 

  28. Manfred Schmidt-Schauß and Gert Smolka. Attributive concept descriptions with complements. Artificial Intelligence, 48(1):1–26, 1991.

    Article  Google Scholar 

  29. Mark E. Stickel. Automated deduction by theory resolution. Journal of Automated Reasoning, 1(3):333–355, 1985.

    Article  Google Scholar 

  30. Mark E. Stickel. Schubert's Steamroller problem: Formulations and solutions. Journal of Automated Reasoning, 2:89–101, 1986.

    Article  Google Scholar 

  31. M. Stickel. A Prolog Technology Theorem Prover: A New Exposition and Implementation in Prolog. Technical note 464, SRI International, 1989.

    Google Scholar 

  32. Frieder Stolzenburg. Logic programming with sets by membership-constraints. In Norbert E. Fuchs and Georg Gottlob, editors, Proceedings of the 10th Logic Programming Workshop, Universität Zürich, 1994. Institut für Informatik. Technical Report ifi 94.10.

    Google Scholar 

  33. Pascal Van Hentenryck. Constraint Satisfaction in Logic Programming. MIT Press, Cambridge, MA, London, England, 1989.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universität Kohlenz, Rheinau 1, D-56075, Koblenz

    Peter Baumgartner & Frieder Stolzenburg

Authors
  1. Peter Baumgartner
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Frieder Stolzenburg
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Peter Baumgartner Reiner Hähnle Joachim Possega

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Baumgartner, P., Stolzenburg, F. (1995). Constraint model elimination and a PTTP-implementation. In: Baumgartner, P., Hähnle, R., Possega, J. (eds) Theorem Proving with Analytic Tableaux and Related Methods. TABLEAUX 1995. Lecture Notes in Computer Science, vol 918. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-59338-1_37

Download citation

  • DOI: https://doi.org/10.1007/3-540-59338-1_37

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-59338-6

  • Online ISBN: 978-3-540-49235-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation