Il Milione: A Journey in the Computational Logic in Italy




Sulla decidibilità di programmi FDNC
On the decidability of FDNC programs
                     P. A. Bonatti




                               55
                             Il Milione: A Journey in the Computational Logic in Italy




SOMMARIO/ABSTRACT                                                          FDNC programs [8] adopt a different strategy. They
                                                                        restrict the syntax to (a skolemized form of) 2-variable
Questo articolo introduce una nuova dimostrazione della                 guarded logic and avoid the restrictions on cycles and con-
decidibilità del controllo di consistenza per i programmi              straints.
FDNC sotto la semantica dei modelli stabili, basandosi su                  In this paper we reformulate the decidability of the con-
splitting sequences regolari. Con questa tecnica, riusciamo             sistency check for FDNC programs in terms of regular
a rilassare leggermente la definizione di programmi                     splitting sequences. In this way we slightly generalize a
FDNC e muoviamo un primo passo verso l’analisi delle                    decidability result published in [8].
relazioni tra programmi FDNC e la teoria dei programmi
finitamente ricorsivi.
                                                                        2    Preliminaries
We provide a new decidability proof for the consistency of
                                                                        We assume the reader to be familiar with Logic Program-
FDNC programs under the stable model semantics, based
                                                                        ming and the stable model semantics [2]
on regular splitting sequences. With this technique, we can
                                                                          Disjunctive logic programs are sets of (disjunctive) rules
slightly relax the definition of FDNC programs and make
a first step towards a precise understanding of the rela-
                                                                            A1 ∨ A2 ∨ ... ∨ Am ← L1 , ..., Ln      (m > 0, n ≥ 0),
tionships between FDNC programs and finitely recursive
programs.                                                               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
Keywords: Answer set programming, finitely recursive,                   a negated atom not A.
finitary, and FDNC programs, module sequences.                             If r is a rule with the above structure, then let head(r) =
                                                                        {A1 , A2 , ..., Am } and body(r) = {L1 , ..., Ln }. More-
1 Introduction                                                          over, let body + (r) (respectively body − (r)) be the set of all
                                                                        atoms A s.t. A (respectively not A) belongs to body(r).
Some of the recent works of Alberto concern modal exten-                   The ground instantiation of a program P is denoted
sions of logic programming [5, 1]. A major motivation for               by Ground(P ), and the set of atoms occurring in
those programs is reasoning about actions and change. In                Ground(P ) is denoted by atom(P ). Similarly, atom(r)
this setting, nonmonotonic constructs such as negation as               denotes the set of atoms occurring in a rule r.
failure are extremely useful to encode compactly the frame                 A Herbrand model M of P is a stable model of P iff
axiom and action consequences. However, for a long time                 M ∈ lm(P M ), where lm(X) denotes the set of least mod-
such features could be supported only by forbidding func-               els of a positive (possibly disjunctive) program X, and
tion symbols, in order to ensure decidability.                          P M is the Gelfond-Lifschitz transformation of P , obtained
   Later results dropped this restriction. Finitary programs            from Ground(P ) by (i) removing all rules r such that
[4] preserve decidability even in the presence of infinite              body − (r) ∩ M 6= ∅, and (ii) removing all negative liter-
domains. This is achieved at the cost of restrictions on the            als from the body of the remaining rules.
cycles in dependency graphs containing an odd number of                    Disjunctive programs may have one, none, or multiple
negative edges. Such limitations imply restrictions on the              stable models. We say that a program is consistent if it has
constraints (in the form of denials like ← A1 , . . . , An , for        at least one stable model; otherwise the program is incon-
example) that can be encoded in a finitary program.                     sistent. A skeptical consequence of a program P is any

                                                                   56
                                      Il Milione: A Journey in the Computational Logic in Italy




formula satisfied by all the stable models of P . A credu-                    2. J is a stable model of eU (Ground(P ) \ botU (P ), I).
lous consequence of P is any formula satisfied by at least
one stable model of P .                                                      The splitting theorem has been extended to transfinite
   The dependency graph of a program P is a labelled di-                  sequences in [7]. A (transfinite) sequence is a family
rected graph, denoted by DG(P ), whose vertices are the                   whose index set is an initial segment of ordinals, {α :
ground atoms of P ’s language. Moreover, there exists an                  α < µ}. The ordinal µ is the length of the sequence.
edge from A to B iff for some rule r ∈ Ground(P ), A ∈                       A sequence hUα iα<µ of sets is monotone if Uα ⊆ Uβ
head(r) and either B occurs in body(r), or B ∈ head(r).                   whenever α <Sβ, and continuous if, for each limit ordinal
   An atom A depends on B if there is a directed path from                α < µ, Uα = ν<α Uν . A sequence with µ = ω is smooth
A to B in the dependency graph.                                           if each of its elements is finite.
   A disjunctive program P is finitely recursive [4, 3] iff
                                                                          Definition 2 [Lifschitz-Turner, [7]] A splitting sequence
each ground atom A depends on finitely many ground
                                                                          for a program P is a monotone,Scontinuous sequence
atoms in DG(P ).
                                                                          hUα iα<µ of splitting sets for P s.t. α<µ Uα = atom(P ).
   A FDNC program is a set of disjunctive rules conform-
ing to any of the following schemata:                                       Lifschitz and Turner generalized the splitting theorem to
 (R1) A1 (x) ∨ ... ∨ An (x) ← (not)B0 (x), ..., (not)Bl (x)               splitting sequences.
 (R2) R1 (x, y) ∨ ... ∨ Rn (x, y) ←
                     (not)P0 (x, y), . . . , (not)Pl (x, y)
                                                                          Theorem 3 (Splitting sequence theorem [7]) Let P be a
 (R3) R1 (x, f1 (x)) ∨ ... ∨ Rn (x, fn (x)) ←                             disjunctive program. M is a stable model of P iff there
                     (not)P0 (x, g0 (x)), . . . , (not)Pl (x, gl (x))     exists a splitting sequence hUα iα<µ such that
 (R4) A1 (y) ∨ ... ∨ An (y) ←
                     (not)B0 (Z0 ), ..., (not)Bl (Zl ), R(x, y)
                                                                              1. M0 is a stable model of botU0 (P ),
 (R5) A1 (f (x)) ∨ ... ∨ An (f (x)) ←                                         2. for all successor ordinals α < µ, MαSis a stable
                     (not)B0 (W0 ), ..., (not)Bl (Wl ), R(x, f (x))
                                                                                 model of eUα−1 (botUα (P ) \ botUα−1 (P ), β<α Mβ ),
 (R6) R1 (x, f1 (x)) ∨ ... ∨ Rn (x, fn (x)) ←
                     (not)B0 (x), ..., (not)Bl (x)                            3. for all limit ordinals λ < µ, Mλ = ∅,
 (R7) C1 (~c1 ) ∨ ... ∨ Cn (~cn ) ← (not)D1 (d~1 ), ..., (not)Dl (d~l )                 S
                                                                              4. M = α<µ Uα .
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              3     Revised decidability results
at least one rule of type (R7) must be a fact.                            We first observe that strictly speaking, FDNC programs are
    Our results depend on a splitting theorem that allows to              not always finitely recursive, due to the presence of local
construct stable models in stages. In turn, this theorem is               variables, i.e. variables that occur in the body of a rule and
based on the notion of splitting set of a program P [2],[6],              not in its head. Such variables arise in instances of rule
that is, any set U of atoms such that, for all rules r ∈                  schema (R4); in particular x occurs only in the body. How-
Ground(P ), if head(r) ∩ U 6= ∅ then atom(r) ⊆ U . The                    ever it is not hard to verify that the following proposition
set of rules r ∈ Ground(P ) such that head(r) ∩ U 6= ∅ is                 holds:
called the bottom of P relative to the splitting set U and is
denoted by botU (P ).                                                     Proposition 4 If an atom R(t, u) belongs to a stable
    The partially evaluated complement of the bottom pro-                 model of an FDNC program, then either u = f (t) for some
gram determines the rest of each stable model. The partial                function symbol f , or (t, u) is one of the vectors of con-
evaluation of a ground logic program P with splitting set                 stants ~ci occurring in the head of some instance of (R7).
U w.r.t. a set of ground atoms X is the program eU (P, X)
defined as follows:                                                         It follows that each rule of the form (R4) can be replaced
                                                                          by a finite number of its instances:
  eU (P, X) = { r0 | there exists r ∈ P s.t.
    (body + (r) ∩ U ) ⊆ X, (body − (r) ∩ U ) ∩ X = ∅,                         • one for each substitution [y/f (x)], where f is a func-
    head(r0 ) = head(r), body + (r0 ) = body + (r) \ U,                         tion symbol occurring in the program;
    body − (r0 ) = body − (r) \ U } .
                                                                              • one for each substitution [x/a1 , y/a2 ] for each vector
We are finally ready to formulate the splitting theorem.                        of constants ~ci = (a1 , a2 ) occurring in the head of
                                                                                some instance of schema (R7).
Theorem 1 (Splitting theorem [6]) Let U be a splitting
set for a logic program P . An interpretation M is a stable               By Proposition 4, such transformation preserves the set
model of P iff M = J ∪ I, where                                           of stable models of the given FDNC program. Moreover,
                                                                          the transformation removes all local variables so the trans-
 1. I is a stable model of botU (P ), and                                 formed program is a finitely recursive FDNC program.

                                                                              57
                               Il Milione: A Journey in the Computational Logic in Italy




   With a similar argument we can further normalize                          We say such a sequence is blocked if Mk = Mj [tj /tk ] for
FDNC programs, restricting the set of atoms that may oc-                     some j such that 1 < j < k, that is, Mk can be obtained
cur in a rule head. Each instance of schema (R2) can be re-                  from Mj by replacing term tj with tk .
placed by a finite number of its instances by analogy with
the previous case. By Proposition 4, such transformation                     Lemma 7 Every blocked model sequence hMi ii<k (in-
preserves the set of stable models of the given FDNC pro-                    duced by a canonical splitting sequence hUi ii<ω for a nor-
gram. Moreover, the transformation specializes the heads                     mal FDNC program P ) can be extended to an infinite se-
of the instances of (R2) so that the following lemma holds:                  quence hMi ii<ω satisfying the following properties:
                                                                              1. M0 is a stable model of botU0 (P );
Lemma 5 Every FDNC program is equivalent to a FDNC
program with no rules of the form (R2) or (R4).                               2. Mi+1 is a stable model of eUi (botUi+1 (P ) \
                                                                                 botUi (P ), Mi ).
Corollary 6 Every FDNC program P is equivalent to a
finitely recursive FDNC program P 0 such that the binary                        Roughly speaking, the idea simply consists in repeat-
atoms occurring in Ground(P 0 ) are of the form R(t, f (t))                  ing the subsequence Mj , . . . , Mk−1 forever, replacing the
(for some function symbol f ) or R(~ci ), where ~ci occurs in                terms tj , . . . , tk−1 as appropriate.
the head of some instance of (R7).
                                                                             Proof. Let hMi ii<k be a blocked sequence as described in
   Note that the above program transformation can be ef-                     the lemma’s statement. Point 1 follows immediately from
fectively computed. Therefore, from now on, we shall fo-                     the hypothesis, so we focus on point 2. Since hMi ii<k is
cus without loss of generality on normal FDNC programs,                      blocked, there exists j < k such that Mk = Mj [tj /tk ].
that we define as programs whose rules conform to some                       For all i > k, let mi = j + (i − k) mod(k − j) and
of the schemata (R1), (R3), (R5), (R6), and (R7).                            Mi = Mmi [tmi /ti ]. Moreover, for all i ≥ 0 let Pi+1 =
   In the following, let P be a given normal FDNC pro-                       botUi+1 (P ) \ botUi (P ). As we already pointed out before
gram, and let us construct a suitable splitting sequence for                 this lemma, Pi = Pmi [tmi /ti ]. Now, since both the pro-
P . First take any effective enumeration t1 , t2 , . . . , ti , . . .        gram slices and the models with indexes i and mi are sub-
of the ground compound terms of P ’s language, such that                     ject to the same symbol renaming, we have that
each term ti precedes all the terms larger than ti (in terms
                                                                                  eUi (Pi , Mi−1 ) = eUmi (Pmi , Mmi −1 )[tmi /ti ] .
of the number of function symbol occurrences). For all
such ground terms ti , we shall denote by Ûi the set of all                 Since semantics does not depend on symbol names and by
ground atoms A(ti ) and R(ti , f (ti )), for all function sym-               assumption Mmi is a stable model of eUmi (Pmi , Mmi −1 )
bols f . Now a canonical splitting sequence for P can be                     (as mi lies between j and k), we clearly have that Mi is a
defined as follows:                                                          stable model of eUi (Pi , Mi−1 ); this proves point 2.
  • let U0 be the set of all atoms of the form A(c), R(c, d),                  Now proving decidability is relatively easy. We start by
    or R(c, f (c)), where c and d are constants;                             characterizing satisfiability in terms of blocked sequences.
  • let Ui+1 = Ui ∪ Ûi+1 .                                                  Theorem 8 M is a stable model of a normal FDNC pro-
                                                                             gram P iff M is the limit of the extension (in the sense of
Since P has no rules conforming to (R2) or (R4), it is easy
                                                                             Lemma 7) of a blocked sequence hMi ii<k (induced by a
to check that hUi ii<ω is indeed a splitting sequence for
                                                                             canonical splitting sequence hUi ii<ω for P ).
Ground(P ).
   Moreover, note that by definition, canonical sequences                    Proof. (If ) Suppose M is the limit of a sequence hMi ii<ω
are smooth, as U0 and the sets Ûi are all finite.                           such that hMi ii<k is a blocked sequence and such that:
   Another important property of canonical sequences is
that the program slices Pi+1 = botUi+1 (P )\botUi (P ) they                   1. M0 is a stable model of botU0 (P );
induce are all isomorphic to each other. By isomorphic, we
                                                                              2. Mi+1 is a stable model of eUi (botUi+1 (P ) \
mean that for all 0 < i < j < ω, Pj can be obtained from
                                                                                 botUi (P ), Mi ).
Pi by uniformly replacing ti with tj (in symbols, Pj =
Pi [ti /tj ]).                                                               Note that each program slice Pi+1 = botUi+1 (P ) \
   Now consider finite sequences of models hMi ii<k with                     botUi (P ) contains only atoms from Ui+1 \ Ui−1 (because
the following properties:                                                    P is a normal FDNC program). Therefore the partial eval-
                                                                             uation of Pi+1 does not depend on the atoms in Ui−1 , that
  • M0 is a stable model of botU0 (P );                                      is, for all i < ω,
                                                                                                      [
  • Mi+1 is a stable model of eUi (botUi+1 (P ) \                                         eUi (Pi+1 ,   Mj ) = eUi (Pi+1 , Mi ) .
    botUi (P ), Mi ).                                                                             j≤i

                                                                        58
                                    Il Milione: A Journey in the Computational Logic in Italy




Then properties 1 and 2 above entail the properties re-              of the finite programs eUi (Pi+1 , Mi ). Such a regular se-
quired by the splitting sequence  S theorem (for µ = ω). It          quence can be finitely represented by a blocked sequence
follows that the limit M = i<ω Mi is a stable model of               hMi ii<k .
P.                                                                      The term blocked is deliberately inspired by the notion
   (Only if ) Suppose that M is a stable model of P . Let            of blocking in tableaux for modal and description logics.
M0 = M ∩ U0 and for all i < ω, let Mi+1 = M ∩                        The intuitions in all these areas are analogous, and the
(Ui+1 \ Ui ). By the splitting theorem, M0 is a stable               goals are the same, namely decidable reasoning in the pres-
model of botU0 (P ). Moreover, by applying the split-                ence of infinite domains through a finite representation of
ting theorem twice for all i, we have that eachSMi+1 is              infinite regular models.
a stable model of eUi (botUi+1 (P ) \ botUi (P ), j≤i Mj )              We are planning to complete this investigation by char-
that, as we pointed out in the If part of the proof, equals          acterizing credulous and skeptical reasoning and their
eUi (botUi+1 (P ) \ botUi (P ), Mi ). Then we are only left to       computational complexity in terms of blocked model se-
show that the sequence hMi ii<ω contains a blocked prefix            quences. In particular, in order to provide effective reason-
hMi ii<k , that is, for some j and k such that 0 < j < k <           ing methods, we are going to exploit the fact that normal
ω, Mk = Mj [tj /tk ].                                                FDNC programs are finitely recursive; for such programs
   To see this, observe that by definition for all i > 0, Mi         the sequence of bottom programs induced by a smooth
is a subset of Ûi , and Ûi is isomorphic to Û1 , that is, Ûi =   splitting ω-sequences is consistent iff the entire program is
Û1 [t1 /ti ] and |Ûi | = |Û1 |. It follows that for all i > 0     consistent. The consistency of the bottoms can be proved
there exists Si ⊆ Û1 such that Mi = Si [t1 /ti ]. Since             by (a suitable adaptation of) Lemma 7.
Û1 is finite, there must be two indexes j and k and a set              It will be interesting to inspect applications of these
S ⊆ Û1 such that 0 < j < k ≤ 2|Û1 | , Mj = S[t1 /tj ], and         ideas to modal extensions of logic programming, in the
Mk = S[t1 /tk ]. Consequently, Mk = S[t1 /tj ][tj /tk ] =            spirit of [5], possibly exploiting the translation in [1].
Mj [tj /tk ], which completes the proof.
                                                                     REFERENCES
Corollary 9 A normal FDNC program P has a stable
model iff P has a blocked model sequence hMi ii<k (in-               [1] M. Baldoni, L. Giordano, and A. Martelli. Translat-
duced by a canonical splitting sequence hUi ii<ω for P )                 ing a modal language with embedded implication into
with k ≤ 2|Û1 | .                                                       horn clause logic. In ELP, volume 1050 of LNCS,
                                                                         pages 19–33. Springer, 1996.
Corollary 10 Deciding whether a FDNC program P is
consistent is decidable.                                             [2] C. Baral. Knowledge Representation, Reasoning and
                                                                         Declarative Problem Solving. Cambridge University
Proof. Consistency can be nondeterministically checked                   Press, Cambridge, 2003.
as follows: First normalize P . Next for i = 1, . . . , 2|Û1 | ,
build the program eUi (Pi+1 , Mi ) and pick up one of its            [3] S. Baselice, P.A. Bonatti, and G. Criscuolo. On finitely
stable models Mi+1 ; if no such model exists, then return                recursive programs. In ICLP 2007, volume 4670 of
false. Check whether Mi+1 is isomorphic to some previous                 LNCS, pages 89–103. Springer, 2007.
Mj ; if so, return true. Otherwise repeat the loop, or return        [4] Piero A. Bonatti. Reasoning with infinite stable mod-
false if the end of the loop is reached. Clearly, this algo-             els. Artif. Intell., 156(1):75–111, 2004.
rithm returns true in at least one run iff P has a blocked
model sequence hMi ii<k with k ≤ 2|Û1 | . By the above              [5] Laura Giordano, Alberto Martelli, and Camilla
corollary, it follows that the algorithm solves the consis-              Schwind. Ramification and causality in a modal ac-
tency problem for P .                                                    tion logic. J. Log. Comput., 10(5):625–662, 2000.

   Our results do not need all the restrictions placed on            [6] V. Lifschitz and H. Turner. Splitting a Logic Program.
FDNC programs. Proposition 4 holds even when the pro-                    In Proc. of the 12th Int. Conf. on Logic Programming,
gram is not safe, provided that the rules conforming to (R2)             MIT Press Series Logic Program, pages 581–595. MIT
have nonempty bodies. The other proofs do not depend on                  Press, 1995.
safeness. In this sense, our results are slightly more general
                                                                     [7] Vladimir Lifschitz and Hudson Turner. Splitting a
than those in [8].
                                                                         logic program. In International Conference on Logic
                                                                         Programming, pages 23–37, 1994.
4    Conclusions and future work
                                                                     [8] M. Simkus and T. Eiter. FDNC: Decidable non-
We have given an alternative proof of a decidability re-                 monotonic disjunctive logic programs with function
sult of [8] for FDNC programs by proving that a consistent               symbols. In LPAR 2007, volume 4790 of Lecture Notes
normal FDNC program has always a stable model which is                   in Computer Science, pages 514–530. Springer, 2007.
the limit of a regular sequence hMi ii<ω of stable models

                                                                       59