Skip to main content
SpringerLink
Log in

Completeness of the pool calculus with an open built-in theory

  • Contributed Papers
  • Conference paper
  • First Online:
Computational Logic and Proof Theory (KGC 1993)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 713))

Included in the following conference series:

Abstract

We present an approach for building-in theories into theorem provers which are based on the connection method. The approach may be applied to a wide class of open, i.e. quantifier-free, theories, among them taxonomic, constraint and equational theories. We generalize the concepts of a spanning mating and of a unifier of a connection towards the theory case. We introduce the notion of the completeness of a set of theory connections with respect to a given query language. This completeness means that for a given theory there are “enough” theory connections in order to refute all theory unsatisfiable matrices which belong to the considered query language. Moreover we define the solvability of the theory unification problem in a set of theory connections. This property means that a complete set of theory unifiers may be constructed for each given theory connection. In order to prove the completeness of a prover with a built-in theory it is sufficient to construct a complete set of theory connections such that the theory unification problem in that set is solvable.

This research has been supported by a grant of the Alfried Krupp von Bohlen und Halbach-Stiftung and the Alexander von Humboldt-Stiftung.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. P. Andrews. Theorem Proving via General Matings. J. ACM, 28(2):193–214, 1981.

    Google Scholar 

  2. P. Baumgartner. Theory Model Elimination. In H. J. Ohlbach, editor, Proc. GWAI 92, 1992. MP-I-Inf.

    Google Scholar 

  3. P. Baumgartner, U. Furbach, and U. Petermann. A Unified Approach to Theory Reasoning. Forschungsbericht 15/92, University of Koblenz, 1992.

    Google Scholar 

  4. W. Bibel. Automated Theorem Proving. Vieweg, 1st edition, 1982.

    Google Scholar 

  5. R. Brachmann, R. Fikes, and H. Levesque. KRYPTON: a functional approach to knowledge representation. IEEE Computer, 16(10):67–73, October 1983.

    Google Scholar 

  6. H. Bürckert. A Resolution Principle for Clauses with Constraints. In M. E. Stickel, editor, Proc CADE 10, pages 178–192. Springer, 1990. LNCS/LNAI 449.

    Google Scholar 

  7. F. Debart, P. Enjalbert, and M. Lescot. Multi modal logic programming using equational and order-sorted logic. In M. Okada and S. Kaplan, editors, Proc. 2nd Conf. on Conditional and Typed Rewriting Systems. Springer, 1990. LNCS.

    Google Scholar 

  8. A. M. Frisch. The Substitutional Framework for Sorted Deduction: Fundamental Results on Hybrid Reasoning. Artificial Intelligence, 1991.

    Google Scholar 

  9. J. Gallier, P. Narendran, D. Plaisted, and W. Snyder. Theorem Proving with Equational Matings and Rigid E-unification. J. of ACM, 1992.

    Google Scholar 

  10. D. Loveland. Automated Theorem Proving — A Logical Basis. North Holland, 1978.

    Google Scholar 

  11. N. Murray and E. Rosenthal. Theory Links: Applications to Automated Theorem Proving. J. of Symbolic Computation, (4):173–190, 1987.

    Google Scholar 

  12. G. Neugebauer. Compiling first order logic: A prolog implementation. Technical report, FG Intellektik, Technisch Hochschule Darmstadt., 1992.

    Google Scholar 

  13. G. Neugebauer and T. Schaub. A pool-based connection calculus. Technical Report AIDA-91-02, FG Intellektik, Technische Hochschule Darmstadt., 1991.

    Google Scholar 

  14. H. Ohlbach and J. Siekmann. The Markgraf Karl Refutation Procedure. In J. Lassez and G. Plotkin, editors, Computational Logic — Essays in Honor of Alan Robinson, pages 41–112. MIT Press, 1991.

    Google Scholar 

  15. U. Petermann. How to build in an open theory into connection calculi. J. on Computer and Artificial Intelligence, 11(2):105–142, 1992.

    Google Scholar 

  16. U. Petermann. Pool calculus with built in constraint theories. Technical report, Inst.-f. Informatik, Univ. Leipzig, 1993.

    Google Scholar 

  17. H. Rasiowa and R. Sikorski. The Mathematics of Metamathematics. Polish Scientific Publishers, 1970.

    Google Scholar 

  18. M. Stickel. Automated deduction by theory resolution. J. of Automated Reasoning, 4(1):333–356, 1985.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Inst. f. Informatik, Universität Leipzig, Augustusplatz 10, D-O-7010, Leipzig, Germany

    Uwe Petermann

Authors
  1. Uwe Petermann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Georg Gottlob Alexander Leitsch Daniele Mundici

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Petermann, U. (1993). Completeness of the pool calculus with an open built-in theory. In: Gottlob, G., Leitsch, A., Mundici, D. (eds) Computational Logic and Proof Theory. KGC 1993. Lecture Notes in Computer Science, vol 713. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0022576

Download citation

  • DOI: https://doi.org/10.1007/BFb0022576

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57184-1

  • Online ISBN: 978-3-540-47943-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation