Axiomatization of Non-Recursive Aggregates in First-Order Answer Set Programming
Authors: Jorge Fandinno, Zachary Hansen, Yuliya Lierler
JAIR 2024 | Venue PDF | Archive PDF | Plain Text | LLM Run Details
| Reproducibility Variable | Result | LLM Response |
|---|---|---|
| Research Type | Theoretical | This paper contributes to the development of theoretical foundations of answer set programming. ... We prove that our characterization coincides with the ASP-Core-2 semantics for logic programs and, if we allow non-positive recursion through aggregates, it coincides with the semantics of the answer set solver CLINGO. ... We derive our Main Theorem, which states that answer sets according to the ASP-Core-2 semantics correspond to the models of the formula obtained from our translation that satisfy the mentioned axioms (Section 6). We provide rigorous and detailed proofs of our results in Appendix A. |
| Researcher Affiliation | Academia | Jorge Fandinno EMAIL Zachary Hansen EMAIL Yuliya Lierler EMAIL University of Nebraska Omaha, PKI 280D, Omaha, NE 68182 USA |
| Pseudocode | No | The paper includes examples of logic programs (Listing 1, 2, 3) and mathematical definitions and theorems, but it does not contain any structured pseudocode or algorithm blocks. |
| Open Source Code | No | The paper discusses related systems like ANTHEM and ANTHEM-P2P (Fandinno et al., 2020, 2023) in the 'Discussion and Conclusions' section, but does not provide specific access to source code for the methodology described in *this* paper. No explicit code release statement or repository link is provided for the current work. |
| Open Datasets | No | The paper presents theoretical work on the axiomatization of logic programs with aggregates. It uses illustrative examples of logic programs, such as the graph coloring problem (Listing 1, 2, 3), but these are not datasets used for empirical evaluation and no concrete access information for any datasets is provided. |
| Dataset Splits | No | The paper describes theoretical research and does not involve empirical experiments with datasets that would require training, test, or validation splits. Therefore, no dataset split information is provided. |
| Hardware Specification | No | The paper focuses on theoretical contributions to answer set programming. It does not describe any experiments that would require specific hardware specifications for execution. Therefore, no hardware details are mentioned. |
| Software Dependencies | No | The paper is theoretical and does not describe an implementation of its proposed axiomatization. While it mentions 'CLINGO (Gebser et al., 2019)', 'DLV (Adrian et al., 2018)' as solvers and 'VAMPIRE (Kov acs & Voronkov, 2013)' as a theorem prover in the context of related or future work, it does not specify versioned software dependencies for the methodology presented in this paper. |
| Experiment Setup | No | This paper presents theoretical work, primarily focusing on axiomatization and proofs of semantic equivalence. It does not describe any experimental evaluations, and therefore, no experimental setup details, hyperparameters, or training configurations are provided. |