2 papers
cs.LO2026
Rewriting Induction for Existentially Quantified Equations in Logically Constrained Rewriting (Full Version)
Naoki Nishida, Kazushi Nishie, Misaki Kojima
Rewriting Induction (RI) is a principle to prove that an equation over terms is an inductive theorem of a rewrite system, i.e., that any ground instance of the equation is a theore…
cs.LO2025
Difference of Constrained Patterns in Logically Constrained Term Rewrite Systems (Full Version)
Naoki Nishida, Misaki Kojima, Yuto Nakamura
Considering patterns as sets of their instances, a difference operator over patterns computes a finite set of two given patterns, which represents the difference between the divide…