Skip to main content
SpringerLink
Log in

Term Rewriting in a Logic of Special Relations

  • Conference paper
  • First Online:
Algebraic Methodology and Software Technology (AMAST 1999)

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

Abstract

Although there exist logics that extend the expressiveness of order-sorted equational logic using additional binary relations besides equality in their logical theories, standard equational rewriting is still the foundation of their operational semantics. But rewriting is not necessarily restricted to the replacement of equals by equals only, and can be generalized to other ‘special’ binary relations. I show in this paper that by applying rewrite techniques to logical theories considered as instances of a general ‘logic of special relations’ we can unify and hence simplify the computational analysis within these theories.

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

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. L. Bachmair and H. Ganzinger. Ordered chaining calculi for first-order theories of binary relations. Technical Report MPI-I-95-2-009, Max-Plank-Institut für Informatik, 1995.

    Google Scholar 

  2. A. Bouhoula, J.-P. Jouannaud, and J. Meseguer. Specification and proof in membership equational logic. In TAPSOF’97, volume 1214 of Lecture Notes in Com-puter Science, pages 67–92. Springer, 1997.

    Google Scholar 

  3. H. Comon. Completion of rewrite systems with membership constraints, Part I: Deduction rules. Journal of Symbolic Computation, 25(4):397–419, 1998.

    Article  MATH  MathSciNet  Google Scholar 

  4. N. Dershowitz and J.-P. Jouannaud. Rewrite systems. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B. Elsevier Science, 1990.

    Google Scholar 

  5. S. Eker and J. Meseguer. Design of the equational proving tools for Cafe, Mar. 1997. Slides of a talk given at the Cafe Workshop, Japan.

    Google Scholar 

  6. P. J. Freyd and A. Scedrov. Categories, Allegories. North-Holland, 1990.

    Google Scholar 

  7. H. Ganzinger. Order-sorted completion: The many-sorted way. In TAPSOFT’ 89, volume 351 of Lecture Notes in Computer Science, pages 244–258. Springer, 1989.

    Google Scholar 

  8. I. Gnaedig, C. Kirchner, and H. Kirchner. Equational completion in order-sorted algebras. In CAAP’ 88, volume 299 of Lecture Notes in Computer Science, pages 165–184. Springer, 1988.

    Chapter  Google Scholar 

  9. G. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. Journal of the ACM, 27(4):797–821, 1980.

    Article  MATH  MathSciNet  Google Scholar 

  10. C. Kirchner, H. Kirchner, and J. Meseguer. Operational semantics of OBJ-3. In ICALP’ 88, volume 317 of Lecture Notes in Computer Science. Springer, 1988.

    Google Scholar 

  11. J. Levy and J. Agustí. Bi-rewrite systems. Journal of Symbolic Computation, 22(3):279–314, 1996.

    Article  MATH  MathSciNet  Google Scholar 

  12. V. Manca, A. Salibra, and G. Scollo. Equational type logic. Theoretical Computer Science, 77:131–159, 1990.

    Article  MathSciNet  MATH  Google Scholar 

  13. Z. Manna and R. Waldinger. Special relations in automated deduction. Journal of the ACM, 33(1):1–59, 1986.

    Article  MATH  MathSciNet  Google Scholar 

  14. Z. Manna and R. Waldinger. The special-relation rules are incomplete. In Automated Deduction-CADE-11, volume 607 of Lecture Notes in Artificial Intelligence, pages 492–506. Springer, 1992.

    Google Scholar 

  15. A. Mégrelis. Partial algebra + order-sorted algebra = galactic algebra. In Logical Foundations of Computer Science, volume 620 of Lecture Notes in Computer Science, pages 314–325. Springer, 1992.

    Chapter  Google Scholar 

  16. J. Meseguer. Membership algebras, July 1996. Lecture at the Dagstuhl Seminar on Specification and Semantics.

    Google Scholar 

  17. P. Mosses. Unified algebras and institutions. In Principles of Programming Languages Conference, pages 304–312. ACM Press, 1989.

    Google Scholar 

  18. W. M. Schorlemmer. Bi-rewriting rewriting logic. In First International Workshop on Rewriting Logic and its Applications, volume 4 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1996.

    Google Scholar 

  19. W. M. Schorlemmer. Unicfialcul de demostració per a la lógica de reescriptura. Research Report IIIA 96/28, Institut d’Investigació en Intel-ligéncial Artificial (CSIC), Dec. 1996. In Catalan.

    Google Scholar 

  20. W. M. Schorlemmer. Rewriting logic as a logic of special relations. In Second International Workshop on Rewriting Logic and its Applications, volume 15 of Electronic Notes in Theoretical Computer Science. Elsevier Science, 1998.

    Google Scholar 

  21. W. W. Wadge. Classified algebras. Research Report 46, Depatment of Computer Science, University of Warwick, 1982.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut d’Investigació en Intel·ligència Artificial Consell Superior d’Investigacions Científiques Departament de Llenguatges i Sistemes Informàtics, Universitat Politècnica de Catalunya, France

    W. Marco Schorlemmer

Authors
  1. W. Marco Schorlemmer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Departamento de Informática, Pontifícia Laboratório de Métodos Formais, Universidade Católica do Rio de Janeiro, Rua Marquês De São Vicente, 225, 22453-900, Rio de Janeiro, RJ, Brazil

    Armando M. Haeberer

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schorlemmer, W.M. (1998). Term Rewriting in a Logic of Special Relations. In: Haeberer, A.M. (eds) Algebraic Methodology and Software Technology. AMAST 1999. Lecture Notes in Computer Science, vol 1548. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-49253-4_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-49253-4_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-49253-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation