Synthesis and transformation of logic programs using unfold/fold proofs

DOI10.1016/S0743-1066(99)00029-1MaRDI QIDQ4939537zbMATH OpenWikidataFDO

Authors Alberto Pettorossi, Maurizio Proietti

Publication date 6 February 2000

Published in The Journal of Logic Programming (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/S0743-1066(99)00029-1

zbMATH Keywords

unfold/fold proof method

Mathematics Subject Classification ID

Logic programming (68N17)

Recommendations

• scientific article; zbMATH DE number 970703
• Logic program synthesis from first-order logic specifications
• Proving theorems by program transformation
• Equivalence-preserving first-order unfold/fold transformation systems
• scientific article; zbMATH DE number 4106263

Cited in

(22)

• Logic program synthesis from first-order logic specifications
• Program development schemata as derived rules
• Constraint-based correctness proofs for logic program transformations
• Totally correct logic program transformations via well-founded annotations
• Synthesis of positive logic programs for checking a class of definitions with infinite quantification
• Proving theorems by program transformation
• Horn clause solvers for program verification
• Combining logic programs and monadic second order logics by program transformation
• On Inductive and Coinductive Proofs via Unfold/Fold Transformations
• Automatic Correctness Proofs for Logic Program Transformations
• scientific article; zbMATH DE number 4106263 (Why is no real title available?)
• scientific article; zbMATH DE number 65745 (Why is no real title available?)
• scientific article; zbMATH DE number 2077065 (Why is no real title available?)
• scientific article; zbMATH DE number 2077069 (Why is no real title available?)
• scientific article; zbMATH DE number 1497831 (Why is no real title available?)
• scientific article; zbMATH DE number 936828 (Why is no real title available?)
• Assertion based inductive verification methods for logic programs
• Logic programs as specifications in the inductive verification of logic programs
• scientific article; zbMATH DE number 7453190 (Why is no real title available?)
• scientific article; zbMATH DE number 970703 (Why is no real title available?)
• Runtime repeated recursion unfolding in CHR: a just-in-time online program optimization strategy that can achieve super-linear speedup
• First order compiler: A deterministic logic program synthesis algorithm

This page was built for publication: Synthesis and transformation of logic programs using unfold/fold proofs

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