[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to main content
Springer Nature Link
Log in

Emmy: A refutational theorem prover for first-order logic with equations

  • Conference paper
  • First Online:
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

Emmy is an implementation in Quintus Prolog of a refutational theorem prover for first-order logic with equations based on a superposition calculus. This paper describes the structure and the functionalities of this theorem prover.

This work was done while the author was a visitor at SUNY at Stony Brook, N.Y., U.S.A.. Research was supported in part by National Science Fondation under grant CCR-8901322.

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

Similar content being viewed by others

4-References

  • Bachmair L. and Dershowitz N. Equational inference, canonical proofs and proof orderings (1989).

    Google Scholar 

  • Bachmair L. and Ganzinger H. On restrictions of ordered paramodulation with simplification. Proc. 10th Int. Conf. Aut. Ded. LNCS vol. 449, pp. 427–441 (M. Stickel, ed.) (1990).

    Google Scholar 

  • Dershowitz N. Termination Journal of Symbolic Computation (1986).

    Google Scholar 

  • Deruyver A. Emmy, a refutational theorem prover for first order logic with equations. Technical report 90/26 State University of New York at Stony Brook. September 1990.

    Google Scholar 

  • Huet G. and Oppen Derek C. Equations and rewrite rules: A survey. Technical report CSL-111 SRI international January 1980.

    Google Scholar 

  • Mccharen John D., Overbeek Ross A. and Wos Laurence A. Problems and experiments for and with automated Theorem-proving programs. IEEE transactions on computers. Vol C-25 No 8 August 1976.

    Google Scholar 

  • Pelletier Francis Jeffry Seventy five problems for testing automatic theorem provers. Journal of automated reasoning (1986) pp. 191–216.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIFL UA 369 CNRS, U.F.R. D'I.E.E.A bât. M3, 59655, Villeneuve D'ascq Cedex, France

    Aline Deruyver

Authors
  1. Aline Deruyver
    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

Deruyver, A. (1991). Emmy: A refutational theorem prover for first-order logic with equations. 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_118

Download citation

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

  • 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