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