Distributed Answer Set Coloring: Stable Models Computation via Graph Coloring

AbstractUnsatisfiable core analysis can boost the computation of optimum stable models for logic programs with weak constraints. However, current solvers employing unsatisfiable core analysis either run to completion, or provide no suboptimal stable models but the one resulting from the preliminary disjoint cores analysis. This drawback is circumvented here by introducing a progression based shrinking of the analyzed unsatisfiable cores. In fact, suboptimal stable models are possibly found while shrinking unsatisfiable cores, hence resulting into an anytime algorithm. Moreover, as confirmed empirically, unsatisfiable core analysis also benefits from the shrinking process in terms of solved instances.

Download Full-text

Temporal logic programs with variables

Theory and Practice of Logic Programming ◽

10.1017/s1471068416000570 ◽

2016 ◽

Vol 17 (2) ◽

pp. 226-243 ◽

Cited By ~ 1

Author(s):

FELICIDAD AGUADO ◽

PEDRO CABALAR ◽

GILBERTO PÉREZ ◽

CONCEPCIÓN VIDAL ◽

MARTÍN DIÉGUEZ

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Logic Program ◽

Answer Set Programming ◽

Logic Programs ◽

First Order ◽

Linear Time Temporal Logic ◽

Definition Of ◽

Stable Models ◽

Answer Set

AbstractIn this note, we consider the problem of introducing variables in temporal logic programs under the formalism of Temporal Equilibrium Logic, an extension of Answer Set Programming for dealing with linear-time modal operators. To this aim, we provide a definition of a first-order version of Temporal Equilibrium Logic that shares the syntax of first-order Linear-time Temporal Logic but has different semantics, selecting some Linear-time Temporal Logic 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 Answer Set Programming 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.

Download Full-text

Module theorem for the general theory of stable models

Theory and Practice of Logic Programming ◽

10.1017/s1471068412000269 ◽

2012 ◽

Vol 12 (4-5) ◽

pp. 719-735 ◽

Cited By ~ 1

Author(s):

JOSEPH BABB ◽

JOOHYUNG LEE

Keyword(s):

General Theory ◽

General Class ◽

Answer Set Programming ◽

Splitting Theorem ◽

Logic Programs ◽

Input Output ◽

Answer Sets ◽

Output Interface ◽

Stable Models ◽

Answer Set

AbstractThe module theorem by Janhunen et al. demonstrates how to provide a modular structure in answer set programming, where each module has a well-defined input/output interface which can be used to establish the compositionality of answer sets. The theorem is useful in the analysis of answer set programs, and is a basis of incremental grounding and reactive answer set programming. We extend the module theorem to the general theory of stable models by Ferraris et al. The generalization applies to non-ground logic programs allowing useful constructs in answer set programming, such as choice rules, the count aggregate, and nested expressions. Our extension is based on relating the module theorem to the symmetric splitting theorem by Ferraris et al. Based on this result, we reformulate and extend the theory of incremental answer set computation to a more general class of programs.

Download Full-text

DatalogMTL with Negation Under Stable Models Semantics

10.24963/kr.2021/58 ◽

2021 ◽

Author(s):

Przemysław A. Wałęga ◽

David J. Tena Cucala ◽

Egor V. Kostylev ◽

Bernardo Cuenca Grau

Keyword(s):

Answer Set Programming ◽

Data Complexity ◽

Temporal Dimension ◽

Temporal Direction ◽

Stable Models ◽

Answer Set

We introduce negation under stable models semantics in DatalogMTL—a temporal extension of Datalog with metric operators. As a result, we obtain a rule language which combines the power of answer set programming with the temporal dimension provided by metric operators. We show that, in this setting, reasoning becomes undecidable over the rationals and decidable in EXPSPACE in data complexity over the integers. We also show that, if we restrict our attention to forward-propagating programs (where rules propagate information in a single temporal direction), reasoning over integers becomes PSPACE-complete in data complexity and hence no harder than over positive programs; however, reasoning over the rationals in this fragment remains undecidable.

Download Full-text

Linear-Time Temporal Answer Set Programming

Theory and Practice of Logic Programming ◽

10.1017/s1471068421000557 ◽

2021 ◽

pp. 1-55

Author(s):

FELICIDAD AGUADO ◽

PEDRO CABALAR ◽

MARTÍN DIÉGUEZ ◽

GILBERTO PÉREZ ◽

TORSTEN SCHAUB ◽

...

Keyword(s):

Temporal Logic ◽

Linear Time ◽

Selection Criterion ◽

Answer Set Programming ◽

Logic Programs ◽

Modal Operators ◽

Linear Time Temporal Logic ◽

Stable Models ◽

Answer Set

Abstract In this survey, we present an overview on (Modal) Temporal Logic Programming in view of its application to Knowledge Representation and Declarative Problem Solving. The syntax of this extension of logic programs is the result of combining usual rules with temporal modal operators, as in Linear-time Temporal Logic (LTL). In the paper, we focus on the main recent results of the non-monotonic formalism called Temporal Equilibrium Logic (TEL) that is defined for the full syntax of LTL but involves a model selection criterion based on Equilibrium Logic, a well known logical characterization of Answer Set Programming (ASP). As a result, we obtain a proper extension of the stable models semantics for the general case of temporal formulas in the syntax of LTL. We recall the basic definitions for TEL and its monotonic basis, the temporal logic of Here-and-There (THT), and study the differences between finite and infinite trace length. We also provide further useful results, such as the translation into other formalisms like Quantified Equilibrium Logic and Second-order LTL, and some techniques for computing temporal stable models based on automata constructions. In the remainder of the paper, we focus on practical aspects, defining a syntactic fragment called (modal) temporal logic programs closer to ASP, and explaining how this has been exploited in the construction of the solver telingo, a temporal extension of the well-known ASP solver clingo that uses its incremental solving capabilities.

Download Full-text

Stable models for infinitary formulas with extensional atoms

Theory and Practice of Logic Programming ◽

10.1017/s1471068416000314 ◽

2016 ◽

Vol 16 (5-6) ◽

pp. 771-786

Author(s):

AMELIA HARRISON ◽

VLADIMIR LIFSCHITZ

Keyword(s):

Programming Languages ◽

Answer Set Programming ◽

Splitting Theorem ◽

First Order ◽

Definition Of ◽

Stable Models ◽

Answer Set

AbstractThe definition of stable models for propositional formulas with infinite conjunctions and disjunctions can be used to describe the semantics of answer set programming languages. In this note, we enhance that definition by introducing a distinction between intensional and extensional atoms. The symmetric splitting theorem for first-order formulas is then extended to infinitary formulas and used to reason about infinitary definitions.

Download Full-text

On equivalence of infinitary formulas under the stable model semantics

Theory and Practice of Logic Programming ◽

10.1017/s1471068414000088 ◽

2014 ◽

Vol 15 (1) ◽

pp. 18-34 ◽

Cited By ~ 6

Author(s):

AMELIA HARRISON ◽

VLADIMIR LIFSCHITZ ◽

MIROSLAW TRUSZCZYNSKI

Keyword(s):

Intuitionistic Logic ◽

Answer Set Programming ◽

Stable Model ◽

Stable Models ◽

Answer Set

AbstractPropositional formulas that are equivalent in intuitionistic logic, or in its extension known as the logic of here-and-there, have the same stable models. We extend this theorem to propositional formulas with infinitely long conjunctions and disjunctions and show how to apply this generalization to proving properties of aggregates in answer set programming.

Download Full-text

Unsatisfiable Core Shrinking for Anytime Answer Set Optimization

Proceedings of the Twenty-Sixth International Joint Conference on Artificial Intelligence ◽

10.24963/ijcai.2017/666 ◽

2017 ◽

Cited By ~ 3

Author(s):

Mario Alviano ◽

Carmine Dodaro

Keyword(s):

Efficient Algorithms ◽

Set Optimization ◽

Core Analysis ◽

Anytime Algorithm ◽

Original Algorithm ◽

Unsatisfiable Core ◽

Stable Models ◽

Answer Set

Efficient algorithms for the computation of optimum stable models are based on unsatisfiable core analysis. However, these algorithms essentially run to completion, providing few or even no suboptimal stable models. This drawback can be circumvented by shrinking unsatisfiable cores. Interestingly, the resulting anytime algorithm can solve more instances than the original algorithm.

Download Full-text

Relating Multi-Adjoint Normal Logic Programs to Core Fuzzy Answer Set Programs from a Semantical Approach

Mathematics ◽

10.3390/math8060881 ◽

2020 ◽

Vol 8 (6) ◽

pp. 881

Author(s):

M. Eugenia Cornejo ◽

David Lobo ◽

Jesús Medina

Keyword(s):

Fuzzy Logic ◽

Logic Programming ◽

Programming Language ◽

Answer Set Programming ◽

Logic Programs ◽

The Core ◽

Normal Logic ◽

Answer Sets ◽

Stable Models ◽

Answer Set

This paper relates two interesting paradigms in fuzzy logic programming from a semantical approach: core fuzzy answer set programming and multi-adjoint normal logic programming. Specifically, it is shown how core fuzzy answer set programs can be translated into multi-adjoint normal logic programs and vice versa, preserving the semantics of the starting program. This translation allows us to combine the expressiveness of multi-adjoint normal logic programming with the compactness and simplicity of the core fuzzy answer set programming language. As a consequence, theoretical properties and results which relate the answer sets to the stable models of the respective logic programming frameworks are obtained. Among others, this study enables the application of the existence theorem of stable models developed for multi-adjoint normal logic programs to ensure the existence of answer sets in core fuzzy answer set programs.

Download Full-text

Relating Two Dialects of Answer Set Programming

Theory and Practice of Logic Programming ◽

10.1017/s1471068419000322 ◽

2019 ◽

Vol 19 (5-6) ◽

pp. 1006-1020 ◽

Cited By ~ 1

Author(s):

AMELIA HARRISON ◽

VLADIMIR LIFSCHITZ

Keyword(s):

Working Group ◽

Answer Set Programming ◽

Stable Model ◽

Input Language ◽

Core Language ◽

Definition Of ◽

Stable Models ◽

Answer Set

AbstractThe input language of the answer set solver clingo is based on the definition of a stable model proposed by Paolo Ferraris. The semantics of the ASP-Core language, developed by the ASP Standardization Working Group, uses the approach to stable models due to Wolfgang Faber, Nicola Leone, and Gerald Pfeifer. The two languages are based on different versions of the stable model semantics, and the ASP-Core document requires, “for the sake of an uncontroversial semantics,” that programs avoid the use of recursion through aggregates. In this paper we prove that the absence of recursion through aggregates does indeed guarantee the equivalence between the two versions of the stable model semantics, and show how that requirement can be relaxed without violating the equivalence property.

Download Full-text