Author name cluster

Concepción Vidal

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

6 papers

2 author rows

AIJ Journal 2024 Journal Article

Syntactic ASP forgetting with forks

Felicidad Aguado
Pedro Cabalar
Jorge Fandinno
David Pearce
Gilberto Pérez
Concepción Vidal

Answer Set Programming (ASP) constitutes nowadays one of the most successful paradigms for practical Knowledge Representation and declarative problem solving. The formal analysis of ASP programs is essential for a rigorous treatment of specifications, the correct construction of solvers and the extension with other representational features. In this paper, we present a syntactic transformation, called the unfolding operator, that allows forgetting an atom in a logic program (under ASP semantics). The main advantage of unfolding is that, unlike other syntactic operators, it is always applicable and guarantees strong persistence, that is, the result preserves the same stable models with respect to any context where the forgotten atom does not occur. The price for its completeness is that the result is an expression that may contain the fork operator. Yet, we illustrate how, in some cases, the application of fork properties may allow us to reduce the fork to a logic program.

Details DOI

AIJ Journal 2022 Journal Article

A polynomial reduction of forks into logic programs

Felicidad Aguado
Pedro Cabalar
Jorge Fandinno
David Pearce
Gilberto Pérez
Concepción Vidal

In this research note we present additional results for an earlier published paper [1]. There, we studied the problem of projective strong equivalence (PSE) of logic programs, that is, checking whether two logic programs (or propositional formulas) have the same behaviour (under the stable model semantics) regardless of a common context and ignoring the effect of local auxiliary atoms. PSE is related to another problem called strongly persistent forgetting that consists in keeping a program's behaviour after removing its auxiliary atoms, something that is known to be not always possible in Answer Set Programming. In [1], we introduced a new connective ‘|’ called fork and proved that, in this extended language, it is always possible to forget auxiliary atoms, but at the price of obtaining a result containing forks. We also proved that forks can be translated back to logic programs introducing new hidden auxiliary atoms, but this translation was exponential in the worst case. In this note we provide a new polynomial translation of arbitrary forks into regular programs that allows us to prove that brave and cautious reasoning with forks has the same complexity as that of ordinary (disjunctive) logic programs and paves the way for an efficient implementation of forks. To this aim, we rely on a pair of new PSE invariance properties.

Details DOI

ECAI Conference 2020 Conference Paper

Explicit Negation in Linear-Dynamic Equilibrium Logic

Felicidad Aguado
Pedro Cabalar
Jorge Fandinno
Gilberto Pérez 0001
Concepción Vidal

In this paper, we revisit a temporal extension of Equilibrium Logic (the logical characterisation of Answer Set Programming) that introduces Linear Dynamic Logic modalities. In particular, we further incorporate to this extension (we call Linear Dynamic Equilibrium Logic) an explicit negation operator, treated as a regular logical connective. We explain several formal properties of this new extension. For instance, we prove that some temporal operators that were not inter-definable, become so if we allow the use of explicit negation. Finally, we also introduce and study a new temporal operator called “while, ” that is an implicational dual of “until” and may be useful as a basic connective for temporal logic programming.

Details

IJCAI Conference 2020 Conference Paper

Forgetting Auxiliary Atoms in Forks (Extended Abstract)

Felicidad Aguado
Pedro Cabalar
Jorge Fandinno
David Pearce
Gilberto Pérez
Concepción Vidal

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 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.

PDF Details DOI

AIJ Journal 2019 Journal Article

Forgetting auxiliary atoms in forks

Felicidad Aguado
Pedro Cabalar
Jorge Fandinno
David Pearce
Gilberto Pérez
Concepción Vidal

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.

Details DOI

JELIA Conference 2008 Conference Paper

Strongly Equivalent Temporal Logic Programs

Felicidad Aguado
Pedro Cabalar
Gilberto Pérez 0001
Concepción Vidal

Abstract This paper analyses the idea of strong equivalence for transition systems represented as logic programs under the Answer Set Programming (ASP) paradigm. To check strong equivalence, we use a linear temporal extension of Equilibrium Logic (a logical characterisation of ASP) and its monotonic basis, the intermediate logic of Here-and-There (HT). Trivially, equivalence in this temporal extension of HT provides a sufficient condition for temporal strong equivalence and, as we show in the paper, it can be transformed into a provability test into the standard Linear Temporal Logic (LTL), something that can be automatically checked using any of the LTL available provers. The paper shows an example of the potential utility of this method by detecting some redundant rules in a simple actions reasoning scenario.

Details