Skip to main content
SpringerLink
Log in

GLUE: Opening the world to theorem provers

  • System-Descriptions
  • Conference paper
  • First Online:
Logic Programming And Nonmonotonic Reasoning (LPNMR 1997)

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

Abstract

GLUE is a system to combine heterogeneous and distributed sources of information with a deductive kernel. For this purpose access methods for external sources of information, like databases, can be specified. Pieces of a program are generated from such a specification which can be used also in other programs. This technique has been developed with an application to theorem provers in mind. We will show how GLUE can be used either stand-alone or together with a theorem prover like PROTEIN to solve real world problems. Some examples of problems utilizing such a combination are presented.

This work has been funded within the project “Deduktive Techniken für Informations-Management-Systeme” by the Ministry for Economy, Traffic, Agriculture, and Vinoculture of the state Rhineland-Palatinate of the Federal Republic of Germany.

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. Peter Baumgartner. Refinements of theory model elimination and a variant without contrapositives. In A.G. Cohn, editor, 11th European Conference on Artificial Intelligence, ECAI'94, pages 90–94. Wiley, 1994.

    Google Scholar 

  2. Peter Baumgartner and Ulrich Furbach. Model elimination without contrapositives. In Bundy [4], pages 87–101.

    Google Scholar 

  3. Peter Baumgartner and Ulrich Furbach. PROTEIN: A Prover with a Theory Extension INterface. In Bundy [4], pages 769–773.

    Google Scholar 

  4. Alan Bundy, editor. Proceedings of the 12 th Conference on Automated Deduction, Nancy, France, June/July 1994. Springer Verlag, Berlin, Heidelberg, New-York, 1994.

    Google Scholar 

  5. Donald E. Knuth. Sorting and Searching, volume 3 of The Art of Computer Programming. Addison Wesley, Reading, MA, 1973.

    Google Scholar 

  6. D. W. Loveland. A simplified version for the model elimination theorem proving procedure. Journal of the ACM, 16(3), 1969.

    Google Scholar 

  7. Mark E. Stickel. A Prolog Technology Theorem Prover: Implementation by an extended Prolog compiler. Journal of Automated Reasoning, 4:353–380, 1988.

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Fachbereich Informatik, Universität Koblenz-Landau, Rheinau 1, 56075, Koblenz, Germany

    Gerd Neugebauer & Dorothea Schäfer

Authors
  1. Gerd Neugebauer
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dorothea Schäfer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jürgen Dix Ulrich Furbach Anil Nerode

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Neugebauer, G., Schäfer, D. (1997). GLUE: Opening the world to theorem provers. In: Dix, J., Furbach, U., Nerode, A. (eds) Logic Programming And Nonmonotonic Reasoning. LPNMR 1997. Lecture Notes in Computer Science, vol 1265. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63255-7_31

Download citation

  • DOI: https://doi.org/10.1007/3-540-63255-7_31

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63255-9

  • Online ISBN: 978-3-540-69249-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation