BZPEERPapers, people, evidence and research paths
Menu

Discover

SearchFind papers, people, topics, institutions and opportunities from one place.GraphSee how papers, authors, topics and evidence connect.

Research tools

HomeContinue from the papers, people and topics that matter now.CollectionsTurn saved papers into reading lists, evidence maps and shareable context.ResearchReconstruct the path that led you from search to paper to question.CollaborationMove from a paper, topic or expert request into a focused thread.PublishCreate full-text research articles with metadata, formulas and versions.

Network

ExpertsFind specialists whose work and reviews explain why they can help.CommunitiesJoin research groups organized around papers, topics and shared evidence.

Opportunities

ListingsBrowse roles, calls and collaborations connected to real research context.

Account

Log inReturn to your saved papers, graph views and active threads.Create accountStart saving papers, building a research trail and joining teams.
Log inCreate account

Source author record

Pedro Cabalar

Pedro Cabalar appears in the imported research catalog. Authorship, coauthor and topic links are available while profile ownership is still unclaimed.

ResearcherUnclaimed source record
Artificial IntelligenceLogic in Computer ScienceProgramming Languages

Catalog footprint

What is connected

20works
3topics
4close collaborators

Actions

Connect this record

Log in to claim
Open graphBrowse works

Research graph

See the researcher in context

Open full explorer

Inspect adjacent papers, topics, institutions and collaborators without losing the researcher page.

Building this map preview

BZPEER is loading the nearby papers, people, topics and institutions for this page.

Published work

20 published item(s)

preprint2025arXiv

Comparing Non-minimal Semantics for Disjunction in Answer Set Programming

In this paper, we compare four different semantics for disjunction in Answer Set Programming that, unlike stable models, do not adhere to the principle of model minimality. Two of these approaches, Cabalar and Muñiz' \emph{Justified Models} and Doherty and Szalas' \emph{Strongly Supported Models}, directly provide an alternative non-minimal semantics for disjunction. The other two, Aguado et al's \emph{Forks} and Shen and Eiter's \emph{Determining Inference} (DI) semantics, actually introduce a new disjunction connective, but are compared here as if they constituted new semantics for the standard disjunction operator. We are able to prove that three of these approaches (Forks, Justified Models and a reasonable relaxation of the DI semantics) actually coincide, constituting a common single approach under different definitions. Moreover, this common semantics always provides a superset of the stable models of a program (in fact, modulo any context) and is strictly stronger than the fourth approach (Strongly Supported Models), that actually treats disjunctions as in classical logic.

0 citations0 reviewsNo code linkedOpen access
preprint2025arXiv

Towards Constraint Temporal Answer Set Programming

Reasoning about dynamic systems with a fine-grained temporal and numeric resolution presents significant challenges for logic-based approaches like Answer Set Programming (ASP). To address this, we introduce and elaborate upon a novel temporal and constraint-based extension of the logic of Here-and-There and its nonmonotonic equilibrium extension, representing, to the best of our knowledge, the first approach to nonmonotonic temporal reasoning with constraints specifically tailored for ASP. This expressive system is achieved by a synergistic combination of two foundational ASP extensions: the linear-time logic of Here-and-There, providing robust nonmonotonic temporal reasoning capabilities, and the logic of Here-and-There with constraints, enabling the direct integration and manipulation of numeric constraints, among others. This work establishes the foundational logical framework for tackling complex dynamic systems with high resolution within the ASP paradigm.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A System for Explainable Answer Set Programming

We present xclingo, a tool for generating explanations from ASP programs annotated with text and labels. These annotations allow tracing the application of rules or the atoms derived by them. The input of xclingo is a markup language written as ASP comment lines, so the programs annotated in this way can still be accepted by a standard ASP solver. xclingo translates the annotations into additional predicates and rules and uses the ASP solver clingo to obtain the extension of those auxiliary predicates. This information is used afterwards to construct derivation trees containing textual explanations. The language allows selecting which atoms to explain and, in its turn, which atoms or rules to include in those explanations. We illustrate the basic features through a diagnosis problem from the literature.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

A Uniform Treatment of Aggregates and Constraints in Hybrid ASP

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

An ASP semantics for Constraints involving Conditional Aggregates

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.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

eclingo: A solver for Epistemic Logic Programs

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. Under consideration for acceptance in TPLP.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Implementing Dynamic Answer Set Programming

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

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Modular Answer Set Programming as a Formal Specification Language

In this paper, we study the problem of formal verification for Answer Set Programming (ASP), namely, obtaining a formal proof showing that the answer sets of a given (non-ground) logic program P correctly correspond to the solutions to the problem encoded by P, 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 modules that may incorporate local hidden atoms at different levels. Then, verifying the logic program P amounts to prove some kind of equivalence between P and its modular specification. Under consideration for acceptance in TPLP.

0 citations0 reviewsNo code linkedOpen access
preprint2020arXiv

Towards Metric Temporal Answer Set Programming

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.

0 citations0 reviewsNo code linkedOpen access
preprint2019arXiv

Revisiting Explicit Negation in Answer Set Programming

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. Under consideration for acceptance in TPLP.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Enablers and Inhibitors in Causal Justifications of Logic Programs

To appear in Theory and Practice of Logic Programming (TPLP). In this paper we propose an extension of logic programming (LP) where each default literal derived from the well-founded model is associated to a justification represented as an algebraic expression. This expression contains both causal explanations (in the form of proof graphs built with rule labels) and terms under the scope of negation that stand for conditions that enable or disable the application of causal rules. Using some examples, we discuss how these new conditions, we respectively call "enablers" and "inhibitors", are intimately related to default negation and have an essentially different nature from regular cause-effect relations. The most important result is a formal comparison to the recent algebraic approaches for justifications in LP: "Why-not Provenance" (WnP) and "Causal Graphs" (CG). We show that the current approach extends both WnP and CG justifications under the Well-Founded Semantics and, as a byproduct, we also establish a formal relation between these two approaches.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Equilibrium Graphs

In this paper we present an extension of Peirce's existential graphs to provide a diagrammatic representation of expressions in Quantified Equilibrium Logic (QEL). Using this formalisation, logical connectives are replaced by encircled regions (circles and squares) and quantified variables are represented as "identity" lines. Although the expressive power is equivalent to that of QEL, the new representation can be useful for illustrative or educational purposes.

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Justifications for Programs with Disjunctive and Causal-choice Rules

In this paper, we study an extension of the stable model semantics for disjunctive logic programs where each true atom in a model is associated with an algebraic expression (in terms of rule labels) that represents its justifications. As in our previous work for non-disjunctive programs, these justifications are obtained in a purely semantic way, by algebraic operations (product, addition and application) on a lattice of causal values. Our new definition extends the concept of causal stable model to disjunctive logic programs and satisfies that each (standard) stable model corresponds to a disjoint class of causal stable models sharing the same truth assignments, but possibly varying the obtained explanations. We provide a pair of illustrative examples showing the behaviour of the new semantics and discuss the need of introducing a new type of rule, which we call causal-choice. This type of rule intuitively captures the idea of "$A$ may cause $B$" and, when causal information is disregarded, amounts to a usual choice rule under the standard stable model semantics. (Under consideration for publication in Theory and Practice of Logic Programming)

0 citations0 reviewsNo code linkedOpen access
preprint2016arXiv

Temporal Logic Programs with Variables

In this note we consider the problem of introducing variables in temporal logic programs under the formalism of "Temporal Equilibrium Logic" (TEL), an extension of Answer Set Programming (ASP) for dealing with linear-time modal operators. To this aim, we provide a definition of a first-order version of TEL that shares the syntax of first-order Linear-time Temporal Logic (LTL) but has a different semantics, selecting some LTL models we call "temporal stable models". Then, we consider a subclass of theories (called "splittable temporal logic programs") that are close to usual logic programs but allowing a restricted use of temporal operators. In this setting, we provide a syntactic definition of "safe variables" that suffices to show the property of "domain independence" -- that is, addition of arbitrary elements in the universe does not vary the set of temporal stable models. Finally, we present a method for computing the derivable facts by constructing a non-temporal logic program with variables that is fed to a standard ASP grounder. The information provided by the grounder is then used to generate a subset of ground temporal rules which is equivalent to (and generally smaller than) the full program instantiation.

0 citations0 reviewsNo code linkedOpen access
preprint2015arXiv

A Denotational Semantics for Equilibrium Logic

In this paper we provide an alternative semantics for Equilibrium Logic and its monotonic basis, the logic of Here-and-There (also known as Gödel's G3 logic) that relies on the idea of "denotation" of a formula, that is, a function that collects the set of models of that formula. Using the three-valued logic G3 as a starting point and an ordering relation (for which equilibrium/stable models are minimal elements) we provide several elementary operations for sets of interpretations. By analysing structural properties of the denotation of formulas, we show some expressiveness results for G3 such as, for instance, that conjunction is not expressible in terms of the other connectives. Moreover, the denotational semantics allows us to capture the set of equilibrium models of a formula with a simple and compact set expression. We also use this semantics to provide several formal definitions for entailment relations that are usual in the literature, and further introduce a new one called "strong entailment". We say that $α$ strongly entails $β$ when the equilibrium models of $α\wedge γ$ are also equilibrium models of $β\wedge γ$ for any context $γ$. We also provide a characterisation of strong entailment in terms of the denotational semantics, and give an example of a sufficient condition that can be applied in some cases.

0 citations0 reviewsNo code linkedOpen access
preprint2014arXiv

Causal Graph Justifications of Logic Programs

In this work we propose a multi-valued extension of logic programs under the stable models semantics where each true atom in a model is associated with a set of justifications. These justifications are expressed in terms of causal graphs formed by rule labels and edges that represent their application ordering. For positive programs, we show that the causal justifications obtained for a given atom have a direct correspon- dence to (relevant) syntactic proofs of that atom using the program rules involved in the graphs. The most interesting contribution is that this causal information is obtained in a purely semantic way, by algebraic op- erations (product, sum and application) on a lattice of causal values whose ordering relation expresses when a justification is stronger than another. Finally, for programs with negation, we define the concept of causal stable model by introducing an analogous transformation to Gelfond and Lifschitz's program reduct. As a result, default negation behaves as "absence of proof" and no justification is derived from negative liter

0 citations0 reviewsNo code linkedOpen access
preprint2013arXiv

An Algebra of Causal Chains

In this work we propose a multi-valued extension of logic programs under the stable models semantics where each true atom in a model is associated with a set of justifications, in a similar spirit than a set of proof trees. The main contribution of this paper is that we capture justifications into an algebra of truth values with three internal operations: an addition '+' representing alternative justifications for a formula, a commutative product '*' representing joint interaction of causes and a non-commutative product '.' acting as a concatenation or proof constructor. Using this multi-valued semantics, we obtain a one-to-one correspondence between the syntactic proof tree of a standard (non-causal) logic program and the interpretation of each true atom in a model. Furthermore, thanks to this algebraic characterization we can detect semantic properties like redundancy and relevance of the obtained justifications. We also identify a lattice-based characterization of this algebra, defining a direct consequences operator, proving its continuity and that its least fix point can be computed after a finite number of iterations. Finally, we define the concept of causal stable model by introducing an analogous transformation to Gelfond and Lifschitz's program reduct.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

A Logical Charaterisation of Ordered Disjunction

In this paper we consider a logical treatment for the ordered disjunction operator 'x' introduced by Brewka, Niemelä and Syrjänen in their Logic Programs with Ordered Disjunctions (LPOD). LPODs are used to represent preferences in logic programming under the answer set semantics. Their semantics is defined by first translating the LPOD into a set of normal programs (called split programs) and then imposing a preference relation among the answer sets of these split programs. We concentrate on the first step and show how a suitable translation of the ordered disjunction as a derived operator into the logic of Here-and-There allows capturing the answer sets of the split programs in a direct way. We use this characterisation not only for providing an alternative implementation for LPODs, but also for checking several properties (under strongly equivalent transformations) of the 'x' operator, like for instance, its distributivity with respect to conjunction or regular disjunction. We also make a comparison to an extension proposed by Kärger, Lopes, Olmedilla and Polleres, that combines 'x' with regular disjunction.

0 citations0 reviewsNo code linkedOpen access
preprint2010arXiv

Functional Answer Set Programming

In this paper we propose an extension of Answer Set Programming (ASP), and in particular, of its most general logical counterpart, Quantified Equilibrium Logic (QEL), to deal with partial functions. Although the treatment of equality in QEL can be established in different ways, we first analyse the choice of decidable equality with complete functions and Herbrand models, recently proposed in the literature. We argue that this choice yields some counterintuitive effects from a logic programming and knowledge representation point of view. We then propose a variant called QELF where the set of functions is partitioned into partial and Herbrand functions (we also call constructors). In the rest of the paper, we show a direct connection to Scott's Logic of Existence and present a practical application, proposing an extension of normal logic programs to deal with partial functions and equality, so that they can be translated into function-free normal programs, being possible in this way to compute their answer sets with any standard ASP solver.

0 citations0 reviewsNo code linkedOpen access
preprint2002arXiv

Alternative Characterizations for Strong Equivalence of Logic Programs

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.

0 citations0 reviewsNo code linkedOpen access