Lloyd-Topor completion and general stable models

AbstractWe investigate the relationship between the generalization of program completion defined in 1984 by Lloyd and Topor and the generalization of the stable model semantics introduced recently by Ferraris et al. The main theorem can be used to characterize, in some cases, the general stable models of a logic program by a first-order formula. The proof uses Truszczynski's stable model semantics of infinitary propositional formulas.

Download Full-text

Verifying Tight Logic Programs with anthem and vampire

Theory and Practice of Logic Programming ◽

10.1017/s1471068420000344 ◽

2020 ◽

Vol 20 (5) ◽

pp. 735-750

Author(s):

JORGE FANDINNO ◽

VLADIMIR LIFSCHITZ ◽

PATRICK LÜHNE ◽

TORSTEN SCHAUB

Keyword(s):

Software Tools ◽

Program Completion ◽

Logic Programs ◽

Input Language ◽

First Order ◽

Input And Output ◽

Definition Of ◽

Correctness Of Programs ◽

The Relationship ◽

Stable Models

AbstractThis paper continues the line of research aimed at investigating the relationship between logic programs and first-order theories. We extend the definition of program completion to programs with input and output in a subset of the input language of the ASP grounder gringo, study the relationship between stable models and completion in this context, and describe preliminary experiments with the use of two software tools, anthem and vampire, for verifying the correctness of programs with input and output. Proofs of theorems are based on a lemma that relates the semantics of programs studied in this paper to stable models of first-order formulas.

Download Full-text

On the existence of stable models of non-stratified logic programs

Theory and Practice of Logic Programming ◽

10.1017/s1471068405002589 ◽

2006 ◽

Vol 6 (1-2) ◽

pp. 169-212 ◽

Cited By ~ 14

Author(s):

STEFANIA COSTANTINI

Keyword(s):

Canonical Form ◽

Logic Program ◽

Practical Importance ◽

The Body ◽

Fundamental Result ◽

Stable Model ◽

Logic Programs ◽

Truth Value ◽

Answer Sets ◽

Stable Models

In this paper we analyze the relationship between cyclic definitions and consistency in Gelfond-Lifschitz's answer sets semantics (originally defined as ‘stable model semantics’). This paper introduces a fundamental result, which is relevant for Answer Set programming, and planning. For the first time since the definition of the stable model semantics, the class of logic programs for which a stable model exists is given a syntactic characterization. This condition may have a practical importance both for defining new algorithms for checking consistency and computing answer sets, and for improving the existing systems. The approach of this paper is to introduce a new canonical form (to which any logic program can be reduced to), to focus the attention on cyclic dependencies. The technical result is then given in terms of programs in canonical form (canonical programs), without loss of generality: the stable models of any general logic program coincide (up to the language) to those of the corresponding canonical program. The result is based on identifying the cycles contained in the program, showing that stable models of the overall program are composed of stable models of suitable sub-programs, corresponding to the cycles, and on defining the Cycle Graph. Each vertex of this graph corresponds to one cycle, and each edge corresponds to one handle, which is a literal containing an atom that, occurring in both cycles, actually determines a connection between them. In fact, the truth value of the handle in the cycle where it appears as the head of a rule, influences the truth value of the atoms of the cycle(s) where it occurs in the body. We can therefore introduce the concept of a handle path, connecting different cycles. Cycles can be even, if they consist of an even number of rules, or vice versa they can be odd. Problems for consistency, as it is well-known, originate in the odd cycles. If for every odd cycle we can find a handle path with certain properties, then the existence of stable model is guaranteed. We will show that based on this results new classes of consistent programs can be defined, and that cycles and cycle graphs can be generalized to components and component graphs.

Download Full-text

Preferred extensions as stable models

Theory and Practice of Logic Programming ◽

10.1017/s1471068408003359 ◽

2008 ◽

Vol 8 (04) ◽

pp. 527-543 ◽

Cited By ~ 27

Author(s):

JUAN CARLOS NIEVES ◽

ULISES CORTÉS ◽

MAURICIO OSORIO

Keyword(s):

Direct Relationship ◽

Logic Program ◽

Nonmonotonic Reasoning ◽

Mapping Function ◽

Propositional Formula ◽

Stable Model ◽

Minimal Models ◽

Argumentation Framework ◽

Polynomial Size ◽

Stable Models

AbstractGiven an argumentation frameworkAF, we introduce a mapping function that constructs a disjunctive logic programP, such that the preferred extensions ofAFcorrespond to the stable models ofP, after intersecting each stable model with the relevant atoms. The given mapping function is of polynomial size w.r.t.AF.In particular, we identify that there is a direct relationship between the minimal models of a propositional formula and the preferred extensions of an argumentation framework by working on representing the defeated arguments. Then we show how to infer the preferred extensions of an argumentation framework by using UNSAT algorithms and disjunctive stable model solvers. The relevance of this result is that we define a direct relationship between one of the most satisfactory argumentation semantics and one of the most successful approach of nonmonotonic reasoning i.e., logic programming with the stable model semantics.

Download Full-text

Relational theories with null values and non-herbrand stable models

Theory and Practice of Logic Programming ◽

10.1017/s147106841200018x ◽

2012 ◽

Vol 12 (4-5) ◽

pp. 565-582 ◽

Cited By ~ 2

Author(s):

VLADIMIR LIFSCHITZ ◽

KARL PICHOTTA ◽

FANGKAI YANG

Keyword(s):

Incomplete Information ◽

Relational Databases ◽

Logic Program ◽

Answer Set Programming ◽

First Order ◽

Relational Theories ◽

Null Values ◽

Closure Assumption ◽

General Method ◽

Stable Models

AbstractGeneralized relational theories with null values in the sense of Reiter are first-order theories that provide a semantics for relational databases with incomplete information. In this paper we show that any such theory can be turned into an equivalent logic program, so that models of the theory can be generated using computational methods of answer set programming. As a step towards this goal, we develop a general method for calculating stable models under the domain closure assumption but without the unique name assumption.

Download Full-text

Computing large and small stable models

Theory and Practice of Logic Programming ◽

10.1017/s1471068402001138 ◽

2001 ◽

Vol 2 (1) ◽

pp. 1-23 ◽

Cited By ~ 3

Author(s):

MIROSŁAW TRUSZCZYŃSKI

Keyword(s):

Upper Bound ◽

Linear Time ◽

Logic Program ◽

Time Algorithm ◽

Stable Model ◽

Linear Time Algorithm ◽

Constant Independent ◽

Fixed Integer ◽

Fixed Parameter ◽

Stable Models

In this paper, we focus on the problem of existence and computing of small and large stable models. We show that for every fixed integer k, there is a linear-time algorithm to decide the problem LSM (large stable models problem): does a logic program P have a stable model of size at least [mid ]P[mid ]−k? In contrast, we show that the problem SSM (small stable models problem) to decide whether a logic program P has a stable model of size at most k is much harder. We present two algorithms for this problem but their running time is given by polynomials of order depending on k. We show that the problem SSM is fixed-parameter intractable by demonstrating that it is W[2]-hard. This result implies that it is unlikely an algorithm exists to compute stable models of size at most k that would run in time O(mc), where m is the size of the program and c is a constant independent of k. We also provide an upper bound on the fixed-parameter complexity of the problem SSM by showing that it belongs to the class W[3].

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

Achieving compositionality of the stable model semantics for smodels programs

Theory and Practice of Logic Programming ◽

10.1017/s147106840800358x ◽

2008 ◽

Vol 8 (5-6) ◽

pp. 717-761 ◽

Cited By ~ 17

Author(s):

EMILIA OIKARINEN ◽

TOMI JANHUNEN

Keyword(s):

Logic Programming ◽

A Priori ◽

Logic Program ◽

Connected Components ◽

Module Structure ◽

Stable Model ◽

Strongly Connected Components ◽

Strongly Connected ◽

Practical Demonstration ◽

Stable Models

AbstractIn this paper, a Gaifman–Shapiro-style module architecture is tailored to the case of smodels programs under the stable model semantics. The composition of smodels program modules is suitably limited by module conditions which ensure the compatibility of the module system with stable models. Hence the semantics of an entire smodels program depends directly on stable models assigned to its modules. This result is formalized as a module theorem which truly strengthens V. Lifschitz and H. Turner's splitting-set theorem (June 1994, Splitting a logic program. In Logic Programming: Proceedings of the Eleventh International Conference on Logic Programming, Santa Margherita Ligure, Italy, P. V. Hentenryck, Ed. MIT Press, 23–37) for the class of smodels programs. To streamline generalizations in the future, the module theorem is first proved for normal programs and then extended to cover smodels programs using a translation from the latter class of programs to the former class. Moreover, the respective notion of module-level equivalence, namely modular equivalence, is shown to be a proper congruence relation: it is preserved under substitutions of modules that are modularly equivalent. Principles for program decomposition are also addressed. The strongly connected components of the respective dependency graph can be exploited in order to extract a module structure when there is no explicit a priori knowledge about the modules of a program. The paper includes a practical demonstration of tools that have been developed for automated (de)composition of smodels programs.

Download Full-text

Modeling and Language Extensions

AI Magazine ◽

10.1609/aimag.v37i3.2673 ◽

2016 ◽

Vol 37 (3) ◽

pp. 33-44 ◽

Cited By ~ 4

Author(s):

Martin Gebser ◽

Torsten Schaub

Keyword(s):

Expressive Language ◽

Logic Program ◽

Answer Set Programming ◽

Stable Model ◽

Logic Programs ◽

First Order ◽

High Level Modeling ◽

High Level ◽

Answer Sets ◽

First Order Variables

Answer set programming (ASP) has emerged as an approach to declarative problem solving based on the stable model semantics for logic programs. The basic idea is to represent a computational problem by a logic program, formulating constraints in terms of rules, such that its answer sets correspond to problem solutions. To this end, ASP combines an expressive language for high-level modeling with powerful low-level reasoning capacities, provided by off-the-shelf tools. Compact problem representations take advantage of genuine modeling features of ASP, including (first-order) variables, negation by default, and recursion. In this article, we demonstrate the ASP methodology on two example scenarios, illustrating basic as well as advanced modeling and solving concepts. We also discuss mechanisms to represent and implement extended kinds of preferences and optimization. An overview of further available extensions concludes the article.

Download Full-text

Well-Founded Semantics Coincides with Three-Valued Stable Semantics1

Fundamenta Informaticae ◽

10.3233/fi-1990-13404 ◽

1990 ◽

Vol 13 (4) ◽

pp. 445-463

Author(s):

Teodor Przymusinski

Keyword(s):

Logic Program ◽

Natural Extension ◽

Natural Generalization ◽

Stable Model ◽

Logic Programs ◽

Default Theory ◽

Recent Approach ◽

Stable Semantics ◽

Disjunctive Logic Programs ◽

Stable Models

We introduce 3-valued stable models which are a natural generalization of standard (2-valued) stable models. We show that every logic program P has at least one 3-valued stable model and that the well-founded model of any program P [Van Gelder et al., 1990] coincides with the smallest 3-valued stable model of P. We conclude that the well-founded semantics of an arbitrary logic program coincides with the 3-valued stable model semantics. The 3-valued stable semantics is closely related to non-monotonic formalisms in AI. Namely, every program P can be translated into a suitable autoepistemic (resp. default) theory P ˆ so that the 3-valued stable semantics of P coincides with the (3-valued) autoepistemic (resp. default) semantics of P ˆ. Similar results hold for circumscription and CWA. Moreover, it can be shown that the 3-valued stable semantics has a natural extension to the class of all disjunctive logic programs and deductive databases. Finally, following upon the recent approach developed by Gelfond and Lifschitz, we extend all of our results to more general logic programs which, in addition to the use of negation as failure, permit the use of classical negation.

Download Full-text

Nonlinear Analysis of Visual Evoked Potentials Elicited by Color Stimulation

Methods of Information in Medicine ◽

10.1055/s-0038-1636871 ◽

1997 ◽

Vol 36 (04/05) ◽

pp. 315-318 ◽

Cited By ~ 3

Author(s):

K. Momose ◽

K. Komiya ◽

A. Uchiyama

Keyword(s):

Visual System ◽

Evoked Potentials ◽

Visual Evoked Potentials ◽

Normal Subjects ◽

Second Order ◽

First Order ◽

The Relationship ◽

Perceived Color ◽

Second Order Nonlinearity ◽

Visual Evoked

Abstract:The relationship between chromatically modulated stimuli and visual evoked potentials (VEPs) was considered. VEPs of normal subjects elicited by chromatically modulated stimuli were measured under several color adaptations, and their binary kernels were estimated. Up to the second-order, binary kernels obtained from VEPs were so characteristic that the VEP-chromatic modulation system showed second-order nonlinearity. First-order binary kernels depended on the color of the stimulus and adaptation, whereas second-order kernels showed almost no difference. This result indicates that the waveforms of first-order binary kernels reflect perceived color (hue). This supports the suggestion that kernels of VEPs include color responses, and could be used as a probe with which to examine the color visual system.

Download Full-text