A coinductive approach to proving reachability properties in logically constrained term rewriting systems

DOI10.1007/978-3-319-94205-6_20OpenAlexW2964321453MaRDI QIDQ1799091

Dorel Lucanu, Ştefan Ciobâcă

Publication date: 18 October 2018

Full work available at URL: https://arxiv.org/abs/1804.08308

Mathematics Subject Classification ID

Grammars and rewriting systems (68Q42) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Related Items

Operationally-based program equivalence proofs using LCTRSs, Reducing non-occurrence of specified runtime errors to all-path reachability problems of constrained rewriting, (Co)inductive proof systems for compositional proofs in reachability logic, Generalized rewrite theories, coherence completion, and symbolic methods, Programming and symbolic computation in Maude, Runtime complexity analysis of logically constrained rewriting

Uses Software

• Maude
• CVC4
• KJS