scholarly journals Reformulating the Situation Calculus and the Event Calculus in the General Theory of Stable Models and in Answer Set Programming

2012 ◽  
Vol 43 ◽  
pp. 571-620 ◽  
Author(s):  
J. Lee ◽  
R. Palla
Keyword(s):  
General Theory ◽  
Situation Calculus ◽  
Stable Model ◽  
Logic Programs ◽  
Event Calculus ◽  
Action Languages ◽  
Canonical Formulas ◽  
Action Logics ◽  
Stable Models ◽  
Answer Set

Circumscription and logic programs under the stable model semantics are two well-known nonmonotonic formalisms. The former has served as a basis of classical logic based action formalisms, such as the situation calculus, the event calculus and temporal action logics; the latter has served as a basis of a family of action languages, such as language A and several of its descendants. Based on the discovery that circumscription and the stable model semantics coincide on a class of canonical formulas, we reformulate the situation calculus and the event calculus in the general theory of stable models. We also present a translation that turns the reformulations further into answer set programs, so that efficient answer set solvers can be applied to compute the situation calculus and the event calculus.

scholarly journals Module theorem for the general theory of stable models

2012 ◽  
Vol 12 (4-5) ◽  
pp. 719-735 ◽  
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.

scholarly journals Query Answering with Guarded Existential Rules under Stable Model Semantics

2020 ◽  
Vol 34 (03) ◽  
pp. 3017-3024
Author(s):  
Hai Wan ◽  
Guohui Xiao ◽  
Chenglin Wang ◽  
Xianqiao Liu ◽  
Junhong Chen ◽  
...  
Keyword(s):  
Answer Set Programming ◽  
Query Answering ◽  
Prototype System ◽  
Stable Model ◽  
Logic Programs ◽  
Termination Problem ◽  
Answer Set

In this paper, we study the problem of query answering with guarded existential rules (also called GNTGDs) under stable model semantics. Our goal is to use existing answer set programming (ASP) solvers. However, ASP solvers handle only finitely-ground logic programs while the program translated from GNTGDs by Skolemization is not in general. To address this challenge, we introduce two novel notions of (1) guarded instantiation forest to describe the instantiation of GNTGDs and (2) prime block to characterize the repeated infinitely-ground program translated from GNTGDs. Using these notions, we prove that the ground termination problem for GNTGDs is decidable. We also devise an algorithm for query answering with GNTGDs using ASP solvers. We have implemented our approach in a prototype system. The evaluation over a set of benchmarks shows encouraging results.

Action language ℬ𝒞+

2015 ◽  
Vol 30 (4) ◽  
pp. 899-922 ◽  
Author(s):  
Joseph Babb ◽  
Joohyung Lee
Keyword(s):  
Main Idea ◽  
Answer Set Programming ◽  
Stable Model ◽  
Formal Models ◽  
Transition Systems ◽  
Action Languages ◽  
Action Language ◽  
Language Constructs ◽  
High Level ◽  
Answer Set

Abstract Action languages are formal models of parts of natural language that are designed to describe effects of actions. Many of these languages can be viewed as high-level notations of answer set programs structured to represent transition systems. However, the form of answer set programs considered in the earlier work is quite limited in comparison with the modern Answer Set Programming (ASP) language, which allows several useful constructs for knowledge representation, such as choice rules, aggregates and abstract constraint atoms. We propose a new action language called BC +, which closes the gap between action languages and the modern ASP language. The main idea is to define the semantics of BC + in terms of general stable model semantics for propositional formulas, under which many modern ASP language constructs can be identified with shorthands for propositional formulas. Language BC  + turns out to be sufficiently expressive to encompass the best features of other action languages, such as languages B , C , C + and BC . Computational methods available in ASP solvers are readily applicable to compute BC +, which led to an implementation of the language by extending system cplus2asp .

scholarly journals A decidable subclass of finitary programs

2010 ◽  
Vol 10 (4-6) ◽  
pp. 481-496 ◽  
Author(s):  
SABRINA BASELICE ◽  
PIERO A. BONATTI
Keyword(s):  
Problem Solving ◽  
Answer Set Programming ◽  
Stable Model ◽  
Unique Combination ◽  
Logic Programs ◽  
Trade Off ◽  
Full Support ◽  
Odd Cycles ◽  
Answer Set

AbstractAnswer set programming—the most popular problem solving paradigm based on logic programs—has been recently extended to support uninterpreted function symbols (Syrjänen 2001, Bonatti 2004; Simkus and Eiter 2007; Gebseret al. 2007; Baseliceet al. 2009; Calimeriet al. 2008). All of these approaches have some limitation. In this paper we propose a class of programs called FP2 that enjoys a different trade-off between expressiveness and complexity. FP2 is inspired by the extension of finitary normal programs with local variables introduced in (Bonatti 2004, Section 5). FP2 programs enjoy the following unique combination of properties: (i) the ability of expressing predicates with infinite extensions; (ii) full support for predicates with arbitrary arity; (iii) decidability of FP2 membership checking; (iv) decidability of skeptical and credulous stable model reasoning for call-safe queries. Odd cycles are supported by composing FP2 programs with argument restricted programs.

scholarly journals Order-consistent programs are cautiously monotonic

2001 ◽  
Vol 1 (4) ◽  
pp. 487-495 ◽  
Author(s):  
HUDSON TURNER
Keyword(s):  
Stable Model ◽  
Logic Programs ◽  
Normal Logic ◽  
Answer Sets ◽  
Answer Set

Some normal logic programs under the answer set (or stable model) semantics lack the appealing property of ‘cautious monotonicity.’ That is, augmenting a program with one of its consequences may cause it to lose another of its consequences. The syntactic condition of ‘order-consistency’ was shown by Fages to guarantee existence of an answer set. This note establishes that order-consistent programs are not only consistent, but cautiously monotonic. From this it follows that they are also ‘cumulative’. That is, augmenting an order-consistent program with some of its consequences does not alter its consequences. In fact, as we show, its answer sets remain unchanged.

scholarly journals Knowledge Forgetting in Answer Set Programming

2014 ◽  
Vol 50 ◽  
pp. 31-70 ◽  
Author(s):  
Y. Wang ◽  
Y. Zhang ◽  
Y. Zhou ◽  
M. Zhang
Keyword(s):  
Logic Program ◽  
Answer Set Programming ◽  
Irrelevant Information ◽  
Semantic Knowledge ◽  
Decision Problems ◽  
Stable Model ◽  
Logic Programs ◽  
Knowledge Based ◽  
Substitution Principle ◽  
Answer Set

The ability of discarding or hiding irrelevant information has been recognized as an important feature for knowledge based systems, including answer set programming. The notion of strong equivalence in answer set programming plays an important role for different problems as it gives rise to a substitution principle and amounts to knowledge equivalence of logic programs. In this paper, we uniformly propose a semantic knowledge forgetting, called HT- and FLP-forgetting, for logic programs under stable model and FLP-stable model semantics, respectively. Our proposed knowledge forgetting discards exactly the knowledge of a logic program which is relevant to forgotten variables. Thus it preserves strong equivalence in the sense that strongly equivalent logic programs will remain strongly equivalent after forgetting the same variables. We show that this semantic forgetting result is always expressible; and we prove a representation theorem stating that the HT- and FLP-forgetting can be precisely characterized by Zhang-Zhou's four forgetting postulates under the HT- and FLP-model semantics, respectively. We also reveal underlying connections between the proposed forgetting and the forgetting of propositional logic, and provide complexity results for decision problems in relation to the forgetting. An application of the proposed forgetting is also considered in a conflict solving scenario.

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

2006 ◽  
Vol 6 (1-2) ◽  
pp. 169-212 ◽  
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.

The intricacies of three-valued extensional semantics for higher-order logic programs

2017 ◽  
Vol 17 (5-6) ◽  
pp. 974-991
Author(s):  
PANOS RONDOGIANNIS ◽  
IOANNA SYMEONIDOU
Keyword(s):  
Infinite Number ◽  
Higher Order ◽  
Order Logic ◽  
Stable Model ◽  
Logic Programs ◽  
Higher Order Logic ◽  
Truth Values ◽  
Positive Side ◽  
Stable Models

AbstractM. Bezem defined an extensional semantics for positive higher-order logic programs. Recently, it was demonstrated by Rondogiannis and Symeonidou that Bezem's technique can be extended to higher-order logic programs with negation, retaining its extensional properties, provided that it is interpreted under a logic with an infinite number of truth values. Rondogiannis and Symeonidou also demonstrated that Bezem's technique, when extended under the stable model semantics, does not in general lead to extensional stable models. In this paper, we consider the problem of extending Bezem's technique under the well-founded semantics. We demonstrate that the well-founded extensionfailsto retain extensionality in the general case. On the positive side, we demonstrate that for stratified higher-order logic programs, extensionality is indeed achieved. We analyze the reasons of the failure of extensionality in the general case, arguing that a three-valued setting cannot distinguish between certain predicates that appear to have a different behaviour inside a program context, but which happen to be identical as three-valued relations.

scholarly journals Anytime answer set optimization via unsatisfiable core shrinking

2016 ◽  
Vol 16 (5-6) ◽  
pp. 533-551 ◽  
Author(s):  
MARIO ALVIANO ◽  
CARMINE DODARO
Keyword(s):  
Set Optimization ◽  
Core Analysis ◽  
Logic Programs ◽  
Anytime Algorithm ◽  
Shrinking Process ◽  
The One ◽  
Weak Constraints ◽  
Unsatisfiable Core ◽  
Stable Models ◽  
Answer Set

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.

scholarly journals The rise and fall of semantic rule updates based onSE-models

2013 ◽  
Vol 14 (6) ◽  
pp. 869-907 ◽  
Author(s):  
MARTIN SLOTA ◽  
JOÃO LEITE
Keyword(s):  
Belief Change ◽  
Syntactic Structure ◽  
Semantic Content ◽  
Rule Base ◽  
Stable Model ◽  
Logic Programs ◽  
Update Semantics ◽  
Specific Operator ◽  
Rule Bases ◽  
Answer Set

AbstractLogic programs under the stable model semantics, or answer-set programs, provide an expressive rule-based knowledge representation framework, featuring a formal, declarative and well-understood semantics. However, handling the evolution of rule bases is still a largely open problem. The Alchourrón, Gärdenfors and Makinson (AGM) framework for belief change was shown to give inappropriate results when directly applied to logic programs under a non-monotonic semantics such as the stable models. The approaches to address this issue, developed so far, proposed update semantics based on manipulating the syntactic structure of programs and rules.More recently, AGM revision has been successfully applied to a significantly more expressive semantic characterisation of logic programs based onSE-models. This is an important step, as it changes the focus from the evolution of a syntactic representation of a rule base to the evolution of its semantic content.In this paper, we borrow results from the area of belief update to tackle the problem of updating (instead of revising) answer-set programs. We prove a representation theorem which makes it possible to constructively define any operator satisfying a set of postulates derived from Katsuno and Mendelzon's postulates for belief update. We define a specific operator based on this theorem, examine its computational complexity and compare the behaviour of this operator with syntactic rule update semantics from the literature. Perhaps surprisingly, we uncover a serious drawback of all rule update operators based on Katsuno and Mendelzon's approach to update and onSE-models.

Sign in / Sign up

Export Citation Format

Share Document