Proving theorems by program transformation
DOI10.3233/FI-2013-899zbMATH Open1315.03019OpenAlexW1555798792MaRDI QIDQ2865083FDOQ2865083
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
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
constraint logic programmingautomated theorem provingquantifier eliminationtemporal logicsbisimilarityprogram transformationprogram specialization
Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Mechanization of proofs and logical operations (03B35) Temporal logic (03B44)
Cited In (13)
- 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
- Title not available (Why is that?)
- Proving properties of co-logic programs by unfold/fold transformations
- On inductive proofs by extended unfold/fold transformation rules
- Constraint-based correctness proofs for logic program transformations
- Proving Properties of Constraint Logic Programs by Eliminating Existential Variables
- Automatic Correctness Proofs for Logic Program Transformations
- Synthesis and transformation of logic programs using unfold/fold proofs
- Title not available (Why is that?)
- Proving the correctness of unfold/fold program transformations using bisimulation
- The applicability of logic program analysis and transformation to theorem proving
- 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)
