On Correctness and Completeness of an n Queens Program

DOI10.1017/S1471068421000223MaRDI QIDQ6063871zbMATH OpenFDO

Authors Włodzimierz Drabent

Publication date 12 December 2023

Published in Theory and Practice of Logic Programming (Search for Journal in Brave)

Copyright license Creative Commons Attribution 4.0 International

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

zbMATH Keywords

declarative programminglogic programmingnonground answersprogram completenessprogram correctnessspecification

Mathematics Subject Classification ID

Orthogonal arrays, Latin squares, Room squares (05B15) Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Combinatorial optimization (90C27)

Abstract: Thom Fr"uhwirth presented a short, elegant and efficient Prolog program for the n queens problem. However the program may be seen as rather tricky and one may not be convinced about its correctness. This paper explains the program in a declarative way, and provides proofs of its correctness and completeness. The specification and the proofs are declarative, i.e. they abstract from any operational semantics. The specification is approximate, it is unnecessary to describe the program's semantics exactly. Despite the program works on non-ground terms, this work employs the standard semantics, based on logical consequence and Herbrand interpretations. Another purpose of the paper is to present an example of precise declarative reasoning about the semantics of a logic program. Under consideration in Theory and Practice of Logic Programming (TPLP).

Recommendations

• S-semantics -- an example
• scientific article; zbMATH DE number 2085284
• On completeness of logic programs
• Proving correctness and completeness of normal programs – a declarative approach
• Correctness and completeness of logic programs

Cites work

• Correctness and completeness of logic programs
• Declarative modeling of the operational behavior of logic languages
• scientific article; zbMATH DE number 3947593 (Why is no real title available?)
• scientific article; zbMATH DE number 788036 (Why is no real title available?)
• scientific article; zbMATH DE number 870438 (Why is no real title available?)
• Logic + control: on program construction and verification
• Modular Verification of Recursive Programs
• Proof methods of declarative properties of definite programs
• Proving correctness and completeness of normal programs – a declarative approach
• S-semantics -- an example
• Strong termination of logic programs
• Verification of logic programs

This page was built for publication: On Correctness and Completeness of an n Queens Program

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6063871)