S-semantics -- an example

TL;DR

This paper demonstrates how s-semantics can be used to prove correctness and completeness of a specific logic program, the n-queens problem, highlighting its applicability to reasoning about programs with nonground data.

Contribution

It provides one of the first practical applications of s-semantics to verify a non-trivial program, comparing it with traditional proof methods.

Findings

s-semantics effectively proves correctness and completeness

Comparison shows advantages over standard semantics

Application to n-queens illustrates practical utility

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 $n$ queens program. This is compared with a proof, published elsewhere, based on the standard semantics and Herbrand interpretations.