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: