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

automated theorem provingbisimilarityconstraint logic programmingprogram specializationprogram transformationquantifier eliminationtemporal logics

Mathematics Subject Classification ID

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

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
• 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
• On inductive proofs by extended unfold/fold transformation rules
• Proving the correctness of unfold/fold program transformations using bisimulation
• Automatic Correctness Proofs for Logic Program Transformations
• scientific article; zbMATH DE number 4029505 (Why is no real title available?)
• Proving properties of co-logic programs by unfold/fold transformations
• Synthesis and transformation of logic programs using unfold/fold proofs
• The applicability of logic program analysis and transformation to theorem proving
• Proving Properties of Constraint Logic Programs by Eliminating Existential Variables
• scientific article; zbMATH DE number 5033863 (Why is no real title available?)
• Analysis and Transformation of Constrained Horn Clauses for Program Verification
• Proving the correctness of recursion-based automatic program transformations

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)