On Inductive and Coinductive Proofs via Unfold/Fold Transformations

DOI10.1007/978-3-642-12592-8_7zbMath1284.68201OpenAlexW1599791095MaRDI QIDQ3558288

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

zbMATH Keywords

coinductionunfold/fold transformationnegative unfoldingpreservation of equivalence

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (4)

Asynchronous unfold/fold transformation for fixpoint logic ⋮ Constraint-based correctness proofs for logic program transformations ⋮ On Inductive Proofs by Extended Unfold/Fold Transformation Rules ⋮ 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