@misc{AguadoCabalarFandinnoetal.2019, author = {Aguado, Felicidad and Cabalar, Pedro and Fandinno, Jorge and Pearce, David and Perez, Gilberto and Vidal, Concepcion}, title = {Revisiting explicit negation in answer set programming}, series = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe}, journal = {Postprints der Universit{\"a}t Potsdam : Mathematisch-Naturwissenschaftliche Reihe}, number = {1104}, issn = {1866-8372}, doi = {10.25932/publishup-46969}, url = {http://nbn-resolving.de/urn:nbn:de:kobv:517-opus4-469697}, pages = {908 -- 924}, year = {2019}, abstract = {A common feature in Answer Set Programming is the use of a second negation, stronger than default negation and sometimes called explicit, strong or classical negation. This explicit negation is normally used in front of atoms, rather than allowing its use as a regular operator. In this paper we consider the arbitrary combination of explicit negation with nested expressions, as those defined by Lifschitz, Tang and Turner. We extend the concept of reduct for this new syntax and then prove that it can be captured by an extension of Equilibrium Logic with this second negation. We study some properties of this variant and compare to the already known combination of Equilibrium Logic with Nelson's strong negation.}, language = {en} } @article{AguadoCabalarFandinnoetal.2019, author = {Aguado, Felicidad and Cabalar, Pedro and Fandinno, Jorge and Pearce, David and Perez, Gilberto and Vidal, Concepcion}, title = {Forgetting auxiliary atoms in forks}, series = {Artificial intelligence}, volume = {275}, journal = {Artificial intelligence}, publisher = {Elsevier}, address = {Amsterdam}, issn = {0004-3702}, doi = {10.1016/j.artint.2019.07.005}, pages = {575 -- 601}, year = {2019}, abstract = {In this work we tackle 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 any logic program containing auxiliary atoms can be reformulated, under PSE, as another logic program or formula without them - this is known as strongly persistent forgetting. In this paper, we introduce a conservative extension of Equilibrium Logic and its monotonic basis, the logic of Here-and-There, in which we deal with a new connective '|' we call fork. We provide a semantic characterisation of PSE for forks and use it to show that, in this extension, it is always possible to forget auxiliary atoms under strong persistence. We further define when the obtained fork is representable as a regular formula.}, language = {en} } @article{AguadoCabalarFandinoetal.2019, author = {Aguado, Felicidad and Cabalar, Pedro and Fandi{\~n}o, Jorge and Pearce, David and Perez, Gilberto and Vidal-Peracho, Concepcion}, title = {Revisiting Explicit Negation in Answer Set Programming}, series = {Theory and practice of logic programming}, volume = {19}, journal = {Theory and practice of logic programming}, number = {5-6}, publisher = {Cambridge Univ. Press}, address = {New York}, issn = {1471-0684}, doi = {10.1017/S1471068419000267}, pages = {908 -- 924}, year = {2019}, language = {en} } @misc{BosserCabalarDieguezetal.2018, author = {Bosser, Anne-Gwenn and Cabalar, Pedro and Dieguez, Martin and Schaub, Torsten H.}, title = {Introducing temporal stable models for linear dynamic logic}, series = {16th International Conference on Principles of Knowledge Representation and Reasoning}, journal = {16th International Conference on Principles of Knowledge Representation and Reasoning}, publisher = {ASSOC Association for the Advancement of Artificial Intelligence}, address = {Palo Alto}, pages = {12 -- 21}, year = {2018}, abstract = {We propose a new temporal extension of the logic of Here-and-There (HT) and its equilibria obtained by combining it with dynamic logic over (linear) traces. Unlike previous temporal extensions of HT based on linear temporal logic, the dynamic logic features allow us to reason about the composition of actions. For instance, this can be used to exercise fine grained control when planning in robotics, as exemplified by GOLOG. In this paper, we lay the foundations of our approach, and refer to it as Linear Dynamic Equilibrium Logic, or simply DEL. We start by developing the formal framework of DEL and provide relevant characteristic results. Among them, we elaborate upon the relationships to traditional linear dynamic logic and previous temporal extensions of HT.}, language = {en} } @article{CabalarDieguezSchaubetal.2020, author = {Cabalar, Pedro and Dieguez, Martin and Schaub, Torsten H. and Schuhmann, Anna}, title = {Towards metric temporal answer set programming}, series = {Theory and practice of logic programming}, volume = {20}, journal = {Theory and practice of logic programming}, number = {5}, publisher = {Cambridge Univ. Press}, address = {Cambridge [u.a.]}, issn = {1471-0684}, doi = {10.1017/S1471068420000307}, pages = {783 -- 798}, year = {2020}, abstract = {We elaborate upon the theoretical foundations of a metric temporal extension of Answer Set Programming. In analogy to previous extensions of ASP with constructs from Linear Temporal and Dynamic Logic, we accomplish this in the setting of the logic of Here-and-There and its non-monotonic extension, called Equilibrium Logic. More precisely, we develop our logic on the same semantic underpinnings as its predecessors and thus use a simple time domain of bounded time steps. This allows us to compare all variants in a uniform framework and ultimately combine them in a common implementation.}, language = {en} } @article{CabalarFandinnoGareaetal.2020, author = {Cabalar, Pedro and Fandinno, Jorge and Garea, Javier and Romero, Javier and Schaub, Torsten H.}, title = {Eclingo}, series = {Theory and practice of logic programming}, volume = {20}, journal = {Theory and practice of logic programming}, number = {6}, publisher = {Cambridge Univ. Press}, address = {New York}, issn = {1471-0684}, doi = {10.1017/S1471068420000228}, pages = {834 -- 847}, year = {2020}, abstract = {We describe eclingo, a solver for epistemic logic programs under Gelfond 1991 semantics built upon the Answer Set Programming system clingo. The input language of eclingo uses the syntax extension capabilities of clingo to define subjective literals that, as usual in epistemic logic programs, allow for checking the truth of a regular literal in all or in some of the answer sets of a program. The eclingo solving process follows a guess and check strategy. It first generates potential truth values for subjective literals and, in a second step, it checks the obtained result with respect to the cautious and brave consequences of the program. This process is implemented using the multi-shot functionalities of clingo. We have also implemented some optimisations, aiming at reducing the search space and, therefore, increasing eclingo 's efficiency in some scenarios. Finally, we compare the efficiency of eclingo with two state-of-the-art solvers for epistemic logic programs on a pair of benchmark scenarios and show that eclingo generally outperforms their obtained results.}, language = {en} } @article{CabalarFandinnoLierler2020, author = {Cabalar, Pedro and Fandinno, Jorge and Lierler, Yuliya}, title = {Modular Answer Set Programming as a formal specification language}, series = {Theory and practice of logic programming}, volume = {20}, journal = {Theory and practice of logic programming}, number = {5}, publisher = {Cambridge University Press}, address = {New York}, issn = {1471-0684}, doi = {10.1017/S1471068420000265}, pages = {767 -- 782}, year = {2020}, abstract = {In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining aformal proofshowing that the answer sets of a given (non-ground) logic programPcorrectly correspond to the solutions to the problem encoded byP, regardless of the problem instance. To this aim, we use a formal specification language based on ASP modules, so that each module can be proved to capture some informal aspect of the problem in an isolated way. This specification language relies on a novel definition of (possibly nested, first order)program modulesthat may incorporate local hidden atoms at different levels. Then,verifyingthe logic programPamounts to prove some kind of equivalence betweenPand its modular specification.}, language = {en} } @article{CabalarFandinnoSchaubetal.2019, author = {Cabalar, Pedro and Fandinno, Jorge and Schaub, Torsten H. and Schellhorn, Sebastian}, title = {Gelfond-Zhang aggregates as propositional formulas}, series = {Artificial intelligence}, volume = {274}, journal = {Artificial intelligence}, publisher = {Elsevier}, address = {Amsterdam}, issn = {0004-3702}, doi = {10.1016/j.artint.2018.10.007}, pages = {26 -- 43}, year = {2019}, abstract = {Answer Set Programming (ASP) has become a popular and widespread paradigm for practical Knowledge Representation thanks to its expressiveness and the available enhancements of its input language. One of such enhancements is the use of aggregates, for which different semantic proposals have been made. In this paper, we show that any ASP aggregate interpreted under Gelfond and Zhang's (GZ) semantics can be replaced (under strong equivalence) by a propositional formula. Restricted to the original GZ syntax, the resulting formula is reducible to a disjunction of conjunctions of literals but the formulation is still applicable even when the syntax is extended to allow for arbitrary formulas (including nested aggregates) in the condition. Once GZ-aggregates are represented as formulas, we establish a formal comparison (in terms of the logic of Here-and-There) to Ferraris' (F) aggregates, which are defined by a different formula translation involving nested implications. In particular, we prove that if we replace an F-aggregate by a GZ-aggregate in a rule head, we do not lose answer sets (although more can be gained). This extends the previously known result that the opposite happens in rule bodies, i.e., replacing a GZ-aggregate by an F-aggregate in the body may yield more answer sets. Finally, we characterize a class of aggregates for which GZ- and F-semantics coincide.}, language = {en} } @misc{CabalarFandinnoSchaubetal.2019, author = {Cabalar, Pedro and Fandinno, Jorge and Schaub, Torsten H. and Schellhorn, Sebastian}, title = {Lower Bound Founded Logic of Here-and-There}, series = {Logics in Artificial Intelligence}, volume = {11468}, journal = {Logics in Artificial Intelligence}, publisher = {Springer}, address = {Cham}, isbn = {978-3-030-19570-0}, issn = {0302-9743}, doi = {10.1007/978-3-030-19570-0_34}, pages = {509 -- 525}, year = {2019}, abstract = {A distinguishing feature of Answer Set Programming is that all atoms belonging to a stable model must be founded. That is, an atom must not only be true but provably true. This can be made precise by means of the constructive logic of Here-and-There, whose equilibrium models correspond to stable models. One way of looking at foundedness is to regard Boolean truth values as ordered by letting true be greater than false. Then, each Boolean variable takes the smallest truth value that can be proven for it. This idea was generalized by Aziz to ordered domains and applied to constraint satisfaction problems. As before, the idea is that a, say integer, variable gets only assigned to the smallest integer that can be justified. In this paper, we present a logical reconstruction of Aziz' idea in the setting of the logic of Here-and-There. More precisely, we start by defining the logic of Here-and-There with lower bound founded variables along with its equilibrium models and elaborate upon its formal properties. Finally, we compare our approach with related ones and sketch future work.}, language = {en} } @article{CabalarKaminskiSchaubetal.2018, author = {Cabalar, Pedro and Kaminski, Roland and Schaub, Torsten H. and Schuhmann, Anna}, title = {Temporal answer set programming on finite traces}, series = {Theory and practice of logic programming}, volume = {18}, journal = {Theory and practice of logic programming}, number = {3-4}, publisher = {Cambridge Univ. Press}, address = {New York}, issn = {1471-0684}, doi = {10.1017/S1471068418000297}, pages = {406 -- 420}, year = {2018}, abstract = {In this paper, we introduce an alternative approach to Temporal Answer Set Programming that relies on a variation of Temporal Equilibrium Logic (TEL) for finite traces. This approach allows us to even out the expressiveness of TEL over infinite traces with the computational capacity of (incremental) Answer Set Programming (ASP). Also, we argue that finite traces are more natural when reasoning about action and change. As a result, our approach is readily implementable via multi-shot ASP systems and benefits from an extension of ASP's full-fledged input language with temporal operators. This includes future as well as past operators whose combination offers a rich temporal modeling language. For computation, we identify the class of temporal logic programs and prove that it constitutes a normal form for our approach. Finally, we outline two implementations, a generic one and an extension of the ASP system clingo. Under consideration for publication in Theory and Practice of Logic Programming (TPLP)}, language = {en} }