@article{CabalarFandinoSchaubetal.2019,
  author    = {Cabalar, Pedro and Fandi{\~n}o, 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}
}
@article{AguadoCabalarFandinoetal.2019,
  author    = {Aguado, Felicidad and Cabalar, Pedro and Fandi{\~n}o, 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}
}