Skip to main content
SpringerLink
Log in
Book cover

International Conference on Automated Deduction

CADE 1988: 9th International Conference on Automated Deduction pp 435–453Cite as

Term rewriting: Some experimental results

  • Conference paper
  • First Online:

  • 160 Accesses

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

Abstract

We discuss term rewriting in conjunction with sprfn, a Prolog-based theorem prover. Two techniques for theorem proving that utilize term rewriting are presented. We demonstrate their effectiveness by exhibiting the results of our experiments in proving some theorems of von Neumann-Bernays-Gödel set theory. Some outstanding problems associated with term rewriting are also addressed.

This research was supported in part by the National Science Foundation under grant DCR-8516243 and by the Office of Naval Research under grant N00014-86-K-0680.

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. Plaisted, D.A., ‘A simplified problem reduction format', Artificial Intelligence 18 (1982) 227–261

    Article  Google Scholar 

  2. Boyer, Robert, Lusk, Ewing, McCune, William, Overbeek, Ross, Stickel, Mark, and Wos, Lawrence, ‘Set theory in first-order logic: clauses for Gödel's axioms', Journal of Automated Reasoning 2 (1986) 287–327

    Google Scholar 

  3. Plaisted, D.A., ‘Another extension of Horn clause logic programming to non-Horn clauses', Lecture Notes 1987

    Google Scholar 

  4. Plaisted, D.A., ‘Non-Horn clause logic programming without contrapositives', unpublished manuscript 1987

    Google Scholar 

  5. Loveland, D.W., Automated Theorem Proving: A Logical Base, North-Holland Publishing Co., 1978, Chapter 6.

    Google Scholar 

  6. Korf, R.E., ‘Depth-first iterative-deepening: an optimal admissible tree search', Artificial Intelligence 27 (1985) 97–109.

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of North Carolina at Chapel Hill, 27514, Chapel Hill, North Carolina

    Richard C. Potter & David A. Plaisted

Authors
  1. Richard C. Potter
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. David A. Plaisted
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Ewing Lusk Ross Overbeek

Rights and permissions

Reprints and permissions

Copyright information

© 1988 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Potter, R.C., Plaisted, D.A. (1988). Term rewriting: Some experimental results. In: Lusk, E., Overbeek, R. (eds) 9th International Conference on Automated Deduction. CADE 1988. Lecture Notes in Computer Science, vol 310. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0012848

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-19343-2

  • Online ISBN: 978-3-540-39216-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation