Constraint-based correctness proofs for logic program transformations

DOI10.1007/s00165-012-0233-8zbMath1259.68036OpenAlexW2039210279MaRDI QIDQ1941873

Alberto Pettorossi, Maurizio Proietti, Valerio Senni

Publication date: 22 March 2013

Published in: Formal Aspects of Computing (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s00165-012-0233-8

zbMATH Keywords

program transformationconstraintslogic programmingprogram correctnesstransformation rules

Mathematics Subject Classification ID

Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Determinization of conditional term rewriting systems ⋮ Inverse Unfold Problem and Its Heuristic Solving

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• The McCarthy's recursion induction principle: oldy but goody
• Transformations of CLP modules
• Termination of rewriting
• Unfold/fold transformation of stratified programs
• A transformation system for deductive database modules with perfect model semantics
• Totally correct logic program transformations via well-founded annotations
• BEYOND TAMAKI-SATO STYLE UNFOLD/FOLD TRANSFORMATIONS FOR NORMAL LOGIC PROGRAMS
• Polytool: Polynomial interpretations as a basis for termination analysis of logic programs
• On Inductive and Coinductive Proofs via Unfold/Fold Transformations
• Transformations of logic programs on infinite lists
• Automatic Correctness Proofs for Logic Program Transformations
• SAT Solving for Termination Analysis with Polynomial Interpretations
• Continuation-Based Program Transformation Strategies
• A Transformation System for Developing Recursive Programs
• Synthesis and transformation of logic programs using unfold/fold proofs
• Coinductive Logic Programming

This page was built for publication: Constraint-based correctness proofs for logic program transformations