Tools and Methodologies for Verifying Answer Set Programs
This work addresses the need for formal verification in ASP to enhance reliability in AI applications, though it appears incremental as it builds on existing ASP foundations.
The research tackles the problem of verifying Answer Set Programs (ASP) to support explainable and trustworthy AI, by extending the theory and tools for verification.
Answer Set Programming (ASP) is a powerful declarative programming paradigm commonly used for solving challenging search and optimization problems. The modeling languages of ASP are supported by sophisticated solving algorithms (solvers) that make the solution search efficient while enabling the programmer to model the problem at a high level of abstraction. As an approach to Knowledge Representation and Reasoning, ASP benefits from its simplicity, conciseness and rigorously defined semantics. These characteristics make ASP a straightforward way to develop formally verifiable programs. In the context of artificial intelligence (AI), the clarity of ASP programs lends itself to the construction of explainable, trustworthy AI. In support of these goals, my research is concerned with extending the theory and tools supporting the verification of ASP progams.