S-semantics -- an example
Abstract
The s-semantics makes it possible to explicitly deal with variables in program answers. So it seems suitable for programs using nonground data structures, like open lists. However it is difficult to find published examples of using the s-semantics to reason about particular programs. Here we apply s-semantics to prove correctness and completeness of Fr\"uhwirth's queens program. This is compared with a proof, published elsewhere, based on the standard semantics and Herbrand interpretations.
Cite
@article{arxiv.2006.06077,
title = {S-semantics -- an example},
author = {Włodzimierz Drabent},
journal= {arXiv preprint arXiv:2006.06077},
year = {2021}
}
Comments
Pre-proceedings paper presented at the 31st International Symposium on Logic-Based Program Synthesis and Transformation (LOPSTR 2021), Tallinn, Estonia, and Virtual, September 7-8, 2021 (arXiv:2107.10160). 15 pages, 1 figure. This version -- small modifications