Abstract

Logically constrained term rewriting is a relatively new formalism where rules
are equipped with constraints over some arbitrary theory. Although there are
many recent advances with respect to rewriting induction, completion,
complexity analysis and confluence analysis for logically constrained term
rewriting, these works solely focus on the syntactic side of the formalism
lacking detailed investigations on semantics. In this paper, we investigate a
semantic side of logically constrained term rewriting. To this end, we first
define constrained equations, constrained equational theories and validity of
the former based on the latter. After presenting the relationship of validity
and conversion of rewriting, we then construct a sound inference system to
prove validity of constrained equations in constrained equational theories.
Finally, we give an algebraic semantics, which enables one to establish
invalidity of constrained equations in constrained equational theories. This
algebraic semantics derives a new notion of consistency for constrained
equational theories.

BibTeX

@inproceedings{TANNJS-FSCD24,
 author    = "Takahito Aoto and Naoki Nishida and Jonas Sch\"{o}pf",
 editor    = "Jakob Rehof",
 title     = "Equational Theories and Validity for Logically Constrained
              Term Rewriting",
 booktitle = "Proceedings of the 9th International Conference on
              Formal Structures for Computation and Deduction",
 series    = "Leibniz International Proceedings in Informatics (LIPIcs)",
 volume    = 299,
 pages     = "31:1--31:21",
 year      = 2024,
 doi       = "10.4230/LIPIcs.FSCD.2024.31"
}