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

Complete Paper: HERE

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.