51ÉçÇø

Members

51ÉçÇø (UNO) Dr. Jorge Fandinno Zachary Hansen

Collaborators Dr. Vladimir Lifschitz, UT Austin Dr. Torsten Schaub, University of Potsdam Tobias Stolzmann, University of Potsdam Nathan Temple, UT Austin

Project Summary

This project encompasses a number of research ventures falling under the umbrella topic of formal verification of answer set programs. These can be roughly divided into three interrelated categories. The first is the task of developing semantics for advanced ASP language constructs (aggregates and conditional literals) that do not refer to grounding. This allows ASP practitioners to reason formally about the correctness of their programs without reference to a particular input. The second category seeks to enhance modularity in Answer Set programs. From a formal verification perspective, it is desirable to reason about program components in isolation. This allows proofs of correctness for sub-programs to be recycled, and simplifies the task of verifying extended programs. Finally, the ability to automatically verify programs will make widespread adoption of formal methods for ASP development much more palatable. Details of our progress in this direction can be found on the Anthem-P2P software system linked below.

This work was partially supported by the Research Development Program (Fall 2020) from the Office of Research and Creative Activity (UNO).

Software

Publications

• - Jorge Fandinno, Zachary Hansen, Yuliya Lierler, Vladimir Lifschitz, and Nathan Temple - ICLP - 2023
• - Jorge Fandinno, Zachary Hansen and Yuliya Lierler - LPNMR - 2022
• - Zachary Hansen and Yuliya Lierler - LPNMR - 2022
• - Jorge Fandinno, Zach Hansen and Yuliya Lierler - AAAI - 2022

Presentations

• Semantics for Conditional Literals via the SM Operator - Zach Hansen - LPNMR - 2022
• Arguing Correctness of ASP Programs with Aggregates - Zach Hansen - LPNMR - 2022
• - Zach Hansen - ICLP - 2022
• Axiomatization of Aggregates In Answer Set Programs - Zach Hansen - AAAI - 2022