| Year | 2018 |
|---|---|
| Type | Conference |
| Status | Proceedings |
| Authors | Stefan Ciobaca, Dorel Lucanu |
Links
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.BibTeX
@TechReport{
name,
author = {},
title = {},
institution = {},
year = {},
number = {},
month = {},
note = {},
url = {}
}