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

Amelia Harrison
UT Austin, USA


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: