S-semantics -- an example
This work addresses a gap in the literature for logic programming researchers by providing a concrete example, though it is incremental as it applies an existing semantics to a known program.
The paper tackles the lack of published examples for applying s-semantics to reason about specific programs by using it to prove correctness and completeness of Frühwirth's n queens program, comparing this with a proof based on standard semantics and Herbrand interpretations.
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ühwirth's $n$ queens program. This is compared with a proof, published elsewhere, based on the standard semantics and Herbrand interpretations.