Strict coherence of conditional rewriting modulo axioms

Research output: Contribution to journalArticlepeer-review


Conditional rewriting modulo axioms with rich types makes specifications and declarative programs very expressive and succinct and is used in all well-known rule-based languages. However, the current foundations of rewriting modulo axioms have focused for the most part on the unconditional and untyped case. The main purpose of this work is to generalize the foundations of rewriting modulo axioms to the conditional order-sorted case. A related goal is to simplify such foundations. In particular, even in the unconditional case, the notion of strict coherence proposed here makes rewriting modulo axioms simpler and easier to understand. Properties of strictly coherent conditional theories, like operational equi-termination of the →R/B and →R,B relations and general conditions for the conditional Church–Rosser property modulo B are also studied.

Original languageEnglish (US)
Pages (from-to)1-35
Number of pages35
JournalTheoretical Computer Science
StatePublished - Apr 11 2017


  • Church–Rosser property
  • Coherence
  • Conditional rewriting modulo equations
  • Operational termination
  • Order-sorted specifications

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Strict coherence of conditional rewriting modulo axioms'. Together they form a unique fingerprint.

Cite this