8 accepted papers
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…
This paper introduces a general framework for generate-and-test-based solvers for epistemic logic programs that can be instantiated with different generate and test programs, and it provides sufficient conditions on those programs for the correctness of the solvers built using this framework. It als…
Splitting a logic program allows us to reduce the task of computing its stable models to similar tasks for its subprograms. This can be used to increase solving performance and to prove the correctness of programs. We generalize the conditions under which this technique is applicable, by considering…
Logic programs are a popular formalism for encoding many problems relevant to knowledge representation and reasoning as well as artificial intelligence. However, for modeling rational behavior it is oftentimes required to represent the concepts of knowledge and possibility. Epistemic logic programs…
The paper presents a characterization of logic programs with aggregates based on many-sorted generalization of operator SM that refers neither to grounding nor to fixpoints. This characterization introduces new symbols for aggregate operations and aggregate elements, whose meaning is fixed by adding…
It is well-known that deciding consistency for normal answer set programs (ASP) is NP-complete, thus, as hard as the satisfaction problem for propositional logic (SAT). The exponential time hypothesis (ETH) implies that the best algorithms to solve these problems take exponential time in the worst c…
This work tackles the problem of checking strong equivalence of logic programs that may contain local auxiliary atoms, to be removed from their stable models and to be forbidden in any external context. We call this property projective strong equivalence (PSE). It has been recently proved that not a…
Epistemic logic programs constitute an extension of the stable model semantics to deal with new constructs called "subjective literals." Informally speaking, a subjective literal allows checking whether some objective literal is true in all or some stable models. However, its associated semantics ha…