scholarly journals Disjunctive ASP with functions: Decidable queries and effective computation

2010 ◽  
Vol 10 (4-6) ◽  
pp. 497-512 ◽  
Author(s):  
MARIO ALVIANO ◽  
WOLFGANG FABER ◽  
NICOLA LEONE
Keyword(s):  
Query Answering ◽  
Query Evaluation ◽  
Stable Model ◽  
Logic Programs ◽  
Disjunctive Logic Programs ◽  
Magic Set

AbstractQuerying over disjunctive ASP with functions is a highly undecidable task in general. In this paper we focus on disjunctive logic programs with stratified negation and functions under the stable model semantics (ASPfs). We show that query answering in this setting is decidable, if the query is finitely recursive (ASPfsfr). Our proof yields also an effective method for query evaluation. It is done by extending the magic set technique to ASPfsfr. We show that the magic-set rewritten program is query equivalent to the original one (under both brave and cautious reasoning). Moreover, we prove that the rewritten program is also finitely ground, implying that it is decidable. Importantly, finitely ground programs are evaluable using existing ASP solvers, making the class of ASPfsfr queries usable in practice.

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.

scholarly journals Modularity Aspects of Disjunctive Stable Models

2009 ◽  
Vol 35 ◽  
pp. 813-857 ◽  
Author(s):  
T. Janhunen ◽  
E. Oikarinen ◽  
H. Tompits ◽  
S. Woltran
Keyword(s):  
Programming Languages ◽  
Connected Components ◽  
Stable Model ◽  
Logic Programs ◽  
Strongly Connected Components ◽  
Verification Method ◽  
Strongly Connected ◽  
Disjunctive Logic Programs ◽  
Mutual Comparison ◽  
Output Interface

Practically all programming languages allow the programmer to split a program into several modules which brings along several advantages in software development. In this paper, we are interested in the area of answer-set programming where fully declarative and nonmonotonic languages are applied. In this context, obtaining a modular structure for programs is by no means straightforward since the output of an entire program cannot in general be composed from the output of its components. To better understand the effects of disjunctive information on modularity we restrict the scope of analysis to the case of disjunctive logic programs (DLPs) subject to stable-model semantics. We define the notion of a DLP-function, where a well-defined input/output interface is provided, and establish a novel module theorem which indicates the compositionality of stable-model semantics for DLP-functions. The module theorem extends the well-known splitting-set theorem and enables the decomposition of DLP-functions given their strongly connected components based on positive dependencies induced by rules. In this setting, it is also possible to split shared disjunctive rules among components using a generalized shifting technique. The concept of modular equivalence is introduced for the mutual comparison of DLP-functions using a generalization of a translation-based verification method.

scholarly journals Justifications for programs with disjunctive and causal-choice rules

2016 ◽  
Vol 16 (5-6) ◽  
pp. 587-603 ◽  
Author(s):  
PEDRO CABALAR ◽  
JORGE FANDINNO
Keyword(s):  
Choice Rule ◽  
Algebraic Expression ◽  
Stable Model ◽  
Logic Programs ◽  
Causal Information ◽  
Disjunctive Logic Programs ◽  
New Type ◽  
Algebraic Operations ◽  
Disjunctive Programs ◽  
Stable Models

AbstractIn 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 ofcausal stable modelto 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 callcausal-choice. This type of rule intuitively captures the idea of “Amay causeB” and, when causal information is disregarded, amounts to a usual choice rule under the standard stable model semantics.

scholarly journals Transformation-based bottom-up computation of the well-founded model

2001 ◽  
Vol 1 (5) ◽  
pp. 497-538 ◽  
Author(s):  
STEFAN BRASS ◽  
JÜRGEN DIX ◽  
BURKHARD FREITAG ◽  
ULRICH ZUKOWSKI
Keyword(s):  
Real Life ◽  
Transformation Method ◽  
Program Transformations ◽  
Logic Programs ◽  
Bottom Up ◽  
Magic Sets ◽  
Disjunctive Logic Programs ◽  
Carry Over ◽  
Magic Set ◽  
New Strategies

We present a framework for expressing bottom-up algorithms to compute the well-founded model of non-disjunctive logic programs. Our method is based on the notion of conditional facts and elementary program transformations studied by BRASS and DIX (Brass and Dix, 1994; Brass and Dix, 1999) for disjunctive programs. However, even if we restrict their framework to nondisjunctive programs, their ‘residual program’ can grow to exponential size, whereas for function-free programs our ‘program remainder’ is always polynomial in the size of the extensional database (EDB). We show that particular orderings of our transformations (we call them strategies) correspond to well-known computational methods like the alternating fixpoint approach (Van Gelder, 1989; Van Gelder, 1993), the well-founded magic sets method (Kemp et al., 1995) and the magic alternating fixpoint procedure (Morishita, 1996). However, due to the confluence of our calculi (first noted in Brass and Dix, 1998), we come up with computations of the well-founded model that are provably better than these methods. In contrast to other approaches, our transformation method treats magic set transformed programs correctly, i.e. it always computes a relevant part of the well-founded model of the original program. These results show that our approach is a valuable tool to analyze, compare, and optimize existing evaluation methods or to create new strategies that are automatically proven to be correct if they can be described by a sequence of transformations in our framework. We have also developed a prototypical implementation. Experiments illustrate that the theoretical results carry over to the implemented prototype and may be used to optimize real life systems.

Disjunctive logic programs with existential quantification in rule heads

2013 ◽  
Vol 13 (4-5) ◽  
pp. 563-578 ◽  
Author(s):  
JIA-HUAI YOU ◽  
HENG ZHANG ◽  
YAN ZHANG
Keyword(s):  
Stable Model ◽  
Logic Programs ◽  
Disjunctive Logic Programs ◽  
Decidable Fragment ◽  
Definition Of ◽  
Existential Quantification ◽  
Disjunctive Programs ◽  
Second Order Logic ◽  
Stable Models

AbstractWe consider disjunctive logic programs without function symbols but with existential quantification in rule heads, under the semantics of general stable models. There are at least two interesting prospects in these programs. The first is that a program can be made more succinct by using existential variables, and the second is on the potential in representing defeasible ontological knowledge by these logic programs. This paper studies some of the properties of these programs. First, we show a simple yet intuitive definition of stable models for these programs that does not resort to second-order logic. Second, the stable models of these programs can be characterized by an extension of progression for disjunctive programs, which provides a native characterization of justification for stable models. We then study the decidability issue. While the stable model existence problem for safe disjunctive programs is decidable, with existential quantification allowed in rule heads the problem becomes undecidable. We identify an interesting decidable fragment by exploring a new notion of stratification over existential quantification.

scholarly journals Thirty years of Epistemic Specifications

2021 ◽  
pp. 1-41
Author(s):  
JORGE FANDINNO ◽  
WOLFGANG FABER ◽  
MICHAEL GELFOND
Keyword(s):  
State Of The Art ◽  
World View ◽  
Formal Semantics ◽  
Future Research ◽  
Knowledge Representation And Reasoning ◽  
Stable Model ◽  
Logic Programs ◽  
Current State ◽  
Closed World ◽  
Disjunctive Logic Programs

Abstract The language of epistemic specifications and epistemic logic programs extends disjunctive logic programs under the stable model semantics with modal constructs called subjective literals. Using subjective literals, it is possible to check whether a regular literal is true in every or some stable models of the program, those models, in this context also called belief sets, being collected in a set called world view. This allows for representing, within the language, whether some proposition should be understood accordingly to the open or the closed world assumption. Several attempts for capturing the intuitions underlying the language by means of a formal semantics were given, resulting in a multitude of proposals that makes it difficult to understand the current state of the art. In this article, we provide an overview of the inception of the field and the knowledge representation and reasoning tasks it is suitable for. We also provide a detailed analysis of properties of proposed semantics, and an outlook of challenges to be tackled by future research in the area.

scholarly journals Extending Well-Founded Semantics with Clark’s Completion for Disjunctive Logic Programs

2018 ◽  
Vol 2018 ◽  
pp. 1-10
Author(s):  
Juan Carlos Nieves ◽  
Mauricio Osorio
Keyword(s):  
Aggregation Operator ◽  
Stable Model ◽  
Logic Programs ◽  
Complete Lattices ◽  
Transformation Rules ◽  
Disjunctive Program ◽  
Stable Semantics ◽  
Disjunctive Logic Programs ◽  
Disjunctive Programs ◽  
Explicit Negation

In this paper, we introduce new semantics (that we call D3-WFS-DCOMP) and compare it with the stable semantics (STABLE). For normal programs, this semantics is based onsuitableintegration of the well-founded semantics (WFS) and the Clark’s completion. D3-WFS-DCOM has the following appealing properties: First, it agrees with STABLE in the sense that it never defines a nonminimal model or a nonminimal supported model. Second, for normal programs it extends WFS. Third, every stable model of a disjunctive programPis a D3-WFS-DCOM model ofP. Fourth, it is constructed using transformation rules accepted by STABLE. We also introduce second semantics that we call D2-WFS-DCOMP. We show that D2-WFS-DCOMP is equivalent to D3-WFS-DCOMP for normal programs but this is not the case for disjunctive programs. We also introduce third new semantics that supports the use of implicit disjunctions. We illustrate how these semantics can be extended to programs including explicit negation, default negation in the head of a clause, and aluboperator, which is a generalization of the aggregation operatorsetofover arbitrary complete lattices.

scholarly journals Enhancing Magic Sets with an Application to Ontological Reasoning

2019 ◽  
Vol 19 (5-6) ◽  
pp. 654-670
Author(s):  
MARIO ALVIANO ◽  
NICOLA LEONE ◽  
PIERFRANCESCO VELTRI ◽  
JESSICA ZANGARI
Keyword(s):  
Program Evaluation ◽  
Query Answering ◽  
Stable Model ◽  
Efficient Computation ◽  
Ontological Reasoning ◽  
Input Program ◽  
Magic Sets ◽  
Magic Set ◽  
The Given ◽  
Recursive Definitions

AbstractMagic sets are a Datalog to Datalog rewriting technique to optimize query answering. The rewritten program focuses on a portion of the stable model(s) of the input program which is sufficient to answer the given query. However, the rewriting may introduce new recursive definitions, which can involve even negation and aggregations, and may slow down program evaluation. This paper enhances the magic set technique by preventing the creation of (new) recursive definitions in the rewritten program. It turns out that the new version of magic sets is closed for Datalog programs with stratified negation and aggregations, which is very convenient to obtain efficient computation of the stable model of the rewritten program. Moreover, the rewritten program is further optimized by the elimination of subsumed rules and by the efficient handling of the cases where binding propagation is lost. The research was stimulated by a challenge on the exploitation of Datalog/dlv for efficient reasoning on large ontologies. All proposed techniques have been hence implemented in the dlv system, and tested for ontological reasoning, confirming their effectiveness.

Sign in / Sign up

Export Citation Format

Share Document