Questo articolo introduce una nuova dimostrazione della decidibilita` del controllo di consistenza per i programmi FDNC sotto la semantica dei modelli stabili, basandosi su splitting sequences regolari. Con questa tecnica, riusciamo a rilassare leggermente la definizione di programmi FDNC e muoviamo un primo passo verso l’analisi delle relazioni tra programmi FDNC e la teoria dei programmi finitamente ricorsivi.
on regular splitting sequences. With this technique, we can slightly relax the definition of FDNC programs and make a first step towards a precise understanding of the relationships between FDNC programs and finitely recursive programs. 1
Some of the recent works of Alberto concern modal
extensions of logic programming [
Later results dropped this restriction. Finitary programs
[
FDNC programs [
In this paper we reformulate the decidability of the
consistency check for FDNC programs in terms of regular
splitting sequences. In this way we slightly generalize a
decidability result published in [
We assume the reader to be familiar with Logic
Programming and the stable model semantics [
Disjunctive logic programs are sets of (disjunctive) rules A1 ∨ A2 ∨ ... ∨ Am ← L1, ..., Ln (m > 0, n ≥ 0), where each Aj (j = 1, ..., m) is a logical atom and each Li (i = 1, ..., n) is a literal, that is, either a logical atom A or a negated atom not A.
If r is a rule with the above structure, then let head(r) = {A1, A2, ..., Am} and body(r) = {L1, ..., Ln}. Moreover, let body+(r) (respectively body−(r)) be the set of all atoms A s.t. A (respectively not A) belongs to body(r).
The ground instantiation of a program P is denoted by Ground(P ), and the set of atoms occurring in Ground(P ) is denoted by atom(P ). Similarly, atom(r) denotes the set of atoms occurring in a rule r.
A Herbrand model M of P is a stable model of P iff M ∈ lm(P M ), where lm(X) denotes the set of least models of a positive (possibly disjunctive) program X, and
from Ground(P ) by (i) removing all rules r such that body−(r) ∩ M 6= ∅, and (ii) removing all negative literals from the body of the remaining rules.
Disjunctive programs may have one, none, or multiple stable models. We say that a program is consistent if it has at least one stable model; otherwise the program is inconsistent. A skeptical consequence of a program P is any formula satisfied by all the stable models of P . A credulous consequence of P is any formula satisfied by at least one stable model of P .
rected graph, denoted by DG(P ), whose vertices are the ground atoms of P ’s language. Moreover, there exists an edge from A to B iff for some rule r ∈ Ground(P ), A ∈ head(r) and either B occurs in body(r), or B ∈ head(r).
An atom A depends on B if there is a directed path from A to B in the dependency graph.
A disjunctive program P is finitely recursive [
A FDNC program is a set of disjunctive rules conforming to any of the following schemata: (R1) A1(x) ∨ ... ∨ An(x) ← (not)B0(x), ..., (not)Bl(x) (R2) R1(x, y) ∨ ... ∨ Rn(x, y) ←
(not)P0(x, y), . . . , (not)Pl(x, y) (R3) R1(x, f1(x)) ∨ ... ∨ Rn(x, fn(x)) ←
(not)P0(x, g0(x)), . . . , (not)Pl(x, gl(x)) (R4) A1(y) ∨ ... ∨ An(y) ←
(not)B0(Z0), ..., (not)Bl(Zl), R(x, y) (R5) A1(f (x)) ∨ ... ∨ An(f (x)) ←
(not)B0(W0), ..., (not)Bl(Wl), R(x, f (x)) (R6) R1(x, f1(x)) ∨ ... ∨ Rn(x, fn(x)) ←
(not)B0(x), ..., (not)Bl(x) (R7) C1(~c1) ∨ ... ∨ Cn(~cn) ← (not)D1(d~1), ..., (not)Dl(d~l) where n, l ≥ 0, Zi ∈ {x, y}, Wi ∈ {x, f (x)}, and each ~ci, d~i is a tuple of one or two constants. Each rule r must be safe, i.e., each variable must occur in body+(r). Moreover at least one rule of type (R7) must be a fact.
Our results depend on a splitting theorem that allows to
construct stable models in stages. In turn, this theorem is
based on the notion of splitting set of a program P [
The partially evaluated complement of the bottom program determines the rest of each stable model. The partial evaluation of a ground logic program P with splitting set U w.r.t. a set of ground atoms X is the program eU (P, X) defined as follows: eU (P, X) = { r0 | there exists r ∈ P s.t.
(body+(r) ∩ U ) ⊆ X, (body−(r) ∩ U ) ∩ X = ∅, head(r0) = head(r), body+(r0) = body+(r) \ U, body−(r0) = body−(r) \ U } .
We are finally ready to formulate the splitting theorem.
Theorem 1 (Splitting theorem [
2. J is a stable model of eU (Ground(P ) \ botU (P ), I).
The splitting theorem has been extended to transfinite
sequences in [
A sequence hUαiα<μ of sets is monotone if Uα ⊆ Uβ whenever α < β, and continuous if, for each limit ordinal α < μ, Uα = Sν<α Uν . A sequence with μ = ω is smooth if each of its elements is finite.
Definition 2 [Lifschitz-Turner, [
Lifschitz and Turner generalized the splitting theorem to splitting sequences.
Theorem 3 (Splitting sequence theorem [
model of eUα−1 (botUα (P ) \ botUα−1 (P ), Sβ<α Mβ), 3. for all limit ordinals λ < μ, Mλ = ∅, 4. M = Sα<μ Uα. 3
We first observe that strictly speaking, FDNC programs are not always finitely recursive, due to the presence of local variables, i.e. variables that occur in the body of a rule and not in its head. Such variables arise in instances of rule schema (R4); in particular x occurs only in the body. However it is not hard to verify that the following proposition holds:
model of an FDNC program, then either u = f (t) for some function symbol f , or (t, u) is one of the vectors of constants ~ci occurring in the head of some instance of (R7).
It follows that each rule of the form (R4) can be replaced by a finite number of its instances: • one for each substitution [y/f (x)], where f is a function symbol occurring in the program; • one for each substitution [x/a1, y/a2] for each vector of constants ~ci = (a1, a2) occurring in the head of some instance of schema (R7).
By Proposition 4, such transformation preserves the set of stable models of the given FDNC program. Moreover, the transformation removes all local variables so the transformed program is a finitely recursive FDNC program. With a similar argument we can further normalize FDNC programs, restricting the set of atoms that may occur in a rule head. Each instance of schema (R2) can be replaced by a finite number of its instances by analogy with the previous case. By Proposition 4, such transformation preserves the set of stable models of the given FDNC program. Moreover, the transformation specializes the heads of the instances of (R2) so that the following lemma holds:
program with no rules of the form (R2) or (R4).
finitely recursive FDNC program P 0 such that the binary atoms occurring in Ground(P 0) are of the form R(t, f (t)) (for some function symbol f ) or R(~ci), where ~ci occurs in the head of some instance of (R7).
Note that the above program transformation can be effectively computed. Therefore, from now on, we shall focus without loss of generality on normal FDNC programs, that we define as programs whose rules conform to some of the schemata (R1), (R3), (R5), (R6), and (R7).
In the following, let P be a given normal FDNC program, and let us construct a suitable splitting sequence for P . First take any effective enumeration t1, t2, . . . , ti, . . . of the ground compound terms of P ’s language, such that each term ti precedes all the terms larger than ti (in terms of the number of function symbol occurrences). For all such ground terms ti, we shall denote by Uˆi the set of all ground atoms A(ti) and R(ti, f (ti)), for all function symbols f . Now a canonical splitting sequence for P can be defined as follows: • let U0 be the set of all atoms of the form A(c), R(c, d), or R(c, f (c)), where c and d are constants;
ˆ • let Ui+1 = Ui ∪ Ui+1.
Since P has no rules conforming to (R2) or (R4), it is easy to check that hUiii<ω is indeed a splitting sequence for Ground(P ).
Moreover, note that by definition, canonical sequences are smooth, as U0 and the sets Uˆi are all finite.
Another important property of canonical sequences is that the program slices Pi+1 = botUi+1 (P )\botUi (P ) they induce are all isomorphic to each other. By isomorphic, we mean that for all 0 < i < j < ω, Pj can be obtained from Pi by uniformly replacing ti with tj (in symbols, Pj = Pi[ti/tj]).
Now consider finite sequences of models hMiii<k with the following properties: • M0 is a stable model of botU0 (P ); • Mi+1 is a stable model of eUi (botUi+1 (P ) \ botUi (P ), Mi).
We say such a sequence is blocked if Mk = Mj[tj/tk] for some j such that 1 < j < k, that is, Mk can be obtained from Mj by replacing term tj with tk.
Lemma 7 Every blocked model sequence hMiii<k (induced by a canonical splitting sequence hUiii<ω for a normal FDNC program P ) can be extended to an infinite sequence hMiii<ω satisfying the following properties:
2. Mi+1 is a stable model of eUi (botUi+1 (P ) \ botUi (P ), Mi).
Roughly speaking, the idea simply consists in repeating the subsequence Mj, . . . , Mk−1 forever, replacing the terms tj, . . . , tk−1 as appropriate.
Proof. Let hMiii<k be a blocked sequence as described in the lemma’s statement. Point 1 follows immediately from the hypothesis, so we focus on point 2. Since hMiii<k is blocked, there exists j < k such that Mk = Mj[tj/tk]. For all i > k, let mi = j + (i − k) mod(k − j) and Mi = Mmi [tmi /ti]. Moreover, for all i ≥ 0 let Pi+1 = botUi+1 (P ) \ botUi (P ). As we already pointed out before this lemma, Pi = Pmi [tmi /ti]. Now, since both the program slices and the models with indexes i and mi are subject to the same symbol renaming, we have that eUi (Pi, Mi−1) = eUmi (Pmi , Mmi−1)[tmi /ti] . Since semantics does not depend on symbol names and by assumption Mmi is a stable model of eUmi (Pmi , Mmi−1) (as mi lies between j and k), we clearly have that Mi is a stable model of eUi (Pi, Mi−1); this proves point 2.
Now proving decidability is relatively easy. We start by characterizing satisfiability in terms of blocked sequences.
gram P iff M is the limit of the extension (in the sense of Lemma 7) of a blocked sequence hMiii<k (induced by a canonical splitting sequence hUiii<ω for P ).
Proof. (If ) Suppose M is the limit of a sequence hMiii<ω such that hMiii<k is a blocked sequence and such that: 1. M0 is a stable model of botU0 (P ); 2. Mi+1 is a stable model of eUi (botUi+1 (P ) \ botUi (P ), Mi).
Note that each program slice Pi+1 = botUi+1 (P ) \ botUi (P ) contains only atoms from Ui+1 \ Ui−1 (because P is a normal FDNC program). Therefore the partial evaluation of Pi+1 does not depend on the atoms in Ui−1, that is, for all i < ω, eUi (Pi+1, [ Mj) = eUi (Pi+1, Mi) .
j≤i Then properties 1 and 2 above entail the properties required by the splitting sequence theorem (for μ = ω). It follows that the limit M = Si<ω Mi is a stable model of P .
(Only if ) Suppose that M is a stable model of P . Let M0 = M ∩ U0 and for all i < ω, let Mi+1 = M ∩ (Ui+1 \ Ui). By the splitting theorem, M0 is a stable model of botU0 (P ). Moreover, by applying the splitting theorem twice for all i, we have that each Mi+1 is a stable model of eUi (botUi+1 (P ) \ botUi (P ), Sj≤i Mj ) that, as we pointed out in the If part of the proof, equals eUi (botUi+1 (P ) \ botUi (P ), Mi). Then we are only left to show that the sequence hMiii<ω contains a blocked prefix hMiii<k, that is, for some j and k such that 0 < j < k < ω, Mk = Mj [tj /tk].
To see this, observe that by definition for all i > 0, Mi is a subset of Uˆi, and Uˆi is isomorphic to Uˆ1, that is, Uˆi = Uˆ1[t1/ti] and |Ui| = |Uˆ1|. It follows that for all i > 0 ˆ there exists Si ⊆ Uˆ1 such that Mi = Si[t1/ti]. Since Uˆ1 is finite, there must be two indexes j and k and a set S ⊆ Uˆ1 such that 0 < j < k ≤ 2|Uˆ1|, Mj = S[t1/tj ], and Mk = S[t1/tk]. Consequently, Mk = S[t1/tj ][tj /tk] = Mj [tj /tk], which completes the proof.
model iff P has a blocked model sequence hMiii<k (induced by a canonical splitting sequence hUiii<ω for P ) with k ≤ 2|Uˆ1|.
consistent is decidable.
Proof. Consistency can be nondeterministically checked as follows: First normalize P . Next for i = 1, . . . , 2|Uˆ1|, build the program eUi (Pi+1, Mi) and pick up one of its stable models Mi+1; if no such model exists, then return false. Check whether Mi+1 is isomorphic to some previous Mj ; if so, return true. Otherwise repeat the loop, or return false if the end of the loop is reached. Clearly, this algorithm returns true in at least one run iff P has a blocked model sequence hMiii<k with k ≤ 2|Uˆ1|. By the above corollary, it follows that the algorithm solves the consistency problem for P .
Our results do not need all the restrictions placed on
FDNC programs. Proposition 4 holds even when the
program is not safe, provided that the rules conforming to (R2)
have nonempty bodies. The other proofs do not depend on
safeness. In this sense, our results are slightly more general
than those in [
We have given an alternative proof of a decidability
result of [
The term blocked is deliberately inspired by the notion of blocking in tableaux for modal and description logics. The intuitions in all these areas are analogous, and the goals are the same, namely decidable reasoning in the presence of infinite domains through a finite representation of infinite regular models.
We are planning to complete this investigation by characterizing credulous and skeptical reasoning and their computational complexity in terms of blocked model sequences. In particular, in order to provide effective reasoning methods, we are going to exploit the fact that normal FDNC programs are finitely recursive; for such programs the sequence of bottom programs induced by a smooth splitting ω-sequences is consistent iff the entire program is consistent. The consistency of the bottoms can be proved by (a suitable adaptation of) Lemma 7.
It will be interesting to inspect applications of these
ideas to modal extensions of logic programming, in the
spirit of [