Proving theorems by program transformation

DOI10.3233/FI-2013-899MaRDI QIDQ2865083zbMATH OpenOpenAlexFDO

Authors Fabio Fioravanti, Alberto Pettorossi, Maurizio Proietti, Valerio Senni

Publication date 28 November 2013

Published in Fundamenta Informaticae (Search for Journal in Brave)

Full work available at URL https://doi.org/10.3233/fi-2013-899

zbMATH Keywords

constraint logic programmingautomated theorem provingquantifier eliminationtemporal logicsbisimilarityprogram transformationprogram specialization

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)

Recommendations

• Automatic Correctness Proofs for Logic Program Transformations
• Constraint-based correctness proofs for logic program transformations
• On inductive proofs by extended unfold/fold transformation rules
• Synthesis and transformation of logic programs using unfold/fold proofs
• Equivalence-preserving first-order unfold/fold transformation systems

Cited in

(13)

• Constraint-based correctness proofs for logic program transformations
• Proving Properties of Constraint Logic Programs by Eliminating Existential Variables
• The applicability of logic program analysis and transformation to theorem proving
• Proving properties of co-logic programs by unfold/fold transformations
• Proving the correctness of recursion-based automatic program transformations
• On inductive proofs by extended unfold/fold transformation rules
• Proving the correctness of unfold/fold program transformations using bisimulation
• Synthesis and transformation of logic programs using unfold/fold proofs
• scientific article; zbMATH DE number 5033863 (Why is no real title available?)
• Automatic Correctness Proofs for Logic Program Transformations
• scientific article; zbMATH DE number 4029505 (Why is no real title available?)
• Program transformation, symbolic computation and algebraic manipulation. Proceedings of a symposium held at the Research Institute for Mathematical Sciences, Kyoto University, Kyoto, Japan, November 29--December 1, 1999
• Analysis and Transformation of Constrained Horn Clauses for Program Verification

This page was built for publication: Proving theorems by program transformation

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