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
CITATION STYLE
Ciobâcă, Ş., & Lucanu, D. (2018). A Coinductive Approach to Proving Reachability Properties in Logically Constrained Term Rewriting Systems. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 10900 LNAI, pp. 295–311). Springer Verlag. https://doi.org/10.1007/978-3-319-94205-6_20
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
