A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems
Logic in Computer Science
2018-04-24 v1
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.
Cite
@article{arxiv.1804.08308,
title = {A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems},
author = {Ştefan Ciobâcă and Dorel Lucanu},
journal= {arXiv preprint arXiv:1804.08308},
year = {2018}
}
Comments
Extended version of IJCAR 2018 article