On Inductive and Coinductive Proofs via Unfold/Fold Transformations
From MaRDI portal
Publication:3558288
DOI10.1007/978-3-642-12592-8_7zbMATH Open1284.68201OpenAlexW1599791095MaRDI QIDQ3558288FDOQ3558288
Authors: Hirohisa Seki 
Publication date: 4 May 2010
Published in: Logic-Based Program Synthesis and Transformation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/978-3-642-12592-8_7
Recommendations
- On inductive proofs by extended unfold/fold transformation rules
- Proving properties of co-logic programs by unfold/fold transformations
- Inductive proofs by specification transformations
- Fold-unfold lemmas for reasoning about recursive programs using the Coq proof assistant
- Integrating induction and coinduction via closure operators and proof cycles
- Synthesis and transformation of logic programs using unfold/fold proofs
- A coinductive approach to proof search
- On transforming cut- and quantifier-free cyclic proofs into rewriting-induction proofs
- On Extending Bounded Proofs to Inductive Proofs
- scientific article; zbMATH DE number 1231696
Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Cited In (7)
- Proving properties of co-logic programs with negation by program transformations
- Proving properties of co-logic programs by unfold/fold transformations
- On inductive proofs by extended unfold/fold transformation rules
- Asynchronous unfold/fold transformation for fixpoint logic
- Constraint-based correctness proofs for logic program transformations
- Induction, coinduction, and adjoints
- Removing algebraic data types from constrained Horn clauses using difference predicates
This page was built for publication: On Inductive and Coinductive Proofs via Unfold/Fold Transformations
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3558288)
