![51社区 logo](/_files/images/uno-icon-50.png"/){kind=icon}
![51社区 logo](/_files/images/uno-icon-50-noline.png"/){kind=icon}
Members
|
51社区 (UNO)
|
Collaborators
|
Table of Contents
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
- Recursive Aggregates as Intensional Functions in Answer Set Programming: Semantics and Strong Equivalence - Jorge Fandinno and Zachary Hansen - AAAI - 2025
- SM-based Semantics for Answer Set Programs Containing Conditional Literals and Arithmetic - Zachary Hansen and Yuliya Lierler - PADL - 2025
- - Jorge Fandinno, Vladimir Lifschitz & Nathan Temple - TPLP - 2024
- Axiomatization of Non-Recursive Aggregates in First-Order Answer Set Programming - Jorge Fandinno, Zachary Hansen and Yuliya Lierler - JAIR - 2024
- - Jorge Fandinno & Vladimir Lifschitz - LPNMR - 2024
- - Jorge Fandinno & Vladimir Lifschitz - 2023
- - Jorge Fandinno & Yuliya Lierler - AAAI - 2023
- - Jorge Fandinno & Vladimir Lifschitz - KR - 2023
- External Behavior of a Logic Program and Verification of Refactoring - Jorge Fandinno, Zachary Hansen, Yuliya Lierler, Vladimir Lifschitz, and Nathan Temple - TPLP - 2023
- - Jorge Fandinno & Vladimir Lifschitz - TPLP - 2023
- Arguing Correctness of ASP Programs with Aggregates - Jorge Fandinno, Zachary Hansen and Yuliya Lierler - LPNMR - 2022
- Semantics for Conditional Literals via the SM Operator - Zachary Hansen and Yuliya Lierler - LPNMR - 2022
- Axiomatization of Aggregates in Answer Set Programming - Jorge Fandinno, Zach Hansen and Yuliya Lierler - AAAI - 2022
Presentations & Tutorials
- Formal Methods in Answer Set Programming - Vladimir Lifschitz - 2024
- 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