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: