Logic + control: On program construction and verification
From MaRDI portal
Publication:4603427
DOI10.1017/S1471068417000047zbMath1425.68051arXiv1110.4978OpenAlexW2963114687MaRDI QIDQ4603427
Publication date: 20 February 2018
Published in: Theory and Practice of Logic Programming (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/1110.4978
program transformationlogic programmingspecificationflounderingdeclarative programmingprogram correctnessprogram completenessoccur-check
Specification and verification (program logics, model checking, etc.) (68Q60) Logic programming (68N17)
Related Items
The Prolog Debugger and Declarative Programming ⋮ On Correctness and Completeness of an n Queens Program ⋮ A relaxed condition for avoiding the occur-check ⋮ On correctness of normal logic programs ⋮ Backjumping is Exception Handling
Uses Software
Cites Work
- Unnamed Item
- A pearl on SAT and SMT solving in Prolog
- Proving completeness of logic programs with the cut
- Proof methods of declarative properties of definite programs
- A 25-year perspective on logic programming. Achievements of the Italian Association for Logic Programming, GULP
- Reasoning about termination of pure Prolog programs
- Algebraic methodology and software technology. 4th international conference, AMAST '95, Montreal, Canada, July 3--7, 1995. Proceedings
- SICStus Prolog—The first 25 years
- On Completeness of Logic Programs
- Polytool: Polynomial interpretations as a basis for termination analysis of logic programs
- Strong termination of logic programs
- Algorithm = logic + control
- Classes of terminating logic programs
- On definite program answers and least Herbrand models
- Verification of logic programs
- Inferring non-suspension conditions for logic programs with dynamic scheduling
- Correctness and Completeness of Logic Programs
- Logic + control: An example
- A machine program for theorem-proving
- Proving correctness and completeness of normal programs – a declarative approach
