Using a generalisation critic to find bisimulations for coinductive proofs

DOI10.1007/3-540-63104-6_29MaRDI QIDQ5234712zbMATH OpenOpenAlexFDO

Authors Louise A. Dennis, Alan Bundy, 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

automated deductionfunctional languagefunctional programminglabeled transition systemproof method

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
• The power of parameterization in coinductive proof
• Generalised coinduction
• Beyond Bisimulation: The “up-to” Techniques
• Incremental pattern-based coinduction for process algebra and its Isabelle formalization

Cites work

• A co-induction principle for recursively defined domains
• A divergence critic
• A fixedpoint approach to implementing (co)inductive definitions
• A lattice-theoretical fixpoint theorem and its applications
• Automated deduction -- CADE-12. 12th international conference, Nancy, France, June 26 -- July 1, 1994. Proceedings
• Circuits as streams in Coq: verification of a sequential multiplier
• Co-induction in relational semantics
• scientific article; zbMATH DE number 4180818 (Why is no real title available?)
• scientific article; zbMATH DE number 4054988 (Why is no real title available?)
• scientific article; zbMATH DE number 4072439 (Why is no real title available?)
• scientific article; zbMATH DE number 42752 (Why is no real title available?)
• scientific article; zbMATH DE number 1231459 (Why is no real title available?)
• scientific article; zbMATH DE number 1348478 (Why is no real title available?)
• Implicit induction in conditional theories
• Productive use of failure in inductive proof
• The OYSTER-CLAM system
• Using a generalisation critic to find bisimulations for coinductive proofs

Cited in

(5)

• Making a productive use of failure to generate witnesses for coinduction from divergent proof attempts
• Automating soundness proofs
• Towards behavioral Maude: behavioral membership equational logic
• Incremental pattern-based coinduction for process algebra and its Isabelle formalization
• Using a generalisation critic to find bisimulations for coinductive proofs

Describes a project that uses

Uses Software

• Isabelle/ZF
• CLAM
• Oyster

This page was built for publication: Using a generalisation critic to find bisimulations for coinductive proofs

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5234712)