Forest Logic Programs (FoLP) are a decidable fragment of Open Answer Set Programming (OASP) which have the forest model property. OASP extends Answer Set Programming (ASP) with open domains-a feature which makes it possible for FoLPs to simulate reasoning with the expressive description logic SHOQ. At the same time, the fragment retains the attractive rule syntax and the non-monotonicity specific to ASP. In the past, several tableaux algorithms have been devised to reason with FoLPs, the most recent of which established a NEXPTIME upper bound for reasoning with the fragment. While known to be EXPTIME-hard, the exact complexity characterization of reasoning with the fragment was still unknown. In this paper we settle this open question by a reduction of reasoning with FoLPs to emptiness checking of fully enriched automata, a form of automata which run on forests, and which are known to be EXPTIME-complete.
Programming (ASP)
et al. 2008), Description Logic Rules
Copyright c 2015 for this paper by its authors. Copying permitted for private and academic purposes.
several fragments have been defined by imposing syntactical restrictions on the shape of rules. Such a fragment are
property: a unary predicate is satisfiable iff it is satisfied by a model that can be represented as a labeled forest, where nodes and arcs are labeled with sets of unary predicates and binary predicates, respectively.
FoLPs are quite an expressive fragment as they allow, for
instance, the simulation of standard reasoning tasks (like
concept satisfiability and KB consistency) with SHOQ
ontologies
known individuals in the rule component. As f-hybrid KBs are based on the simulation of SHOQ KBs within FoLPs, no such restriction is needed. Conceptual modeling using
(ORM) models as sets of FoLP rules, e.g.
Logic (DL) SHOQ, it follows that reasoning with FoLPs
is EXPTIME-hard. However, the exact complexity
characterization of FoLPs was still open. Previously, reasoning
with FoLPs was addressed by means of tableau-based
algorithms:
In this paper, we settle the open question regarding the exact complexity characterization of FoLPs: by using a reduction to emptiness checking of Fully Enriched Automata (FEAs), we show that satisfiability checking of unary predicates w.r.t. FoLPs is EXPTIME-complete. Hence, reasoning with FoLP rules and SHOQ ontologies is not harder than reasoning with SHOQ ontologies themselves.
Fully enriched automata have been introduced in
to reason with CoLPs (Heymans, Van Nieuwenborgh, and
w.r.t. a CoLP has been reduced to non-emptiness checking
of two-way alternating tree automata (2ATA)
mal bidirectional ASP programs (bd-programs) (Eiter and
tended with function symbols that also exhibit the tree model property. In the context of DL, 2ATAs have been employed to check concept satisfiability (Calvanese, Giacomo, and
vanese, Eiter, and Ortiz 2007)–in the latter case, canonical models are forest-shaped, and as such they were encoded as trees in order to be processed using 2ATAs. In the case of
to the special form of their forest model property. Finally,
concepts
mantics
S+ = fa j a 2 Sg and S = fa j not a 2 Sg. If S is a set of (possibly negated) predicates of arity n and t1; : : : ; tn are terms, then S(t1; : : : ; tn) = fl(t1; : : : ; tn) j l 2 Sg. For a set S of atoms, not S = fnot a j a 2 Sg.
A program is a finite set of rules r : , where is a finite set of regular literals and is a finite set of literals. We denote as head(r)/body(r) the set / , where / stands for a disjunction/conjunction.
Atoms, literals, rules, and programs that do not contain variables are ground. For a rule or a program R, let vars(R), preds(R), and cts(R) be the sets of variables, predicates, and constants that occur in R, resp. A universe U for P is a non-empty countable superset of the constants in P : U cts(P ). We call PU the ground program obtained from P by substituting every variable in P by every element in U .
a ground program P .
An interpretation I of a ground program P is a subset of BP . We write I j= p(t1; : : : ; tn) if p(t1; : : : ; tn) 2 I and I j= not p(t1; : : : ; tn) if I 6j= p(t1; : : : ; tn). Also, for ground terms s; t, we write I j= s 6= t if s 6= t. For a set of ground literals L, I j= L if I j= l for every l 2 L. A ground rule r : is satisfied w.r.t. I, denoted I j= r, if I j= l for some l 2 whenever I j= . A ground constraint is satisfied w.r.t. I if I 6j= .
not , an interpretation I of P is a model of P if I satisfies every rule in P ; it is an answer set of P if it is a - minimal model of P . When P is definite (does not contain disjunction) the minimal model of P can be computed using the well-known TP operator: for a set of atoms B, let TP (B) = B [ fa j a 2 P ^ B j= g. Then, let TP0 (B) = B and T i+1(B) = TP (TPi (B)); the minimal model (answer set)
P of P , M(P ), is defined as S1
i=0 TPn(;). The derivation level of an atom a in M(P ), level(a; M(P )), is the least integer k such that a 2 T k (;). For ground programs P containing
P
not , the GL-reduct
An open interpretation of a program P is a pair (U; M )
where U is a universe for P and M is an interpretation
of PU . An open answer set of P is an open
interpretation (U; M ) of P , with M an answer set of PU . For every
atom a 2 M , where (U; M ) is an open answer set of P ,
level(a; M(PUM ) = M ) is finite
Trees and forests: we introduce notation for trees and
forests which extend those in
Given a tree T , its set of arcs is AT = f(x; y) j x; y 2 TT;j9yn =2 xN+i:;yi =2 xN +ng. We denote with succT (x) = fy 2 g the successors of a node x in T . For a node y = x i 2 T , precT (y) = x.
finite set of arbitrary constants. The set of nodes, NF , and the set of arcs, AF , of a forest F are defined as: NF = [T 2F T , and AF = [T 2F AT , resp. For a node x 2 NF , let succF (x) = succT (x), where x 2 T and T 2 F . For a node y = x i 2 T and T 2 F , precF (y) = precT (y) = x.
An interconnected forest EF is a tuple (F; ES ), where F = fTc j c 2 Cg is a forest and ES NF C. The sets of nodes NEF and arcs AEF of an interconnected forest EF are defined as: NEF = NF , and AEF = AF [ ES , resp.
connected forest/tree and f : NF ! is a labelling function, with being a set of arbitrary symbols.
Forest Logic Programs (FoLPs) are a fragment of OASP which have the forest model property. They allow only for unary and binary predicates and tree-shaped rules. The treelike structure of rules refers to the chaining pattern of rule variables: one variable can be seen as the root of a tree and the others as descendants such that for every arc in the tree, there is a positive binary literal in the body which connects the two corresponding variables. Inequalities between ‘successor’ variables can also appear in the body of such a rule; we will refer to the set of literals in the body of a rule formed only with the ‘root’ variable as the ‘local part’ and to the remaining part as the ‘successor part’. FoLPs allow also for so-called ‘free’ rules, which are rules of the form: p(~t ) _ not p(~t ) , where p is a unary/binary predicate and ~t is a unary/binary tuple of terms.
Definition 1 A forest logic program (FoLP) is an open answer set program with only unary and binary predicates, and s. t. a rule is either: a free rule: or a unary rule: a(s) _ not a(s)
; f (s; t ) _ not f (s; t ) (1) (2) (3) (4) a(s)
(s); ( i (s; ti ); i (ti ))1 6i6m ; with S16i6=j6mfti 6= tj g and m 2 N, or a binary rule: f (s; t )
(s); (s; t ); (t ); where in each rule above: – a is a unary predicate, and f is a binary predicate, – s, t, and (ti)16i6m are distinct terms, – ; ; and ( i)16i6m are sets of (possibly negated) unary predicates, – , and ( i)16i6m are sets of (possibly negated) binary predicates, – inequality does not appear in any : 6= 2= m, for 1 6 m 6 k, and 6=2= ; – there is a positive atom that connects the head term s with any successor term which is a variable: i+ 6= ;, if ti is a variable, for every 1 6 i 6 m, and + 6= ;, if t is a variable.
A predicate q is free if it occurs in a free rule in P . Example 1 The following program P is a FoLP: it describes the fact that somebody who has read two different novels is a literature lover (unary rule r1), a novel is something written by a novelist (unary rule r2), and a novelist is somebody who wrote at least one novel (unary rule r3). There are three free rules describing binary predicates read, writtenBy, and wrote as being free. Finally, there are two facts (unary rules with empty bodies): f1 and f2. r1 : LitLover (X ) read (X ; Y1 ); read (X ; Y2 );
Novel (Y1 ); Novel (Y2 ); Y1 6= Y2 r2 : Novel (X ) wrBy (X ; Y ); Novelist (Y ) r3 : Novelist (X ) wrote(X ; Y ); Novel (Y ) r4 : read (X ; Y ) _ not read (X ; Y ) r5 : wrBy (X ; Y ) _ not wrBy (X ; Y ) r6 : wrote(X ; Y ) _ not wrote(X ; Y ) f1 : Novel (a) f2 : Novelist (b)
and brul (P ), the sets of unary and binary predicates and unary and binary rules which occur in P , resp.
For a unary rule r of type (3), the degree of r, denoted as deg(r), is the number k of successor variables which appear in the rule. Intuitively, it indicates the maximum number of successor individuals needed to make the body of the rule true. The degree of a free rule is 0. For a unary predicate p: deg(p) = maxfdeg(r) j p 2 preds(head(r))g: Finally, the degree of a FoLP P is deg(P ) = Pp2upr(P ) deg(p):
needed to satisfy all atoms of the form p(x), where p 2 upr (P ), for a given individual x.
Example 2 Let P be the FoLP from Example 1. Then, deg(LitLover) = 2, deg(N ovel) = 1, deg(N ovelist) = 1, and thus, deg(P ) = 4.
Forest models: The forest model property of an OASP P is as follows: if a unary predicate p is satisfiable, then there exists a model which satisfies p that can be seen as an interconnected forest. The forest contains for each constant in P a tree having the constant as root, and possibly an additional tree with an anonymous root. The predicate checked to be satisfiable, p, belongs to the label of one of the root nodes. Definition 2 Let P be a program. A predicate p 2 upr (P ) is forest satisfiable w.r.t. P if there exist an open answer set (U; M ) of P ; an interconnected forest EF = (fT g [ fTa j a 2 cts(P )g; ES ), where is a constant, possibly from cts(P ); and a labelling function ef : fT g [ fTa j a 2 cts(P )g [ AEF ! 2preds(P ) such that: p 2 ef ( ), U = NEF , ef (x) 2 2upr(P ), when x 2 T [ fTa j a 2 cts(P )g, ef (x) 2 2bpr(P ), when x 2 AT , M = fp(x) j p 2 ef (x); x 2 NEF g [ ff (x; y) j f 2 ef (x; y); (x; y) 2 AEF g, and for every (z; z i) 2 AEF : ef (z; z i) 6= ;.
We call such a pair (U; M ) a forest model. A program P
has the forest model property, if every unary predicate p that
is satisfiable w.r.t. P , is forest satisfiable w.r.t. P .
Proposition 1 FoLPs have the forest model property.
Example 3 Consider again the FoLP P from Example 1.
Figure 1 a) depicts a forest model which satisfies the unary
predicate LitLover. Intuitively, the predicate is satisfied
at the anonymous root as there are two distinct
readsuccessors of where N ovel holds: a and 1, and thus
LitLover( ) is ‘supported’ by a ground version of rule r1.
In turn, N ovel holds at 1 as it is supported by rule r2
grounded such that X is replaced with 1 and Y is replaced
with b. Note that every atom in the model is finitely
supported: there is no infinite chain of dependencies of atoms
in the model. This is a property of (open) answer sets also
known as ‘well-supportedness’
Consider in contrast the tentative model depicted in Figure 1 b). There, N ovel( 1) is motivated by a wrBysuccessor where N ovelist holds, which in turn is motivated by a wrote-successor where N ovel holds, etc. The interpretation is not a model, as N ovel( 1) is not finitely motivated. One of the main challenges when designing algorithms to reason with FoLPs is ensuring that every atom in a model is well-supported.
As explained in the Introduction, FoLPs can be used to
simulate reasoning with SHOQ ontologies. Thus, they can
be viewed as an integrative formalism for reasoning with
both ontologies and rules:
nomial, and modular translation from SHOQ to FoLPs is
provided in
et al. 2008) as a tool to reason in hybrid graded -calculus.
For a set Y , we denote with B+(Y ) the set of positive Boolean formulas over Y , where true and f alse are also allowed and where ^ has precedence over _. For a set X Y and a formula 2 B+(Y ), we say that
signing false to elements in Y X makes true. For b > 0, let Db = fh0i; h1i; : : : ; hbig [ f[0]; [1]; : : : ; [b]g [ f 1; "; hrooti; [root]g.
A fully enriched automaton (FEA) is a tuple A = h ; b; Q; ; q0; F i, where is a finite input alphabet, b > 0 is a counting bound, Q is a finite set of states, : Q ! B+(Db Q) is a transition function, q0 2 Q is an initial state, and F = fF1; F2; : : : ; Fkg, where F1 F2 : : : Fk = Q is a parity acceptance condition. The number k of sets in F is the index of the automaton.
A run of a FEA on a labeled forest (F; V ) is an NF Qlabeled tree (Tc; r) such that: r(c) = (d; q0), for some root d in F , and for all y 2 Tc with r(y) = (x; q) and (q; V (x)) = , there is a (possibly empty) set S Db Q such that S satisfies and for all (d; s) 2 S, the following hold: – if d 2 f 1; "g, then x d is defined and there is j 2 N+ such that y j 2 Tc and r(y j) = (x d; s); – if d = hni, then there is a set M succF (x) of cardinality n + 1 such that for all z 2 M , there is j 2 N+ such that y j 2 Tc and r(y j) = (z; s); – if d = [n], then there is a set M succF (x) of cardinality n such that for all z 2 succF (x) M , there is j 2 N+ such that y j 2 Tc and r(y j) = (z; s); – if d = hrooti (d = [root]), then for some (all) root(s) c 2 F there exists j 2 N+ such that y j 2 Tc and r(y j) = (c; s);
Moreover, since no set S satisfies = f alse, there cannot be any run that takes a transition with = f alse. A run is accepting if each of its infinite paths is accepting, that is if the minimum i for which Inf ( )\Fi 6= ;, where Inf ( ) is the set of states occurring infinitely often in , is even. The automaton accepts a forest iff there exists an accepting run of the automaton on the forest. The language of A, denoted
Theorem 1 (Corollary 4.3
predicates with respect to FoLPs as emptiness checking for
We start by introducing for every FoLP P and unary predicate p a class of FEAs Ap;;P , where is one of cts(P ) or a new anonymous individual and : cts(P ) [ f g ! 2upr(P )[cts(P )[f g is a function which has the following properties: oi 2 (oi), and oj 2= (oi), for every oi; oj 2 cts(P ) [ f g, such that oi 6= oj . Furthermore, p 2 (c), where c is one of cts(P ) [ f g and c is if 2= cts(P ). Intuitively Ap;;P will accept forest models of p with respect to P encoded in a certain fashion: in particular, for every root in the forest model, the root node will appear in its own label; function fixes a content for the label of each root of accepted forest models.
In the following, let d = deg(P ). We will also denote with PATP the set f g [ cts(P ) of term patterns, where stands for a generic anonymous individual: we say that a term t matches a term pattern pt, and write t 7! pt iff t = pt, when t is a constant. In all other cases, the match trivially holds. Term patterns will be used in our encoding as a unification mechanism between terms occurring in a FoLP (variables and constants) and elements in a universe (anonymous individuals and constants): a variable will match with a constant or an anonymous individual, but a constant will match only with itself. The automata Ap;;P will run on forests labelled using the following alphabet: = 2S , where o S = upr (P ) [ f1; : : : ; dg [ cts(P ) [ f g [ f"f j f 2 t bpr (P )g [ f#f j f 2 bpr (P ); t 2 PATP g.
Unlike the case for forest models, the arcs of forests accepted by FEAs are not labelled: as such, binary predicates occur in the label of nodes in an adorned form. These adorned predicates are either of the form #tf , in which case they represent an f -link between the predecessor of the labelled node, which has term pattern t and the node itself, or of the form "fo , in which case the current node is linked to a constant o from P via the binary predicate f . Additionally, besides unary predicates, labels might contain natural numbers and constants, which will be used as an addressing mechanism for successors of a given node and nodes which stand for constants in accepted forests, resp. The set of states of the automaton are as follows: Q = Qi [ Q+ [ Q , with: Qi = fq0; q1; qo; q:kg, Q+ = fqt;a; qt;ra ; qt1;t2;u; qt1;t2;rf ; qk;t; ;ug, and Q
= fqt;a; qt;ra ; qt1;t2;u; qt1;t2;rf ; qk;t; ;ug, where o 2 cts(P ) [ f g, a 2 upr (P ), f 2 bpr (P ), u is of the form a, f , not a or not f , k 2 f1; : : : ; dg, ra 2 urul (P ), rf 2 brul (P ), and t; t1; t2 2 PATP . We will refer to Q+ and Q as the positive and the negative states of Ap;;P , resp. Intuitively, positive states are used to motivate the presence of atoms in an open answer set while negative states are used to motivate the absence of atoms in an open answer set. Qi contains some additional states, like q0, the initial state, q1, a state which will be visited recursively in every node of the forest, qo, a state corresponding to the initial visit of constant nodes, and q:k, a state which asserts that for every node in an accepted forest there must be at most one successor which has k in the label.
We describe in detail the transition function of Ap;;P . The initial transition prescribes that the automaton visits a root of the forest in state qo, for every o 2 cts(P ) [ f g: (q0; ) = ^ o2cts(P )[f g
In every such state qo, it should hold that o and only o is part of the label. Furthermore, the automaton justifies the presence and absence of each unary predicate a and each adorned upward binary predicate in the label1 by entering states qo;a, qo;o0;f , qo;a, and qo;o0;f resp. At the same time every successor of the constant node is visited in state q1. Let coP = cts(P ) [ f g fog. Then: (qo; ) = o 2 ^
^ o0 2= o02coP ^
^ ("; qo;a) ^ a2 (o)
^ a2= (o) ("; qo;a) ^ ^ ("; qo;o0;f ) ^ ^ ("; qo;o0;f ) ^ ([0]; q1) (6) "fo0 2 (o)
"fo0 2= (o)
Whenever the automaton finds itself in state q1 it tries to motivate the presence and absence of each unary and adorned binary predicate in its label and then it recursively enters the same state into each successor of the current node. It also ensures that for each integer 1 6 k 6 d, the labels of each but one successor do not contain k: (q1; )=([0]; q1)^ ^ ([1]; q:k)^^("; q ;a) ^^ ("; q ;a)^ 16k6d a2 a2= ^("; qt; ;f ) ^ ^("; qt; ;f ) ^^("; q ;o0;f ) ^ ^ ("; q ;o0;f ) (7) t #f 2 #tf 2= "fo0 2
"fo0 2= (q:k; ) = k 2= (8)
To motivate the presence of a unary/binary predicate in the label of a node, the automaton checks whether the given predicate is free (we assume that f ree(a) evaluates to true if a is free, and, to false, otherwise) or finds a unary/binary rule which supports the predicate. Note the distinction concerning the term pattern for the node where the predicate has to hold. In the case of unary predicates, if the node is a constant, there is first a preliminary check that we are at the right node - this is needed as later the automaton will visit all roots in this state. In the case of binary predicates, depending on the term pattern, the label is checked for different types of adorned binary atoms. In all cases, only rules whose head terms match the given term patterns are chosen to motivate the presence of predicates in the label.
(q ;a; ) = a 2 ^ f ree(a) _ 1As constants have no predecessors in the forest, there will be no adorned downward predicates in the label. for every ji 2 Jra , vi 2 cts(P ) implies ji = vi, and for every ji; jl 2 Jra , vi 6= vl 2 implies ji 6= jl. Intuitively, a multiset provides a way to satisfy the successor part of a unary rule in a forest model by identifying the successor terms of the rule with either successors of the current element in the model or constants in the program. We next describe the transition function for unary rules: (qt;ra ; ) = ^ ("; q ;t;u) ^ 9Jra : u2 qk;t; ;u) ^ ^ ^ d ^ ^ k=1ji=ku2 i[ i ^ ("; qt;o;u) ^ (h0i; (13) o2cts(P ) ji=o u2 i[ i
State qk;t; ;u enforces that the (possibly negated) unary or adorned binary predicate u is (is not) part of the label of the k-th successor of a given node; we thus define: (qk;t1;t2;u; ) = k 2 ^ ("; qt1;t2;u) (14) ^ ^ j 2=
j6=k
The state qt1;t2;u can be seen as a multi-state with different transitions depending on its arguments (two transitions have already been introduced as rules (11) and (12) above): if t2 = , one has the justify the presence/absence of u in the label of the current node; otherwise, when t2 = o, one has to justify it from the label of the root node corresponding to constant o: note that, as it is not possible to jump directly to a given root node in the forest, nor to enforce that there will be a single root node corresponding to each constant, in transition (17) we visit each root node in state qo;a: (qt1;t2;u; ) = 8 ("; q ;a); if t2 = and u = a (15) > >>>> ([root]; qo;a); if t2 = o and u = a (16) ><>> a 2= ; if t2 = and u = not a (17)
a 2= (o); if t2 = o and u = not a (18) > > >>>> #tf 2= ; if t2 = and u = not f (19) > > : "fo 2= (o); if t2 = o and u = not f (20)
For binary rules: rf : f (s; v) (s); (s; v); (v), when v is grounded using an anonymous individual, the check involves looking to the predecessor node to see if the local part of the rule is satisfied. When v is grounded using a constant, the local part of the rule is checked at the current node and the successor part at the respective constant. Note that the first term pattern in the first conjunct in both rules (21) and (22) is irrelevant as contains only unary predicates: (qt; ;rf ; ) = ^ ( 1; q ;t;u) ^ ^ f ree(f )_ (qt; ;rf ; ) = _ ( 1; q ;t;u) _ u2
_ ("; qt; ;u) u2 [ (qt;o;rf ; ) = _ ("; q ;t;u) _ _ ("; qt;o;u) (36) u2 u2 [
Finally we specify the parity acceptance condition. The index of the automaton is 2, with F1 = fqt;a; qt1;t2;f j a 2 upr (P ); f 2 bpr (P ); t; t1; t2 2 PATP g and F2 = Q. Intuitively, paths in a run of the automaton correspond to dependencies of literals in the accepted model and by disallowing the infinite occurrence on a path of states associated to atoms in the model we ensure that only well-supported models are accepted.
Theorem 2 Let P be a FoLP and let p be a unary predicate symbol. Then, p is satisfiable w.r.t. P iff there exists an automaton Ap;;P such that L(Ap;;P ) 6= ;.
^ ("; q ;t;u) ^ u2
In the following, we describe the transitions of the automaton in the negative states, i.e. the states which are used to motivate the absence of certain unary/binary predicates in the labels of the forest. If one ignores the checks for the absence of unary/adorned binary predicates in the label of the current node, the transition rules can be seen as dual versions of the ones for the counterpart positive states.
(q ;a; ) = a 2= ^ Proof Sketch. ()): Assume p is satisfiable w.r.t. P . Then, by Prop. 1, p is satisfied by a forest model (U; M ). Let (EF; ef ), with EF = (F; ES) be the labelled forest which induces (U; M ), as in Definition 2. Then, let l : fTc j c 2 cts(P ) [ f gg be a labelling function such that for every y 2 fTc j c 2 cts(P ) [ f gg, l(y) is the least set cono taining: (i) ef (y), (ii) f"f j f 2 ef (y; o); o 2 cts(P )g, (iii) f#fy j f 2 ef (z; y); z = precF (y); z 2= cts(P )g, (iv) f#zf j f 2 ef (z; y); z = precF (y); z 2 cts(P )g, (v) fyg, when y 2 cts(P ) [ , and (vi) fig if y = z i.
We define an automaton Ap;;P which accepts (F; l). Let be the same as its homonym in the considered forest model and let be such that (o) = l(o), for every o 2 cts(P ) [ f g. We construct a run (Tc; r) of Ap;;P on (F; l) by first setting r(c) = ( ; q0), where is the root of some forest in F . Then, for each o 2 cts(P ) [ f g, we introduce a successor of c, c i, such that r(c i) = (o; qo).
maintaining the following invariant, for each w 2 Tr: r(w) = (y; q ;a) implies a 2 l(y); r(w) = (y; qo;a) implies o 2= l(y) or a 2 (o); r(w) = (y; qt;ra ) implies a 2 l(y), a is not free, and there is a rule s 2 P M derived from ra such that head(s) =
U a(y), M j= body(s), and maxb2body(s)(level(b; M )) < level(a(y); M ); r(w) = (y; qt; ;u) implies a 2 l(y), if u = a; a 2= l(y), if u = not a; #tf 2 l(y), if u = f ; #tf 2= l(y), if u = not f ; r(w) = (y; qt;o;u) implies a 2 l(o), if u = a; a 2= l(o), if u = not a; "fo 2 l(y), if u = f ; "tf 2= l(y), if u = not f ; r(w) = (y; qk;t; ;u) implies k 2 l(y), and j 2= l(y), for every 1 6 j 6= k 6 d; a 2 l(y), if u = a; a 2= l(y), if u = not a; #tf 2 l(y), if u = f ; #tf 2= l(y), if u = not f ; r(w) = (y; qt; ;rf ) implies #tf 2 l(y), f is not free, and there is a rule s 2 PUM derived from r such that head(s) = f (precF (y); y), M j= body(s), and maxb2body(s) level(b; M ) < level(f (precF (y); y); M ); o r(w) = (y; qt;o;rf ) implies "f 2 l(y), f is not free, and there is a rule s 2 P M derived from r such that
U head(s) = f (y; o), M j= body(s), and maxb2body(s) level(b; M ) < level(f (y; o); M ); r(w) = (y; qt;a) implies a 2= l(y); r(w) = (y; qt;ra ) implies a 2= l(y); r(w) = (y; qt; ;u) implies a 2= l(y), if u = a; a 2 l(y), if u = not a; #tf 2= l(y), if u = f ; #tf 2 l(y), if u = not f ; r(w) = (y; qt;o;f ) implies a 2= l(o), if u = a; a 2 l(o), if u = not a; "fo 2= l(y), if u = f ; "tf 2 l(y), if u = not f ; r(w) = (y; qk;t; ;u) implies k 2= l(y) or a 2= l(y), if u = a; a 2 l(y), if u = not a; #tf 2= l(y), if u = f ; t #f 2 l(y), if u = not f ; r(w) = (y; qt; ;f ) implies #tf 2= l(y); r(w) = (y; qt;o;rf ) implies "fo 2= l(y).
Assume r(w) = (y; qt;a), for some w 2 Tr. Then, from the IH: a 2 l(y), and a(y) 2 M . Then, there must be a finite n such that level(a(y); M ) = n and some rule s in PUM such that maxb2body(s)(level(b; M )) = n 1 (from which a(y) has been derived at iteration n). Let ra be the rule in P from which s has been derived and let w i be a successor of w in Tr such that r(w i) = (y; qt;ra ). The invariant is preserved.
Assume r(w) = (y; qt;ra ), for some w 2 Tr. Then, from the IH: a 2 l(y), a is not free, and there exists some rule s in PUM derived from ra: a(y) +(y) [ S16i6m( i+(y; zi) [ i+(zi)) such that M j= body(s) and maxb2body(s)(level(b; M )) < level(a(y); M ). Note that M j= (y) [ Sim=1( i(y; zi) [ i(zi)). As (U; M ) is a forest model, each zm must be of the form y k, for some 1 6 k 6 d, or of the form o 2 cts(P ). Let Jra be a multiset such that ji = zi, if zi 2 cts(P ) and ji = k if zi = y k. Then, we introduce the following successors of w in Tc (denoted just by their label): – (y; q ;t;u), for every u 2 (y).
: the invariant holds as M j= – (y k; qk;t; ;u), for every 1 6 k 6 d, i such that ji = k, and u 2 i [ i: the invariant holds as M j= i(y; y k) [ i(y k). It is also the case that k 2 l(y k) and j 2= l(y k), for every 1 6 j 6= k leqd. – (y; qt;o;u), for every o and i such that ji = o and u 2 i [ i: the invariant holds as M j= i(y; o) [ i(o).
The invariant ensures the existence of a run. We next show that every run Tc constructed as above is accepting, i.e. on every path of Tc there are finitely many occurrences of states of the form qt;a or qt1;t2;f . Assume that every element w 2 Tc for which r(w) = (y; qt;a), r(w) = (y; qt; ;f ), or r(w) = (y; qt;o;f ) is annotated with level(a(y); M ), level(f (prec(y); y); M ), or level(f (y; o); M ), resp. From the invariant of the construction it follows that level annotations decrease along each path of Tc. But the level of every atom in an open answer set is finite. Thus, the number of level annotations, and consequently the number of occurrences of such states must be finite.
((): Assume that there exists an automaton Ap;;P such that L(Ap;;P ) 6= ;. Then, there exists a labelled forest (F 0; f 0) and an accepting run (Tc; r) on (F 0; f 0) such that r(c) = ( ; q0), for some root in F 0. Let F be the forest containing the nodes y 2 NF 0 for which either (i) there exists some w 2 Tc such that r(w) = (y; qo) or (ii) precF 0 (y) 2 NF and there exists some w 2 Tc such that r(w) = (y; qk;t1;t2;u). Assume C is the set of roots in F . Then let : NF ! NF [ cts(P ) [ f g be as follows: (y) = oi; if oi 2 l(y); and (c) s; if y = c s; for c 2 C let l be the following labeling function for NF : l(y) = : ( (y)); if (y) 2 cts(P ) f 0(y);
if (y) 2 NF cts(P )
Also, let: U = f (y) j y 2 NF g, M = fa( (y)) j a 2 l(y)\upr (P )^y 2 NF g[ff ( (z); (z) i) j#f 2 l(y)^y = oi z i ^ y 2 NF g [ ff ( (y); oi) j"f 2 l(y) ^ y 2 NF g.
that: (i) M is a model of PUM , i.e every rule in PUM is satisfied by
Let r0 : a( (y)) +( (y)); ( i+( (y); (yi)); i+( (yi)))16i6m be a rule in P M derived from a unary rule
U r : a(s) (s); ( i(s; ti); i(ti))16i6m; in P . Let Jr be the multiset formed of elements ji, 1 6 i 6 m, such that: ji =
(yi); if (yi) 2 cts(P ); k; if (yi) = (x) k: Assume M j= body(r0), but M 6j= a( (y)). Then, a 2= l(y) and there must be some w 2 Tc such that either: – r(w) = (y; qx;a). Then, for every rule ra : a(s) 2 P , there must be a node wra 2 Tc such that r(wra ) = (y; qx;ra ). This holds also for rule r. Then, one of the following holds: there exists w0 2 Tc such that r(w0) = (y; qx;x;u), for some u 2 : then, either u = a and (y; q ;a) 2 Tc and thus a 2= l(y) or M 6j= a( (y)) – contradiction, or for some u = not a, a 2 l(y) or M j= a( (y)) – contradiction. for every multiset Jra as in transition rule (14) (including Jr above) and every ji 2 Jra either: there exist 1 6 k 6 d, 1 6 i 6 m, and u 2 i [ i such that ji = k and for every y g 2 F , there is a node wg 2 Tc such that r(wg) = (y g; qk;t;x;u): then, there is wk 2 Tc such that r(wk) = (y k; qk;t;x;u) and either (1) k 2= l(y k) – contradiction, (2) u = a, a 2= l(y k): a( (y k)) 2= M or M 6j= a( (yi)), and thus M 6j= i( (yi)) – contradiction, (3) u = not a, a 2 l(y k): a( (y k)) 2 M or M j= a( (yi)), and thus M 6j= i( (yi)) – contradiction, (4) u = f , #tf 2= l(y k): f ( (y); (y k)) 2= M or M 6j= f ( (y); (yi)), and thus M 6j= i( (y); (yi)) – contradiction, (5) for some u = not f , #tf 2 l(y k): f ( (y); (y k)) 2 M or M j= f ( (y); (yi)), and thus M 6j= i( (y); (yi)) – contradiction. there exists 1 6 i 6 m such that ji = o, for some o 2 cts(P ), a node wo 2 Tc, and u 2 i [ i such that r(wo) = (y; qt;o;u): similar to above we reach a contradiction with the fact that M j= i( (y); o) [ i(o). – r(w) = (y; qo;a) with (y) = o. Then, o 2= l(y) = (o) – contradiction or a 2= (o) and for every rule ra : a(s) 2 P , such that s 7! o there must be a node wra 2 Tc such that r(wra ) = (y; qo;ra ) – similar to above.
Thus, in each case we obtained a contradiction and M j= a( (y)): every unary rule is satisfied by M . Similarly it can be shown that every binary rule is satisfied as well. (i) M is minimal: from the fact that (Tc; r) is accepting, it follows that every path starting at a state in Q+ must be finite. For every node w 2 Tc, such that r(w) = (y; q), for some q 2 Q+, let: d(w) = 0; if w has no successors in Tc;
r(w) = (y; qx;a) implies a( (y)) 2 M(PUM ), r(w) = (y; qo;a) implies o 2= l(y) or a(o) 2 M(PUM ), r(w) = (y; qt;ra ) implies PUM contains a rule a( (y)) such that M(PUM ) j= , r(w) = (y; qt;x;rf ) implies y = z i, for some i, and P M U contains f ( (z); (z) i) such that M(PUM ) j= , r(w) = (y; qt;o;rf ) implies PUM contains f ( (y); o) such that M(PUM ) j= , r(w) = (y; qk;t;x;u) implies y = z i, k 2 l(y), for every j 6= k: j 2= l(y), and: a( (y)) 2 M(PUM ), if u = a; a( (y)) 2= M(PUM ), if u = not a; f ( (z); (z) i) 2 M(PUM ), if u = f ; f ( (z); (z) i) 2= M(PUM ), if u = not f ; r(w) = (y; qt;x;u) implies y = z i, and: a( (y)) 2 M(PUM ), if u = a; a( (y)) 2= M(PUM ), if u = not a; f ( (z); (z) i) 2 M(PUM ), if u = f ; f ( (z); (z) i) 2= M(PUM ), if u = not f ; r(w) = (y; qt;o;u) implies: a(o) 2 M(PUM ), if u = a; a(o) 2= M(PUM ), if u = not a; f ( (y); o) 2 M(PUM ), if u = f ; f ( (y); o) 2= M(PUM ), if u = not f .
Induction base: assume w is a leaf in Tc and r(w) = (y; q), for some q 2 Q+ (d(w) = 0). Then, one of the following holds: r(w) = (y; qt;a) and a is free: in this case a( (y)) 2 M and thus PUM will contain rule a( (y)) . Thus, a( (y)) 2 M(PUM ). r(w) = (y; qt1;t2;f ) and f is free: similar to above. r(w) = (y; qt1;t2;u) and u = not a or u = not f : from the fact that (Tr; t) is a run and transition rules (17-20), it follows that a 2= l(y) or #tf2 (t2 = )= "fo (t2 = o) 2= l(y). Then, the claim follows from the definition of M .
Induction step: consider a non-leaf node w 2 Tc (d(w) > 0). We will analyse the case when r(w) = (y; qt;ra ): then, for every u 2 there is a successor w i ;u of w such that r(w i ;u) = (y; qx;t;u) and there exists a multiset Jra and successors w mk;i;u and w mo;i;u for w such that: r(w mk;i;u) = (y zk;i;u; qk;t;x;u), for all pairs (k; i) such that ji = k and u 2 i [ i; r(w mo;i;u) = (y; qt;o;u), for all pairs (o; i) such that ji = o and u 2 i [ i.
M(PUM ) j= u( (y)), for every u 2 M(PUM ) j= ( (y)) (*1), , and thus M(PUM ) j= u( (y); (y) zk;i;u), for every u 2 i and M(PUM ) j= u( (y) zk;i;u), for every u 2 i and k 2 l( (y) zk;i;u): as there is a unique successor y zk of y such that k 2 l(y zk), it follows that: M(PUM ) j= u( (y); (y) zk), for every u 2 i and M(PUM ) j= u( (y) zk), for every u 2 i and thus M(PUM ) j= i( (y); (y) zk) [ i( (y) zk) (*2), M(PUM ) j= u( (y); o), for every u 2 i and M(PUM ) j= u(o)), for every u 2 i, where ji = o, and thus M(PUM ) j= i( (y); o) [ i(o) (*3).
From (*1)-(*3) and the fact that ji 6= jl implies zji 6= zjl , it follows that M(PUM ) j= ( (y)) [ S16k6d( i( (y); (y) zk) [ i( (y) zk))ji=k [ So2cts(P )( i( (y); o)[ i(o))ji=o; , which is the body of a grounding of ra in PU with head a( (y)). Then, by applying the reduct one obtains that +( (y)) [ S16k6d( i+( (y); (y) M(PUM ) j= zk) [ i+( (y) zk))ji=k [ So2cts(P )( i+( (y); o) [ i+(o))ji=o, which is the body of a rule with head a( (y)) in PUM .
Then, as a 2 l(y) \ upr (P ) implies that there exists a node w 2 Tr such that r(w) = (y; qt;a), #tf 2 l(y) implies that there exists a node w 2 Tr such that r(w) = (y; qt;x;f ), o and "f 2 l(y) implies that there exists a node w 2 Tr such that r(w) = (y; qt;o;f ) (from transition rule (7)), it follows that M M(PUM ), and thus M is a minimal model of PUM . 2 Theorem 3 Satisfiability checking of unary predicates w.r.t. FoLPs is EXPTIME-complete.
the fact that satisfiability checking of unary concepts w.r.t.
latter has been reduced to satisfiability checking of unary
predicates w.r.t. FoLPs in
For the upper bound, we observe that for a given P and p, there is an exponential number of automata Ap;;P (as there are an exponential number of possible ). Each such automaton can be constructed in exponential time, and emptiness checking for Ap;;P can be performed again in exponential time. The latter follows from Theorem 1 and the fact that the branching factor and the number of states of Ap;;P are polynomial in the size of P , while its index is constant (viz.
on this reasoning task for FoLPs. Other reasoning tasks like
consistency checking of FoLPs and skeptical and brave
entailment of ground atoms can be polynomially reduced to
satisfiability checking of unary predicates
sult applies to fKBs as well: satisfiability checking of unary predicates w.r.t. fKBs is EXPTIME-complete. Thus, reasoning with FoLP rules and SHOQ ontologies is not harder than reasoning with SHOQ ontologies themselves.
In the introduction, we mentioned the special form of forest model property as one of the reasons FoLPs cannot be straightforwardly dealt with using 2ATAs. An additional technical difficulty we had to overcome compared to both encodings using 2ATAs and other encodings using FEAs, is the fact that FEAs, unlike 2ATAs, cannot explicitly address successor nodes in runs: they are suitable for encoding graded modalities/number restrictions where the same property has to hold/not to hold at a given number of successors.
hold at different successors (as the structure of FoLP rules allows), we had to devise an addressing mechanism for successors. Furthermore, as terms occurring in any position in
complexity as CoLPs, we plan to further investigate the extension of the deterministic AND/OR tableau algorithm for