CertifASP: Certified Answer Set Programming

Answer Set Programming (ASP) is a declarative problem-solving paradigm, where a user needs to
write a description of the problem they want to solve, rather than having to program in a classical
programming language how to solve the problem. This problem description is then fed to a so-called
solver, which searches for a solution. Since ASP is used in practice for many critical applications,
solvers are expected to be robust algorithms that always give a correct result. Unfortunately, the
reality is different: bugs occur and even compile-errors might cause a faulty solution. This project
aims at resolving this issue by means of certifying solvers. A certifying solver produces not only a
solution to the problem but also a mathematical proof of the correctness of the produced solution. An
independent proof checker (which is easier to trust due to its simpler implementation, and which is
often even formally verified) then checks whether the proof is correct, and thus that the solution was
found using correct reasoning. Building on the success in Satisfiability Checking, this project aims at
taking the next step and also provide a proof system, with corresponding proof checker, that allows a
wide variety of ASP solving approaches to produce this kind of proofs. This newly created proof
system will be used to add proof logging to different kinds of solvers, bringing formal guarantees on
correctness to the ASP community.