Correctness and Completeness of Logic Programs

DOI10.1145/2898434zbMath1367.68030arXiv1412.8739OpenAlexW1804654308MaRDI QIDQ5277919

Włodzimierz Drabent

Publication date: 12 July 2017

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/1412.8739

zbMATH Keywords

logic programmingspecificationsdeclarative programmingprogram correctnessprogram completenessdeclarative diagnosis/algorithmic debugging

Mathematics Subject Classification ID

Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.) (68N19) Logic programming (68N17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items

The Prolog Debugger and Declarative Programming, On Completeness of Logic Programs, On Correctness and Completeness of an n Queens Program, On definite program answers and least Herbrand models, S-semantics -- an example, On correctness of normal logic programs, Logic + control: On program construction and verification, Proving completeness of logic programs with the cut

Uses Software

• LPTP
• XSB

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A pearl on SAT and SMT solving in Prolog
• Inductive assertion method for logic pograms
• Reasoning about termination of pure Prolog programs
• XSB: Extending Prolog with Tabled Logic Programming
• Truth versus information in logic programming
• Automated termination proofs for logic programs by term rewriting
• Polytool: Polynomial interpretations as a basis for termination analysis of logic programs
• The relation between logic programming and logic specification
• The Transformational Approach to Program Development
• Negation in logic programming
• Strong termination of logic programs
• The theoretical foundations of LPTP (a logic program theorem prover)
• The well-founded semantics for general logic programs
• Logic program synthesis
• On definite program answers and least Herbrand models
• cTI: a constraint-based termination inference tool for ISO-Prolog
• A semantic basis for the termination analysis of logic programs
• Inferring non-suspension conditions for logic programs with dynamic scheduling
• Logic + control: An example
• A three-valued semantics for logic programmers
• Proving correctness and completeness of normal programs – a declarative approach