On Correctness and Completeness of an n Queens Program


Włodzimierz Drabent

Theory and Practice of Logic Programming 22(1), pages 37–50,  2022
Cambridge University Press

Thom Frühwirth 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, that is 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.

(keywords) logic programming; declarative programming; program completeness; program correctness specification; nonground answers
 @article{nqueens-tplp22,
author = {Drabent, W{\l}odzimierz},
doi = {10.1017/S1471068421000223},
journal = {Theory and Practice of Logic Programming},
number = 1,
pages = {37--50},
publisher = {Cambridge University Press},
title = {On Correctness and Completeness of an n {Q}ueens Program},
volume = 22,
year = 2022

Journals & Series

Publication

— authors

Włodzimierz Drabent

— status

published

— sort

article in journal

Venue

— journal

Theory and Practice of Logic Programming

— volume

22

— issue

1

— pages

37–50

— publication date

2022

URLs

original page  |  open access PDF

Identifiers

— DOI

10.1017/S1471068421000223

— print ISSN

1471-0684

— online ISSN

1475-3081

BibTeX

— BibTeX ID
nqueens-tplp22
— BibTeX category
article

Partita IVA: 01131710376 - Copyright © 2008-2022 APICe@DISI Research Group - PRIVACY