Asynchronous unfold/fold transformation for fixpoint logic

DOI10.1007/978-3-030-99461-7_3MaRDI QIDQ2163155zbMATH OpenOpenAlexFDO

Authors Mahmudul Faisal Al Ameen, Naoki Kobayashi, Ryosuke Sato

Publication date 10 August 2022

Full work available at URL https://doi.org/10.1007/978-3-030-99461-7_3

zbMATH Keywords

fixed point logicsize change graphsunfold/fold transformation

Mathematics Subject Classification ID

Logic programming (68N17) Functional programming and lambda calculus (68N18)

Recommendations

• Fold/unfold transformations for fixpoint logic
• Proving properties of co-logic programs by unfold/fold transformations
• Unfold/fold transformations of logic programs
• Program Development in Computational Logic
• scientific article; zbMATH DE number 1696824

Cites work

• Automating induction for solving Horn clauses
• Fold/unfold transformations for fixpoint logic
• On Inductive and Coinductive Proofs via Unfold/Fold Transformations
• Proving properties of co-logic programs by unfold/fold transformations
• Sequent calculi for induction and infinite descent
• Solving Horn clauses on inductive data types without induction
• The size-change principle for program termination
• Tupling calculation eliminates multiple data traversals

Describes a project that uses

Uses Software

• z3

This page was built for publication: Asynchronous unfold/fold transformation for fixpoint logic

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