Hostname: page-component-cd9895bd7-dzt6s Total loading time: 0 Render date: 2024-12-25T05:04:28.714Z Has data issue: false hasContentIssue false
  • English
  • Français

On Correctness and Completeness of an n Queens Program

Published online by Cambridge University Press:  14 October 2021

WŁODZIMIERZ DRABENT Open the ORCID record for WŁODZIMIERZ DRABENT [Opens in a new window]
WŁODZIMIERZ DRABENT*
Affiliation:
Institute of Computer Science, Polish Academy of Sciences, ul. Jana Kazimierza 5, 01-248 Warszawa, Poland Department of Computer and Information Science, Linköping University S – 581 83 Linköping, Sweden (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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 programmingdeclarative programmingprogram completenessprogram correctnessspecificationnonground answers
Type
Original Article
Information
Theory and Practice of Logic Programming , Volume 22 , Issue 1 , January 2022 , pp. 37 - 50
Creative Commons
Creative Common License - CCCreative Common License - BY
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
© The Author(s), 2021. Published by Cambridge University Press

References

Apt, K. R. 1997. From Logic Programming to Prolog. International Series in Computer Science. Prentice-Hall.Google Scholar
Apt, K. R., de Boer, F. S. and Olderog, E.-R. 2009. Modular verification of recursive programs. In Languages: From Formal to Natural, Essays Dedicated to Nissim Francez. Lecture Notes in Computer Science, vol. 5533. Springer, 1–21.Google Scholar
Bezem, M. 1993. Strong termination of logic programs. Journal of Logic Programming 15, 1&2, 79–97.CrossRefGoogle Scholar
Bossi, A. and Cocco, N. 1989. Verifying correctness of logic programs. In TAPSOFT, Vol. 2, Díaz, J. and Orejas, F., Eds. Lecture Notes in Computer Science, vol. 352. Springer, 96–110.Google Scholar
Clark, K. L. 1979. Predicate logic as computational formalism. Tech. Rep. 79/59, Imperial College, London. December.Google Scholar
Deransart, P. 1993. Proof methods of declarative properties of definite programs. Theoretical Computer Science 118, 2, 99–166.CrossRefGoogle Scholar
Deransart, P. and Małuszyński, J. 1993. A Grammatical View of Logic Programming. The MIT Press.Google Scholar
Drabent, W. 2016. Correctness and completeness of logic programs. ACM Transactions on Computational Logic 17, 3, 18:1–18:32.Google Scholar
Drabent, W. 2018. Logic + control: On program construction and verification. Theory and Practice of Logic Programming 18, 1, 1–29.Google Scholar
Drabent, W. 2019. On correctness of an n queens program. CoRR abs/1909.07479. http://arxiv.org/abs/1909.07479. A preliminary version of the current paper, with extended introductory sections.Google Scholar
Drabent, W. 2020. S-semantics – an example. CoRR abs/2006.06077. http://arxiv.org/abs/2006.06077. Presented at LOPSTR 2021.Google Scholar
Drabent, W. 2021. A note on occur-check. In Proceedings 37th International Conference on Logic Programming (Technical Communications), Formisano, A. et al Eds. Electronic Proceedings in Theoretical Computer Science, vol 345. Open Publishing Association, 54–67.Google Scholar
Drabent, W. and Miłkowska, M. 2005. Proving correctness and completeness of normal programs – a declarative approach. Theory and Practice of Logic Programming 5, 6, 669–711.CrossRefGoogle Scholar
Falaschi, M., Levi, G., Palamidessi, C. and Martelli, M. 1989. Declarative modeling of the operational behavior of logic languages. Theoretical Computer Science 69, 3, 289–318.CrossRefGoogle Scholar
Frühwirth, T. 1991. nqueens. A post in comp.lang.prolog. 1991-03-08. Also in (Sterling and Shapiro 1994, Section 4.1, Exercise (v)).Google Scholar
Pedreschi, D. and Ruggieri, S. 1999. Verification of logic programs. Journal of Logic Programming 39, 1–3, 125–176.CrossRefGoogle Scholar
Shapiro, E. 1983. Algorithmic Program Debugging. The MIT Press.Google Scholar
Sterling, L. and Shapiro, E. 1994. The Art of Prolog, 2 ed. The, MIT Press. Google Scholar