Synthesis of positive logic programs for checking a class of definitions with infinite quantification
From MaRDI portal
Publication:2629858
DOI10.1016/j.ic.2016.06.014zbMath1353.68050OpenAlexW2439147558MaRDI QIDQ2629858
José M. Cañete-Valdeón, Francisco J. Galán
Publication date: 7 July 2016
Published in: Information and Computation (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1016/j.ic.2016.06.014
Logic in computer science (03B70) Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)
Uses Software
Cites Work
- Unfolding--definition--folding, in this order, for avoiding unnecessary variables in logic programs
- First order compiler: A deterministic logic program synthesis algorithm
- The calculus of constructions
- Equivalence-preserving first-order unfold/fold transformation systems
- Adding metatheoretic facilities to first-order theories
- SWI-Prolog
- Taking Satisfiability to the Next Level with Z3
- Lifting abstract interpreters to quantified logical domains
- Completed logic programs and their consistency
- Simplify: a theorem prover for program checking
- Solving Quantified Verification Conditions Using Satisfiability Modulo Theories
- Derivation of Logic Programs
- Logic programming and negation: A survey
- A transformational approach to negation in logic programming
- Synthesis and transformation of logic programs using unfold/fold proofs
- From program verification to program synthesis
- Unfold⧸fold transformation of general logic programs for the well-founded semantics
- Program Development in Computational Logic
- Integrated Formal Methods
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
