A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems

TL;DR

This paper presents a coinductive proof system for verifying reachability in transition systems defined by logically constrained term rewriting, enabling finite proofs of infinite behaviors.

Contribution

It introduces a sound and complete coinductive calculus with a circularity rule for finite representation of infinite proofs in term rewriting systems.

Findings

The proof system is sound and complete.

Circularity rule enables finite proofs of infinite behaviors.

Applicable to systems with complex constraints.

Abstract

We introduce a sound and complete coinductive proof system for reachability properties in transition systems generated by logically constrained term rewriting rules over an order-sorted signature modulo builtins. A key feature of the calculus is a circularity proof rule, which allows to obtain finite representations of the infinite coinductive proofs.