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

zbMATH Keywords

functional programmingfunctional languageautomated deductionlabeled transition systemproof method

Mathematics Subject Classification ID

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

Automating Soundness Proofs, Using a generalisation critic to find bisimulations for coinductive proofs, Towards Behavioral Maude

Uses Software

• Isabelle/ZF
• CLAM
• Oyster

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