On correctness and completeness of an n queens program

Autor:	Drabent, Włodzimierz
Rok vydání:	2021
Předmět:	Computer Science - Logic in Computer Science Computer Science - Programming Languages Computer Science - Software Engineering 68N17 (Primary) 68N30 (Secondary) D.1.6 D.2.4 F.3.1
Zdroj:	Theory and Practice of Logic Programming, Volume 22 , Issue 1 , January 2022 , pp. 37 - 50
Druh dokumentu:	Working Paper
DOI:	10.1017/S1471068421000223
Popis:	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). Comment: Under consideration in Theory and Practice of Logic Programming (TPLP). 13 pages, 1 figure. A re-worked version of arXiv:1909.07479
Databáze:	arXiv
Externí odkaz:	http://arxiv.org/abs/2108.08079 Zobrazit plný text záznamu View this record from Arxiv