scholarly journals On the complexity of index sets for finite predicate logic programs which allow function symbols

2020 ◽  
Vol 30 (1) ◽  
pp. 107-156
Author(s):  
D Cenzer ◽  
V W Marek ◽  
J B Remmel
Keyword(s):  
Positive Integer ◽  
Predicate Logic ◽  
Stable Model ◽  
Logic Programs ◽  
Index Set ◽  
Natural Properties ◽  
Index Sets ◽  
Predicate Language ◽  
Arithmetic Hierarchy ◽  
Stable Models

Abstract We study the recognition problem in the metaprogramming of finite normal predicate logic programs. That is, let $\mathcal{L}$ be a computable first-order predicate language with infinitely many constant symbols and infinitely many $n$-ary predicate symbols and $n$-ary functions symbols for all $n \geq 1$. Then we can effectively list all the finite normal predicate logic programs $Q_0,Q_1,\ldots $ over $\mathcal{L}$. Given some property $\mathcal{P}$ of finite normal predicate logic programs over $\mathcal{L}$, we define the index set $I_{\mathcal{P}}$ to be the set of indices $e$ such that $Q_e$ has property $\mathcal{P}$. We classify the complexity of the index set $I_{\mathcal{P}}$ within the arithmetic hierarchy for various natural properties of finite predicate logic programs. For example, we determine the complexity of the index sets relative to all finite predicate logic programs and relative to certain special classes of finite predicate logic programs of properties such as (i) having no stable models, (ii) having no recursive stable models, (iii) having at least one stable model, (iv) having at least one recursive stable model, (v) having exactly $c$ stable models for any given positive integer $c$, (vi) having exactly $c$ recursive stable models for any given positive integer $c$, (vii) having only finitely many stable models, (viii) having only finitely many recursive stable models, (ix) having infinitely many stable models and (x) having infinitely many recursive stable models.

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 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.

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 On the Splitting Property for Epistemic Logic Programs (Extended Abstract)

2020 ◽  
Author(s):  
Pedro Cabalar ◽  
Jorge Fandinno ◽  
Luis Fariñas del Cerro
Keyword(s):  
General Condition ◽  
Epistemic Logic ◽  
Stable Model ◽  
Logic Programs ◽  
Splitting Property ◽  
Conformant Planning ◽  
Planning Problems ◽  
Made In ◽  
Stable Models

Epistemic logic programs constitute an extension of the stable model semantics to deal with new constructs called "subjective literals." Informally speaking, a subjective literal allows checking whether some objective literal is true in all or some stable models. However, its associated semantics has proved to be non-trivial, since the truth of subjective literals may interfere with the set of stable models it is supposed to query. As a consequence, no clear agreement has been reached and different semantic proposals have been made in the literature. In this paper, we review an extension of the well-known splitting property for logic programs to the epistemic case. This "epistemic splitting property" is defined as a general condition that can be checked on any arbitrary epistemic semantics. Its satisfaction has desirable consequences both in the representation of conformant planning problems and in the encoding of the so-called subjective constraints.

scholarly journals On finitely recursive programs

2009 ◽  
Vol 9 (02) ◽  
pp. 213-238 ◽  
Author(s):  
SABRINA BASELICE ◽  
PIERO A. BONATTI ◽  
GIOVANNI CRISCUOLO
Keyword(s):  
Stable Model ◽  
Logic Programs ◽  
Compactness Property ◽  
Infinite Domains ◽  
Input Program ◽  
Recursive Programs ◽  
Splitting Sequence ◽  
Computational Properties ◽  
Stable Models

AbstractDisjunctivefinitary programsare a class of logic programs admitting function symbols and hence infinite domains. They have very good computational properties; for example, ground queries are decidable, while in the general case the stable model semantics are Π11-hard. In this paper we prove that a larger class of programs, calledfinitely recursive programs, preserve most of the good properties of finitary programs under the stable model semantics, which are as follows: (i) finitely recursive programs enjoy a compactness property; (ii) inconsistency checking and skeptical reasoning are semidecidable; (iii) skeptical resolution is complete for normal finitely recursive programs. Moreover, we show how to check inconsistency and answer skeptical queries using finite subsets of the ground program instantiation. We achieve this by extending the splitting sequence theorem by Lifschitz and Turner: we prove that if the input programPis finitely recursive, then the partial stable models determined by any smooth splitting ω-sequence converge to a stable model ofP.

scholarly journals Splitting Epistemic Logic Programs

2020 ◽  
pp. 1-21 ◽  
Author(s):  
PEDRO CABALAR ◽  
JORGE FANDINNO ◽  
LUIS FARIÑAS DEL CERRO
Keyword(s):  
Epistemic Logic ◽  
Stable Model ◽  
Logic Programs ◽  
Recent Proposal ◽  
Splitting Property ◽  
General Properties ◽  
Conformant Planning ◽  
Epistemic Constraints ◽  
Made In ◽  
Stable Models

Abstract Epistemic logic programs constitute an extension of the stable model semantics to deal with new constructs called subjective literals. Informally speaking, a subjective literal allows checking whether some objective literal is true in all or some stable models. As it can be imagined, the associated semantics has proved to be non-trivial, since the truth of subjective literals may interfere with the set of stable models it is supposed to query. As a consequence, no clear agreement has been reached and different semantic proposals have been made in the literature. Unfortunately, comparison among these proposals has been limited to a study of their effect on individual examples, rather than identifying general properties to be checked. In this paper, we propose an extension of the well-known splitting property for logic programs to the epistemic case. We formally define when an arbitrary semantics satisfies the epistemic splitting property and examine some of the consequences that can be derived from that, including its relation to conformant planning and to epistemic constraints. Interestingly, we prove (through counterexamples) that most of the existing approaches fail to fulfill the epistemic splitting property, except the original semantics proposed by Gelfond 1991 and a recent proposal by the authors, called Founded Autoepistemic Equilibrium Logic.

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 Characterizations of stable model semantics for logic programs with arbitrary constraint atoms

2009 ◽  
Vol 9 (4) ◽  
pp. 529-564 ◽  
Author(s):  
YI-DONG SHEN ◽  
JIA-HUAI YOU ◽  
LI-YAN YUAN
Keyword(s):  
The Body ◽  
Stable Model ◽  
Logic Programs ◽  
Abstract Representation ◽  
Disjunctive Logic Programs ◽  
The One ◽  
Answer Sets ◽  
Semantics Of Logic Programs ◽  
Natural Way ◽  
Stable Models

AbstractThis paper studies the stable model semantics of logic programs with (abstract) constraint atoms and their properties. We introduce a succinct abstract representation of these constraint atoms in which a constraint atom is represented compactly. We show two applications. First, under this representation of constraint atoms, we generalize the Gelfond–Lifschitz transformation and apply it to define stable models (also called answer sets) for logic programs with arbitrary constraint atoms. The resulting semantics turns out to coincide with the one defined by Son et al. (2007), which is based on a fixpoint approach. One advantage of our approach is that it can be applied, in a natural way, to define stable models for disjunctive logic programs with constraint atoms, which may appear in the disjunctive head as well as in the body of a rule. As a result, our approach to the stable model semantics for logic programs with constraint atoms generalizes a number of previous approaches. Second, we show that our abstract representation of constraint atoms provides a means to characterize dependencies of atoms in a program with constraint atoms, so that some standard characterizations and properties relying on these dependencies in the past for logic programs with ordinary atoms can be extended to logic programs with constraint atoms.

Sign in / Sign up

Export Citation Format

Share Document