Using a generalisation critic to find bisimulations for coinductive proofs
DOI10.1007/3-540-63104-6_29zbMath1430.68399OpenAlexW1541732450MaRDI QIDQ5234712
Alan Bundy, Louise Abigail Dennis, Ian Green
Publication date: 1 October 2019
Published in: Automated Deduction—CADE-14 (Search for Journal in Brave)
Full work available at URL: https://www.pure.ed.ac.uk/ws/files/6329544/Using_a_generalisation_critic_to_find_bisimulations_for_coinductive_proofs.pdf
Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)
Related Items
Uses Software
Cites Work
- Co-induction in relational semantics
- A co-induction principle for recursively defined domains
- Automated deduction -- CADE-12. 12th international conference, Nancy, France, June 26 -- July 1, 1994. Proceedings
- Implicit induction in conditional theories
- Productive use of failure in inductive proof
- A lattice-theoretical fixpoint theorem and its applications
- Circuits as streams in Coq: Verification of a sequential multiplier
- A divergence critic
- A fixedpoint approach to implementing (Co)inductive definitions
- Using a generalisation critic to find bisimulations for coinductive proofs
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item