Canonical conditional rewrite systems

Nachum Dershowitz, Mitsuhiro Okada, G. Sivakumar

Research output: Chapter in Book/Report/Conference proceedingConference contribution

43 Citations (Scopus)

Abstract

Conditional equations have been studied for their use in the specification of abstract data types and as a computational paradigm that combines logic and function programming in a clean way. In this paper we examine different formulations of conditional equations as rewrite systems, compare their expressive power and give sufficient conditions for rewrite systems to have the “confluence” property. We then examine a restriction of these systems using a “decreasing” ordering. With this restriction, most of the basic notions (like rewriting and computing normal forms) are decidable, the “critical pair” lemma holds, and some formulations preserve canonicity.

Original languageEnglish
Title of host publication9th International Conference on Automated Deduction, Proceedings
EditorsEwing Lusk, Ross Overbeek
PublisherSpringer Verlag
Pages538-549
Number of pages12
ISBN (Print)9783540193432
DOIs
Publication statusPublished - 1988 Jan 1
Externally publishedYes
Event9th International Conference on Automated Deduction, CADE 1988 - Argonne, United States
Duration: 1988 May 231988 May 26

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume310 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

Other9th International Conference on Automated Deduction, CADE 1988
CountryUnited States
CityArgonne
Period88/5/2388/5/26

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Canonical conditional rewrite systems'. Together they form a unique fingerprint.

  • Cite this

    Dershowitz, N., Okada, M., & Sivakumar, G. (1988). Canonical conditional rewrite systems. In E. Lusk, & R. Overbeek (Eds.), 9th International Conference on Automated Deduction, Proceedings (pp. 538-549). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 310 LNCS). Springer Verlag. https://doi.org/10.1007/BFb0012855