Proving Program Correctness Using the AG Semantics: An Example with n-Queens

By
Amelia Harrison
UT Austin, USA

ABSTRACT

We show an example of how the proposal for the semantics of the subset of the input language of gringo called AG can be used as the basis for a proof of correctness of a program encoding the n-queens problem.

PDF Complete Paper: