Zachary Hansen

Zach Hansen

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.

Zachary Hansen

Answer Set Programming (ASP) is an important logic programming paradigm within the field of Knowledge Representation and Reasoning. As a concise, human-readable, declarative language, ASP is an excellent tool for developing trustworthy (especially, artificially intelligent) software systems. However, formally verifying ASP programs offers some unique challenges, such as 1. a lack of modularity (the meanings of rules are difficult to define in isolation from the enclosing program), 2. the ground-and-solve semantics (the meanings of rules are dependent on the input data with which the program is grounded), and 3. limitations of existing tools. My research agenda has been focused on addressing these three issues with the intention of making ASP verification an accessible, routine task that is regularly performed alongside program development. In this vein, I have investigated alternative semantics for ASP based on translations into the logic of here-and-there and many-sorted first-order logic. These semantics promote a modular understanding of logic programs, bypass grounding, and enable us to use automated theorem provers to automatically verify properties of programs.

Jorge Fandinno, Zachary Hansen

This paper shows that the semantics of programs with aggregates implemented by the solvers clingo and dlv can be characterized as extended First-Order formulas with intensional functions in the logic of Here-and-There. Furthermore, this characterization can be used to study the strong equivalence of programs with aggregates under either semantics. We also present a transformation that reduces the task of checking strong equivalence to reasoning in classical First-Order logic, which serves as a foundation for automating this procedure.