Skip to main content
SpringerLink
Log in

A narrowing-based theorem prover

  • Conference paper
  • First Online:
Book cover Rewriting Techniques and Applications (RTA 1991)

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

Included in the following conference series:

Abstract

This work presents a theorem prover for inductive proofs within an equational theory which supports the verification of universally quantified equations. This system, called TIP, is based on a modification of the well-known narrowing algorithm. Particulars of the implementation are stated and practical experiences are summarized.

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

References

  1. U. Fraus, H. Hußmann: A Narrowing-Based Theorem Prover (long version). Internal report, University of Passau, 1990

    Google Scholar 

  2. J. V. Guttag: The specification and application to programming of abstract data types. Ph.D. thesis, University of Toronto, Toronto, 1975.

    Google Scholar 

  3. U. S. Reddy: Term Rewriting Induction. CADE 10, Lecture Notes in Computer Science 249, 1990, 162–177.

    Google Scholar 

  4. M. Wirsing, P. Pepper, H. Partsch, W. Dosch, M. Broy: On hierarchies of abstract data types. Acta Informatica 20, 1983, 1–33.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Bayerisches Forschungszentrum für Wissensbasierte Systeme, Universität Passau, Postfach 2540, W-8390, Passau, Germany

    Ulrich Fraus

  2. Institut für Informatik, Technische Universität München, Postfach 20 24 20, W-8000, München 2, Germany

    Heinrich Hußmann

Authors
  1. Ulrich Fraus
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Heinrich Hußmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ronald V. Book

Rights and permissions

Reprints and permissions

Copyright information

© 1991 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fraus, U., Hußmann, H. (1991). A narrowing-based theorem prover. In: Book, R.V. (eds) Rewriting Techniques and Applications. RTA 1991. Lecture Notes in Computer Science, vol 488. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-53904-2_116

Download citation

  • DOI: https://doi.org/10.1007/3-540-53904-2_116

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

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

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation