Arrow Research search

Author name cluster

Pedro Cabalar

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.

37 papers
2 author rows

Possible papers

37

AAMAS Conference 2025 Conference Paper

Tackling Temporal Deontic Challenges with Equilibrium Logic

  • Davide Soldà
  • Pedro Cabalar
  • Agata Ciabattoni
  • Emery Neufeld

Combining temporal reasoning with normative requirements presents significant challenges. In this paper, we tackle the most relevant challenges in the literature from a computational perspective, using Answer Set Programming (ASP). We integrate Temporal Equilibrium Logic, the foundation of Temporal ASP, with Deontic Equilibrium Logic with Explicit Negation, to reason about norms in a temporal context. Our approach is validated by: (i) addressing key benchmarks for temporal normative systems, providing (ii) a normal form reduction that enables the use of existing tools, and (iii) a polynomial LTL reduction for a relevant logic fragment.

PDF

KR Conference 2024 Conference Paper

Contracted Temporal Equilibrium Logic

  • Pedro Cabalar
  • Thomas Eiter
  • Davide Soldà

The stable model semantics of logic programs has been characterized by Equilibrium Logic, which is a non-monotonic formalism that selects models from the (monotonic) intermediate logic of Here-and-There. It provides stable models for arbitrary propositional formulas and has been fruitfully extended to different modal languages. Among them are theories in the syntax of Linear-Time Temporal Logic (LTL), giving rise to Temporal Equilibrium logic (TEL) based on Temporal Here-and-There (THT). In TEL, models are selected that minimize truth among THT traces of the same length. In this paper, we consider a selection that in addition may reduce the number of transitions in a trace, intuitively forming a contraction of it. We thus introduce contracted THT and contracted TEL on top of a model selection on a logical basis. The resulting c-stable models can be viewed as stable models in TEL that can not be summarized into a smaller trace. We illustrate contraction on several examples related to logic programming and explore several properties, like the relation to TEL and LTL, and in particular the connection to the LTL property of stuttering.

PDF Details DOI

JELIA Conference 2023 Conference Paper

Deontic Equilibrium Logic with eXplicit Negation

  • Pedro Cabalar
  • Agata Ciabattoni
  • Leendert W. N. van der Torre

Abstract Equilibrium logic is a logical characterization of Answer Set Programming (ASP). We introduce Deontic Equilibrium Logic with eXplicit negation (DELX), its extension for normative reasoning. In contrast to modal approaches, DELX utilizes a normal form that restricts deontic operators solely to atoms. We establish that any theories in DELX can be reduced to ASP, and demonstrate the efficacy of this minimalist approach in addressing key challenges from the defeasible deontic logic literature.

Details

JELIA Conference 2023 Conference Paper

Logic, Accountability and Design: Extended Abstract

  • Pedro Cabalar
  • David Pearce 0001

Abstract This note is a contribution to the methodology of applied, computational logics in light of their potential role in securing the accountability of Artificial Intelligence (AI) systems.

Details

JELIA Conference 2023 Conference Paper

Past-Present Temporal Programs over Finite Traces

  • Pedro Cabalar
  • Martín Diéguez
  • François Laferrière
  • Torsten Schaub

Abstract Extensions of Answer Set Programming with language constructs from temporal logics, such as temporal equilibrium logic over finite traces ( \(\text {TEL}_{\! f}\) ), provide an expressive computational framework for modeling dynamic applications. In this paper, we study the so-called past-present syntactic subclass, which consists of a set of logic programming rules whose body references to the past and head to the present. Such restriction ensures that the past remains independent of the future, which is the case in most dynamic domains. We extend the definitions of completion and loop formulas to the case of past-present formulas, which allows for capturing the temporal stable models of past-present temporal programs by means of an \(\text {LTL}_{\! f}\) expression.

Details

KR Conference 2020 Conference Paper

A Uniform Treatment of Aggregates and Constraints in Hybrid ASP

  • Pedro Cabalar
  • Jorge Fandinno
  • Torsten Schaub
  • Philipp Wanko

Characterizing hybrid ASP solving in a generic way is difficult since one needs to abstract from specific theories. Inspired by lazy SMT solving, this is usually addressed by treating theory atoms as opaque. Unlike this, we propose a slightly more transparent approach that includes an abstract notion of a term. Rather than imposing a syntax on terms, we keep them abstract by stipulating only some basic properties. With this, we further develop a semantic framework for hybrid ASP solving and provide aggregate functions for theory variables that adhere to different semantic principles, show that they generalize existing aggregate semantics in ASP and how we can rely on off-the-shelf hybrid solvers for implementation.

PDF Details DOI

ECAI Conference 2020 Conference Paper

An ASP Semantics for Constraints Involving Conditional Aggregates

  • Pedro Cabalar
  • Jorge Fandinno
  • Torsten Schaub
  • Philipp Wanko

We elaborate upon the formal foundations of hybrid Answer Set Programming (ASP) and extend its underlying logical framework with aggregate functions over constraint values and variables. This is achieved by introducing the construct of conditional expressions, which allow for considering two alternatives while evaluating constraints. Which alternative is considered is interpretation-dependent and chosen according to an associated condition. We put some emphasis on logic programs with linear constraints and show how common ASP aggregates can be regarded as particular cases of so-called conditional linear constraints. Finally, we introduce a polynomial-size, modular and faithful translation from our framework into regular (condition-free) Constraint ASP, outlining an implementation of conditional aggregates on top of existing hybrid ASP solvers.

Details

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

ECAI Conference 2020 Conference Paper

Implementing Dynamic Answer Set Programming over Finite Traces

  • Pedro Cabalar
  • Martín Diéguez
  • Torsten Schaub
  • François Laferrière

We introduce an implementation of an extension of Answer Set Programming (ASP) with language constructs from dynamic (and temporal) logic that provides an expressive computational framework for modeling dynamic applications. Starting from logical foundations, provided by dynamic and temporal equilibrium logics over finite linear traces, we develop a translation of dynamic formulas into temporal logic programs. This provides us with a normal form result establishing the strong equivalence of formulas in different logics. Our translation relies on the introduction of auxiliary atoms to guarantee polynomial space complexity and to provide an embedding that is doomed to be impossible over the same language. Finally, the reduction of dynamic formulas to temporal logic programs allows us to extend ASP with both approaches in a uniform way and to implement both extensions via temporal ASP solvers such as telingo.

Details

IJCAI Conference 2020 Conference Paper

On the Splitting Property for Epistemic Logic Programs (Extended Abstract)

  • Pedro Cabalar
  • Jorge Fandinno
  • Luis Fariñas del Cerro

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 has proved to be non-trivial, since the truth of subjective literals may interfere with the set of stable models it is supposed to query. As a consequence, no clear agreement has been reached and different semantic proposals have been made in the literature. In this paper, we review an extension of the well-known splitting property for logic programs to the epistemic case. This "epistemic splitting property" is defined as a general condition that can be checked on any arbitrary epistemic semantics. Its satisfaction has desirable consequences both in the representation of conformant planning problems and in the encoding of the so-called subjective constraints.

PDF Details DOI

KR Conference 2020 Conference Paper

Spatial Reasoning about String Loops and Holes in Temporal ASP

  • Pedro Cabalar
  • Paulo E. Santos

This paper introduces a new formalism for the automated solution of spatial scenarios involving strings and holed objects. In particular, we revisit a previous formalisation that allows string loops to be treated as holes, but make a substantial modification by removing a previous limitation that prevented a string to cross its own loops. The formalisation introduced in the present paper relies on string segments as basic entities and achieves a greater degree of elaboration tolerance by using inertia to describe those parts of the physical scenario that are unaffected by a given action. As a representation language, we have used Temporal Answer Set Programming since it provides a simple and natural way to deal with time and inertia while, at the same time, it is accompanied by the automated tool 'telingo' that allows a systematic testing of the effects of any sequence of actions. As an illustrative example, we have studied the African Ring puzzle, a problem involving loops crossed by a unique string, and provided the first formalisation of its solution, to the best of our knowledge.

PDF Details DOI

TIME Conference 2020 Conference Paper

Temporal Modalities in Answer Set Programming (Invited Talk)

  • Pedro Cabalar

Based on the answer set (or stable model) semantics for logic programs, Answer Set Programming (ASP) has become one of the most successful paradigms for practical Knowledge Representation and problem solving. Although ASP is naturally equipped for solving static combinatorial problems up to NP complexity (or ΣP2 in the disjunctive case) its application to temporal scenarios has been frequent since its very beginning, partly due to its early use for reasoning about actions and change. Temporal problems normally suppose an extra challenge for ASP for several reasons. On the one hand, they normally raise the complexity (in the case of classical planning, for instance, it becomes PSPACE-complete), although this is usually accounted for by making repeated calls to an ASP solver. On the other hand, temporal scenarios also pose a representational challenge, since the basic ASP language does not support temporal expressions. To fill this representational gap, a temporal extension of ASP called Temporal Equilibrium Logic (TEL) was proposed in and extensively studied later. This formalism constitutes a modal, linear-time extension of Equilibrium Logic which, in its turn, is a complete logical characterisation of (standard) ASP based on the intermediate logic of Here-and-There (HT). As a result, TEL is an expressive non-monotonic modal logic that shares the syntax of Linear-Time Temporal Logic (LTL) but interprets temporal formulas under a non-monotonic semantics that properly extends stable models.

Details

JELIA Conference 2019 Conference Paper

Lower Bound Founded Logic of Here-and-There

  • Pedro Cabalar
  • Jorge Fandinno
  • Torsten Schaub
  • Sebastian Schellhorn

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.

Details

KR Conference 2018 Conference Paper

Introducing Temporal Stable Models for Linear Dynamic Logic

  • Anne-Gwenn Bosser
  • Pedro Cabalar
  • Martín Diéguez
  • Torsten Schaub

We propose a new temporal extension of the logic of Hereand-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.

IJCAI Conference 2016 Conference Paper

An ASP Semantics for Default Reasoning with Constraints

  • Pedro Cabalar
  • Roland Kaminski
  • Max Ostrowski
  • Torsten Schaub

We introduce the logic of Here-and-There with Constraints in order to capture constraint theories in the non-monotonic setting known from Answer Set Programming (ASP). This allows for assigning default values to constraint variables or to leave them undefined. Also, it provides us with a semantic framework integrating ASP and Constraint Processing in a uniform way. We put some emphasis on logic programs dealing with linear constraints on integer variables, where we further introduce a directional assignment operator. We elaborate upon the formal relation and implementation of these programs in terms of Constraint ASP, sketching an existing system.

PDF Details

JELIA Conference 2014 Conference Paper

A Complexity Assessment for Queries Involving Sufficient and Necessary Causes

  • Pedro Cabalar
  • Jorge Fandinno
  • Michael Fink 0001

Abstract In this work, we revisit a recently proposed multi-valued semantics for logic programs where each true atom in a stable model is associated with a set of expressions (or causal justifications) involving rule labels. For positive programs, these causal justifications correspond to the possible alternative proofs of the atom that further satisfy some kind of minimality or lack of redundancy. This information can be queried for different purposes such as debugging, program design, diagnosis or causal explanation. Unfortunately, in the worst case, the number of causal justifications for an atom can be exponential with respect to the program size, so that computing the complete causal model may become intractable in the general case. However, we may instead just be interested in querying whether some particular set of rules are involved in the atom derivation, either as a sufficient cause (they provide one of the alternative proofs) or as a necessary cause (they are mandatorily used in all proofs). In this paper, we formally define sufficient and necessary causation for this setting and provide precise complexity characterizations of the associated decision problems, showing that they remain within the first two levels of the polynomial hierarchy.

Details

JELIA Conference 2014 Conference Paper

A Free Logic for Stable Models with Partial Intensional Functions

  • Pedro Cabalar
  • Luis Fariñas del Cerro
  • David Pearce 0001
  • Agustín Valverde

Abstract In this paper we provide a new logical characterisation of stable models with partial functions that consists in a free-logic extension of Quantified Equilibrium Logic (QEL). In so-called “free” logics, terms may denote objects that are outside the domain of quantification, something that can be immediately used to capture partial functions. We show that this feature can be naturally accommodated in the monotonic basis of QEL (the logic of Quantified Here-and-There, QHT) by allowing variable quantification domains that depend on the world where the formula is being interpreted. The paper provides two main contributions: (i) a correspondence with Cabalar’s semantics for stable models with partial functions; and (ii) a Gentzen system for free QHT, the monotonic basis of free QEL.

Details

KR Conference 2014 Short Paper

Strong Equivalence of Non-monotonic Temporal Theories

  • Pedro Cabalar
  • Martín Diéguez

properties of a given dynamic system. For instance, questions such as “is there a reachable state in which both p and q are false? ” or “can we show that whenever p is true it will remain so forever? ” can be answered by an analytical inspection of our simple program, but cannot be solved in an automated way. To overcome these limitations, (Aguado et al. 2013) proposed a temporal extension of Equilibrium Logic (Pearce 1996), the best-known logical formalisation of ASP. This extension, which received the name of Temporal Equilibrium Logic (TEL), is defined as follows. First, it extends the monotonic basis of Equilibrium Logic, the intermediate logic of Here-and-There (HT) (Heyting 1930), by introducing the full syntax of the well-known Linear-time Temporal Logic (LTL) (Pnueli 1977). The result of this combination is called Temporal Here-and-There (THT). Then, a selection criterion on THT models is imposed, obtaining nonmonotonicity in this way. As a result, TEL constitutes a full non-monotonic temporal logic that allows a proper definition of temporal stable models for any arbitrary theory in the syntax of LTL. For instance, the ASP program (1)-(4) would be represented in TEL as: In this paper we solve the following open problem: we prove that equivalence in the logic of Temporal Here-and-There (THT) is not only a sufficient, but also a necessary condition for strong equivalence of two Temporal Equilibrium Logic (TEL) theories. This result has allowed constructing a tool, ABSTEM, that can be used to check different types of equivalence between two arbitrary temporal theories. More importantly, when the theories are not THT-equivalent, the system provides a context theory that makes them behave differently, together with a Büchi automaton showing the temporal stable models that arise from that difference.

LOPSTR Conference 2011 Conference Paper

Automata-Based Computation of Temporal Equilibrium Models

  • Pedro Cabalar
  • Stéphane Demri

Abstract Temporal Equilibrium Logic (TEL) is a formalism for temporal logic programming that generalizes the paradigm of Answer Set Programming (ASP) introducing modal temporal operators from standard Linear-time Temporal Logic (LTL). In this paper we solve some problems that remained open for TEL like decidability, bounds for computational complexity as well as computation of temporal equilibrium models for arbitrary theories. We propose a method for the latter that consists in building a Büchi automaton that accepts exactly the temporal equilibrium models of a given theory, providing an automata-based decision procedure and illustrating the ω -regularity of such sets. We show that TEL satisfiability can be solved in exponential space and it is hard for polynomial space. Finally, given two theories, we provide a decision procedure to check if they have the same temporal equilibrium models.

Details

JELIA Conference 2010 Conference Paper

A Normal Form for Linear Temporal Equilibrium Logic

  • Pedro Cabalar

Abstract In previous work, the so-called Temporal Equilibrium Logic (TEL) was introduced. This formalism provides an extension of the Answer Set semantics for logic programs to arbitrary theories in the syntax of Linear Temporal Logic. It has already been shown that, in the non-temporal case, arbitrary propositional theories can always be reduced to logic program rules (with disjunction and negation in the head) independently on the context. That is, logic programs constitute a normal form for the non-temporal case. In this paper we show that TEL can be similarly reduced to a normal form consisting of a set of implications (embraced by a necessity operator) quite close to logic program rules. This normal form may be useful both for a practical implementation of TEL and a simpler analysis of theoretical problems.

Details

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

KR Conference 2006 Conference Paper

Logical Foundations of Well-Founded Semantics

  • Pedro Cabalar
  • Sergei Odintsov
  • David Pearce

We propose a solution to a long-standing problem in the foundations of well-founded semantics (WFS) for logic programs. The problem addressed is this: which (non-modal) logic can be considered adequate for well-founded semantics in the sense that its minimal models (appropriately defined) coincide with the partial stable models of a logic program? We approach this problem by identifying the HT² frames previously proposed by Cabalar to capture WFS as structures of a kind used by Došen to characterise a family of logics weaker than intuitionistic and minimal logic. We define a notion of minimal, total HT² model which we call partial equilibrium model. Since for normal logic programs these models coincide with partial stable models, we propose the resulting partial equilibrium logic as a logical foundation for well-founded semantics. In addition we axiomatise the logic of HT²-models and prove that it captures the strong equivalence of theories in partial equilibrium logic.

JELIA Conference 2006 Conference Paper

On the Logic and Computation of Partial Equilibrium Models

  • Pedro Cabalar
  • Sergei P. Odintsov
  • David Pearce 0001
  • Agustín Valverde

Abstract The nonmonotonic formalism of partial equilibrium logic (PEL) has recently been proposed as a logical foundation for the partial stable and well-founded semantics of logic programs [1, 2]. We study certain logical properties of PEL and some techniques to compute partial equilibrium models.

Details

JELIA Conference 2004 Conference Paper

Logic Programs with Functions and Default Values

  • Pedro Cabalar
  • David Lorenzo

Abstract In this work we reconsider the replacement of predicate-like notation by functional terms, using a similar syntax to Functional Logic Programming, but under a completely different semantic perspective. Our starting point comes from the use of logic programs for Knowledge Representation and Nonmonotonic Reasoning, especially under three well-known semantics for default negation: Clark’s completion, stable models and well-founded semantics. The motivation for introducing functions in this setting arises from the frequent occurrence of functional dependences in the representation of many domains. The use of functions allows us to avoid explicit axiomatization and provides a more compact representation by nesting functional terms. From a representational point of view, the most interesting introduced feature is the possibility of replacing default negation by the concept of default value of a function. In the paper, we explore this idea of functions with default values, providing adapted versions of the three mentioned semantics for the functional case, and equivalent translations into logic programs.

Details

AAAI Conference 2002 Conference Paper

A Three-Valued Characterization for Strong Equivalence of Logic Programs

  • Pedro Cabalar

In this work we present additional results related to the property of strong equivalence of logic programs. This property asserts that two programs share the same set of stable models, even under the addition of new rules. As shown in a recent work by Lifschitz, Pearce and Valverde, strong equivalence can be simply reduced to equivalence in the logic of Hereand-There (HT). In this paper we provide an alternative based on 3-valued logic, using also, as a first step, a classical logic charaterization. We show that the 3-valued encoding provides a direct interpretation for nested expressions but, when moving to an unrestricted syntax, it generally yields different results from HT.

PDF Details

NMR Workshop 2002 Conference Paper

Alternative characterizations for strong equivalence of logic programs

  • Pedro Cabalar

In this work we present additional results related to the property of strong equivalence of logic programs. This property asserts that two programs share the same set of stable models, even under the addition of new rules. As shown in a recent work by Lifschitz, Pearce and Valverde, strong equivalence can be simply reduced to equivalence in the logic of Here-and-There (HT). In this paper we provide two alternatives respectively based on classical logic and 3-valued logic. The former is applicable to general rules, but not for nested expressions, whereas the latter is applicable for nested expressions but, when moving to an unrestricted syntax, it generally yields different results from HT.

Details