Reasoning with Forest Logic Programs Using Fully Enriched Automata Cristina Feier Thomas Eiter Department of Computer Science Institute of Information Systems University of Oxford Vienna University of Technology cristina.feier@cs.ox.ac.uk eiter@kr.tuwien.ac.at Abstract In general, OASP is undecidable. To achieve decidability, several fragments have been defined by imposing syntacti- Forest Logic Programs (FoLP) are a decidable frag- cal restrictions on the shape of rules. Such a fragment are ment of Open Answer Set Programming (OASP) which Forest Logic Programs (FoLP) which enjoy the forest model have the forest model property. OASP extends Answer property: a unary predicate is satisfiable iff it is satisfied by Set Programming (ASP) with open domains—a feature which makes it possible for FoLPs to simulate reason- a model that can be represented as a labeled forest, where ing with the expressive description logic SHOQ. At nodes and arcs are labeled with sets of unary predicates and the same time, the fragment retains the attractive rule binary predicates, respectively. syntax and the non-monotonicity specific to ASP. In FoLPs are quite an expressive fragment as they allow, for the past, several tableaux algorithms have been devised instance, the simulation of standard reasoning tasks (like to reason with FoLPs, the most recent of which estab- concept satisfiability and KB consistency) with SHOQ on- lished a NE XP T IME upper bound for reasoning with the tologies (Feier and Heymans 2013). This property of FoLPs fragment. While known to be E XP T IME-hard, the ex- led to f-hybrid KBs, a combination of rules and ontologies act complexity characterization of reasoning with the fragment was still unknown. In this paper we settle this which distinguish themselves among other approaches like open question by a reduction of reasoning with FoLPs to dl-safe rules, r-hybrid knowledge bases, or MKNF+ knowl- emptiness checking of fully enriched automata, a form edge bases, by the fact that they impose no restrictions on the of automata which run on forests, and which are known interaction between the signatures of the two components. to be E XP T IME-complete. Such restrictions prevent the need for reasoning with un- known individuals in the rule component. As f-hybrid KBs are based on the simulation of SHOQ KBs within FoLPs, Introduction no such restriction is needed. Conceptual modeling using FoLPs is not restricted to simulating reasoning with SHOQ Open Answer Set Programming (OASP) (Heymans, KBs: it is also possible to translate object-role modeling Van Nieuwenborgh, and Vermeir 2008) extends Answer Set (ORM) models as sets of FoLP rules, e.g. (Heymans 2006). Programming (ASP) (Gelfond and Lifschitz 1988) with an open domain semantics: programs are interpreted w.r.t. ar- As they can simulate reasoning within the Description bitrary domains that might contain individuals which do Logic (DL) SHOQ, it follows that reasoning with FoLPs not occur explicitly in the program. This makes it possi- is E XP T IME-hard. However, the exact complexity charac- ble to state generic knowledge using OASP. At the same terization of FoLPs was still open. Previously, reasoning time, OASP inherits from ASP the negation under the sta- with FoLPs was addressed by means of tableau-based algo- ble model semantics. Thus, OASP bridges two important rithms: (Feier and Heymans 2013) described a 2NE XP T IME knowledge representation paradigms: the classical First Or- tableau algorithm, while an improved algorithm which runs der Logic (FOL) open world and the non-monotonic rules in the worst case in NE XP T IME has been described in (Feier closed world. It is part of a broad line of research which 2012). While in the latter work it has been speculated that includes approaches like DL-safe rules (Motik, Sattler, and the non-deterministic tableau algorithm can be determinized Studer 2005), DL+log (Rosati 2006), dl-programs (Eiter in order to lead to an E XP T IME procedure which would be et al. 2008), Description Logic Rules (Krötzsch, Rudolph, worst-case optimal, the determinization in the case of FoLPs and Hitzler 2008), r-hybrid knowledge bases (Rosati 2008), proved elusive. Such a deterministic worst-case optimal al- Datalog± (Calı̀, Gottlob, and Lukasiewicz 2009), MKNF+ gorithm has been devised for CoLPs, which restrict FoLPs to knowledge bases (Motik and Rosati 2010), and Nonmono- programs without constants, and simple FoLPs, a fragment tonic Existential Rules (Magka, Krötzsch, and Horrocks in which recursion is restricted: the technique does not scale 2013). up to FoLPs (see (Feier 2014)). In this paper, we settle the open question regarding the Copyright c 2015 for this paper by its authors. Copying permitted exact complexity characterization of FoLPs: by using a re- for private and academic purposes. duction to emptiness checking of Fully Enriched Automata (FEAs), we show that satisfiability checking of unary predi- a non-empty countable superset of the constants in P : U ⊇ cates w.r.t. FoLPs is E XP T IME-complete. Hence, reasoning cts(P ). We call PU the ground program obtained from P with FoLP rules and SHOQ ontologies is not harder than by substituting every variable in P by every element in U . reasoning with SHOQ ontologies themselves. Let BP be the set of regular atoms that can be formed from Fully enriched automata have been introduced in (Bon- a ground program P . atti et al. 2008) as a tool to reason with hybrid graded µ- An interpretation I of a ground program P is a subset calculus, which extends µ-calculus with graded modalities of BP . We write I |= p(t1 , . . . , tn ) if p(t1 , . . . , tn ) ∈ I and nominals. They offer an elegant device for our encod- and I |= not p(t1 , . . . , tn ) if I 6|= p(t1 , . . . , tn ). Also, for ing as they accept forests as inputs and also feature a parity ground terms s, t, we write I |= s 6= t if s 6= t. For a set of acceptance condition that is useful in distinguishing well- ground literals L, I |= L if I |= l for every l ∈ L. A ground supported models (Fages 1991), a fundamental characteris- rule r : α ← β is satisfied w.r.t. I, denoted I |= r, if I |= l tic of (open) answer sets. However, FoLPs exhibit a specific for some l ∈ α whenever I |= β. A ground constraint ← β form of the forest model property, in which every node can is satisfied w.r.t. I if I 6|= β. point back to any root of the forest, and as such the encoding For a positive ground program P , i.e., a program without is not without its challenges. not, an interpretation I of P is a model of P if I satisfies The automata-based method has been previously applied every rule in P ; it is an answer set of P if it is a ⊆- minimal to reason with CoLPs (Heymans, Van Nieuwenborgh, and model of P . When P is definite (does not contain disjunc- Vermeir 2006): satisfiability checking of unary predicates tion) the minimal model of P can be computed using the w.r.t. a CoLP has been reduced to non-emptiness checking well-known TP operator: for a set of atoms B, let TP (B) = of two-way alternating tree automata (2ATA) (Vardi 1998). B ∪ {a | a ← β ∈ P ∧ B |= β}. Then, let TP0 (B) = B and 2ATAs have also been used to check consistency of nor- TPi+1 (B) = TP (TPi (B)); S the minimal model (answer set) ∞ mal bidirectional ASP programs (bd-programs) (Eiter and of P , M(P ), is defined as i=0 TPn (∅). The derivation level Šimkus 2009), which are a decidable fragment of ASP ex- of an atom a in M(P ), level(a, M(P )), is the least integer tended with function symbols that also exhibit the tree model k such that a ∈ TPk (∅). For ground programs P containing property. In the context of DL, 2ATAs have been employed not, the GL-reduct (Gelfond and Lifschitz 1988) w.r.t. I is to check concept satisfiability (Calvanese, Giacomo, and defined as P I , where P I contains α+ ← β + for α ← β in Lenzerini 2002) and satisfiability of ALCQIbreg KBs (Cal- P , I |= not β − and I |= α− . I is an answer set of a ground vanese, Eiter, and Ortiz 2007)–in the latter case, canonical P if I is an answer set of P I . models are forest-shaped, and as such they were encoded as An open interpretation of a program P is a pair (U, M ) trees in order to be processed using 2ATAs. In the case of where U is a universe for P and M is an interpretation FoLPs, it is not clear how such an encoding would work due of PU . An open answer set of P is an open interpreta- to the special form of their forest model property. Finally, tion (U, M ) of P , with M an answer set of PU . For every FEAs were used to encode satisfiability checking of ZOIQ atom a ∈ M , where (U, M ) is an open answer set of P , concepts (Calvanese, Eiter, and Ortiz 2009). level(a, M(PUM ) = M ) is finite (Heymans 2006). Trees and forests: we introduce notation for trees and Preliminaries forests which extend those in (Vardi 1998). Let · be a con- catenation operator between sequences of constants or nat- We start by introducing the open answer set syntax and se- ural numbers, N+ be the set of positive integers, and hN+ i mantics (Heymans, Van Nieuwenborgh, and Vermeir 2008). be the set of all sequences of positive integers formed using We assume countably infinite disjoint sets of constants, vari- the concatenation operator. We denote with ε the empty se- ables, and predicate symbols. Terms and atoms are defined quence: for every constant or natural number c, c · ε = c. A as usual. We refer to an atom where the predicate symbol is tree T with root c, also denoted as Tc , is a set of nodes, where unary or binary, as a unary or binary atom, resp. A literal is each node is a sequence of the form c · s, where s ∈ hN+ i, an atom a or a negated atom not a. We allow for inequality and for every x · d ∈ Tc , d ∈ N+ , it must be the case that literals of the form s 6= t, where s and t are terms. A literal x ∈ Tc . When the root of the tree is irrelevant, we will sim- that is not an inequality literal will be called a regular literal. ply refer to the tree as T . For a set S of literals or (possibly negated) predicates, Given a tree T , its set of arcs is AT = {(x, y) | x, y ∈ S + = {a | a ∈ S} and S − = {a | not a ∈ S}. If S is a T, ∃n ∈ N+ .y = x · n}. We denote with succT (x) = {y ∈ set of (possibly negated) predicates of arity n and t1 , . . . , tn T | y = x · i, i ∈ N + } the successors of a node x in T . For are terms, then S(t1 , . . . , tn ) = {l(t1 , . . . , tn ) | l ∈ S}. For a node y = x · i ∈ T , precT (y) = x. a set S of atoms, not S = {not a | a ∈ S}. A forest F is a set of trees {Tc | c ∈ C}, where C is a A program is a finite set of rules r : α ← β, where α is a finite set of arbitrary constants. The set of nodes, NF , and finite set of regular literals and β is a finite set of literals. We the set of arcs, AF , of a forest F are defined as: NF = denote as head(r)/body(r) the set α/β, where α/β stands for ∪T ∈F T , and AF = ∪T ∈F AT , resp. For a node x ∈ NF , a disjunction/conjunction. let succ F (x) = succ T (x), where x ∈ T and T ∈ F . For a Atoms, literals, rules, and programs that do not contain node y = x · i ∈ T and T ∈ F , precF (y) = precT (y) = x. variables are ground. For a rule or a program R, let vars(R), An interconnected forest EF is a tuple (F, ES ), where preds(R), and cts(R) be the sets of variables, predicates, F = {Tc | c ∈ C} is a forest and ES ⊆ NF × C. The sets and constants that occur in R, resp. A universe U for P is of nodes NEF and arcs AEF of an interconnected forest EF are defined as: NEF = NF , and AEF = AF ∪ ES , resp. writtenBy, and wrote as being free. Finally, there are two A Σ-labelled forest is a tuple (F, f ) where F is an inter- facts (unary rules with empty bodies): f1 and f2 . connected forest/tree and f : NF → Σ is a labelling func- tion, with Σ being a set of arbitrary symbols. r1 : LitLover (X ) ← read (X , Y1 ), read (X , Y2 ), Novel (Y1 ), Novel (Y2 ), Y1 6= Y2 r2 : Novel (X ) ← wrBy(X , Y ), Novelist(Y ) Forest Logic Programs r3 : Novelist(X ) ← wrote(X , Y ), Novel (Y ) Forest Logic Programs (FoLPs) are a fragment of OASP r4 : read (X , Y ) ∨ not read (X , Y ) ← which have the forest model property. They allow only for r5 : wrBy(X , Y ) ∨ not wrBy(X , Y ) ← unary and binary predicates and tree-shaped rules. The tree- r6 : wrote(X , Y ) ∨ not wrote(X , Y ) ← like structure of rules refers to the chaining pattern of rule f1 : Novel (a) ← variables: one variable can be seen as the root of a tree f2 : Novelist(b) ← and the others as descendants such that for every arc in the tree, there is a positive binary literal in the body which con- For a FoLP P , we denote with upr (P ), bpr (P ), urul (P ), nects the two corresponding variables. Inequalities between and brul (P ), the sets of unary and binary predicates and ‘successor’ variables can also appear in the body of such a unary and binary rules which occur in P , resp. rule; we will refer to the set of literals in the body of a rule For a unary rule r of type (3), the degree of r, denoted as formed only with the ‘root’ variable as the ‘local part’ and deg(r), is the number k of successor variables which appear to the remaining part as the ‘successor part’. FoLPs allow in the rule. Intuitively, it indicates the maximum number of also for so-called ‘free’ rules, which are rules of the form: successor individuals needed to make the body of the rule p(t̃) ∨ not p(t̃) ← , where p is a unary/binary predicate true. The degree of a free rule is 0. For a unary predicate and ~t is a unary/binary tuple of terms. p: deg(p) = max{deg(r) | p ∈ preds(head(r))}. P Finally, the degree of a FoLP P is deg(P ) = p∈upr (P ) deg(p). Definition 1 A forest logic program (FoLP) is an open an- It over-approximates the number of successor individuals swer set program with only unary and binary predicates, and needed to satisfy all atoms of the form p(x), where p ∈ s. t. a rule is either: upr (P ), for a given individual x. • a free rule: Example 2 Let P be the FoLP from Example 1. Then, a(s) ∨ not a(s) ← , (1) deg(LitLover) = 2, deg(N ovel) = 1, deg(N ovelist) = 1, or and thus, deg(P ) = 4. f (s, t) ∨ not f (s, t) ← (2) Forest models: The forest model property of an OASP P is • a unary rule: as follows: if a unary predicate p is satisfiable, then there a(s) ← β(s), (γi (s, ti ), δi (ti ))1 6i6m , ψ (3) exists a model which satisfies p that can be seen as an inter- S connected forest. The forest contains for each constant in P with ψ ⊆ 16i6=j6m {ti 6= tj } and m ∈ N, a tree having the constant as root, and possibly an additional • or a binary rule: tree with an anonymous root. The predicate checked to be satisfiable, p, belongs to the label of one of the root nodes. f (s, t) ← β(s), γ(s, t), δ(t), (4) Definition 2 Let P be a program. A predicate p ∈ upr (P ) where in each rule above: is forest satisfiable w.r.t. P if there exist an open answer set – a is a unary predicate, and f is a binary predicate, (U, M ) of P ; an interconnected forest EF = ({Tρ } ∪ {Ta | – s, t, and (ti )16i6m are distinct terms, a ∈ cts(P )}, ES ), where ρ is a constant, possibly from – β, δ, and (δi )16i6m are sets of (possibly negated) cts(P ); and a labelling function ef : {Tρ } ∪ {Ta | a ∈ unary predicates, cts(P )} ∪ AEF → 2preds(P ) such that: – γ, and (γi )16i6m are sets of (possibly negated) binary • p ∈ ef (ρ), predicates, • U = NEF , – inequality does not appear in any γ: 6= ∈ / γm , for 1 6 • ef (x) ∈ 2upr (P ) , when x ∈ Tρ ∪ {Ta | a ∈ cts(P )}, m 6 k, and 6=∈ / γ; • ef (x) ∈ 2bpr (P ) , when x ∈ ATρ , – there is a positive atom that connects the head term s • M = {p(x) | p ∈ ef (x), x ∈ NEF } ∪ {f (x, y) | f ∈ with any successor term which is a variable: γi+ 6= ∅, ef (x, y), (x, y) ∈ AEF }, and if ti is a variable, for every 1 6 i 6 m, and γ + 6= ∅, if t is a variable. • for every (z, z · i) ∈ AEF : ef (z, z · i) 6= ∅. A predicate q is free if it occurs in a free rule in P . We call such a pair (U, M ) a forest model. A program P has the forest model property, if every unary predicate p that Example 1 The following program P is a FoLP: it de- is satisfiable w.r.t. P , is forest satisfiable w.r.t. P . scribes the fact that somebody who has read two different novels is a literature lover (unary rule r1 ), a novel is some- Proposition 1 FoLPs have the forest model property. thing written by a novelist (unary rule r2 ), and a novelist Example 3 Consider again the FoLP P from Example 1. is somebody who wrote at least one novel (unary rule r3 ). Figure 1 a) depicts a forest model which satisfies the unary There are three free rules describing binary predicates read, predicate LitLover. Intuitively, the predicate is satisfied LitLover N ovel N ovelist LitLover N ovel For a set Y , we denote with B + (Y ) the set of posi- ρ read a ρ read a tive Boolean formulas over Y , where true and f alse are b also allowed and where ∧ has precedence over ∨. For a read N ovel read set X ⊆ Y and a formula θ ∈ B + (Y ), we say that wrBy ρ1 X satisfies θ iff assigning true to elements in X and as- wrBy N ovelist signing false to elements in Y − X makes θ true. For ρ1 ρ11 b > 0, let Db = {h0i, h1i, . . . , hbi} ∪ {[0], [1], . . . , [b]} ∪ {−1, ε, hrooti, [root]}. N ovel wrote ... A fully enriched automaton (FEA) is a tuple A = a) b) hΣ, b, Q, δ, q0 , Fi, where Σ is a finite input alphabet, b > 0 is a counting bound, Q is a finite set of states, δ : Q × Σ → Figure 1: Forest model (a)/tentative forest model (b) for P B + (Db × Q) is a transition function, q0 ∈ Q is an initial state, and F = {F1 , F2 , . . . , Fk }, where F1 ⊆ F2 ⊆ . . . ⊆ Fk = Q is a parity acceptance condition. The number k of at the anonymous root ρ as there are two distinct read- sets in F is the index of the automaton. successors of ρ where N ovel holds: a and ρ1, and thus A run of a FEA on a labeled forest (F, V ) is an NF × Q- LitLover(ρ) is ‘supported’ by a ground version of rule r1 . labeled tree (Tc , r) such that: In turn, N ovel holds at ρ1 as it is supported by rule r2 • r(c) = (d, q0 ), for some root d in F , and grounded such that X is replaced with ρ1 and Y is replaced with b. Note that every atom in the model is finitely sup- • for all y ∈ Tc with r(y) = (x, q) and δ(q, V (x)) = θ, ported: there is no infinite chain of dependencies of atoms there is a (possibly empty) set S ⊆ Db × Q such that S in the model. This is a property of (open) answer sets also satisfies θ and for all (d, s) ∈ S, the following hold: known as ‘well-supportedness’ (Fages 1991). – if d ∈ {−1, ε}, then x · d is defined and there is j ∈ N+ Consider in contrast the tentative model depicted in Fig- such that y · j ∈ Tc and r(y · j) = (x · d, s); ure 1 b). There, N ovel(ρ1) is motivated by a wrBy- – if d = hni, then there is a set M ⊆ succF (x) of cardi- successor where N ovelist holds, which in turn is motivated nality n + 1 such that for all z ∈ M , there is j ∈ N+ by a wrote-successor where N ovel holds, etc. The interpre- such that y · j ∈ Tc and r(y · j) = (z, s); tation is not a model, as N ovel(ρ1) is not finitely motivated. – if d = [n], then there is a set M ⊆ succF (x) of cardi- One of the main challenges when designing algorithms to nality n such that for all z ∈ succF (x) − M , there is reason with FoLPs is ensuring that every atom in a model is j ∈ N+ such that y · j ∈ Tc and r(y · j) = (z, s); well-supported. – if d = hrooti (d = [root]), then for some (all) root(s) As explained in the Introduction, FoLPs can be used to c ∈ F there exists j ∈ N+ such that y · j ∈ Tc and simulate reasoning with SHOQ ontologies. Thus, they can r(y · j) = (c, s); be viewed as an integrative formalism for reasoning with If θ above is true, then y does not need to have successors. both ontologies and rules: (Feier and Heymans 2009) intro- Moreover, since no set S satisfies θ = f alse, there cannot duces so-called f-hybrid knowledge bases (fKBs) which are be any run that takes a transition with θ = f alse. A run is pairs of the form (Σ, P ), where Σ is a SHOQ KB and P is accepting if each of its infinite paths π is accepting, that is if a FoLP. The semantics of fKBs is defined in terms of pairs the minimum i for which Inf (π)∩Fi 6= ∅, where Inf (π) is of interpretations, one for each component, which share the the set of states occurring infinitely often in π, is even. The same domain and which agree on the interpretation of com- automaton accepts a forest iff there exists an accepting run mon symbols between the two components. The salient fea- of the automaton on the forest. The language of A, denoted ture of f-hybrid KBs is that they impose no restriction on the L(A), is the set of forests accepted by A. We say that A is occurrence of DL symbols in the FoLP KB. non-empty if L(A) 6= ∅. A concept/unary predicate satisfiability preserving, poly- nomial, and modular translation Θ from SHOQ to FoLPs is Theorem 1 (Corollary 4.3 (Bonatti et al. 2008)) Given a provided in (Feier and Heymans 2009). The translation ex- FEA A = hΣ, b, Q, δ, q0 , Fi with n states and index k, tends to fKBs as follows: given an fKB (Σ, P ), its transla- deciding whether L(A) = ∅ is possible in time (b + 3 2 2 tion is simply Θ(Σ) ∪ P . Thus, any reasoning procedure for 2)O(n ·k ·log k·log b ) . FoLPs can be employed to reason with fKBs. More details about the semantics, translation, and an extended example From Forest Logic Programs to Fully can be found in (Feier and Heymans 2013). Enriched Automata In this section we encode satisfiability checking of unary Fully Enriched Automata predicates with respect to FoLPs as emptiness checking for Fully enriched automata (FEAs) were introduced in (Bonatti FEAs. et al. 2008) as a tool to reason in hybrid graded µ-calculus. We start by introducing for every FoLP P and unary pred- They accept forests as input. We describe them following icate p a class of FEAs Ap,P ρ,θ , where ρ is one of cts(P ) (Bonatti et al. 2008). or a new anonymous individual and θ : cts(P ) ∪ {ρ} → 2upr (P )∪cts(P )∪{ρ} is a function which has the following ^ properties: oi ∈ θ(oi ), and oj ∈ / θ(oi ), for every oi , oj ∈ δ(q0 , σ) = (hrooti, qo ) (5) cts(P ) ∪ {ρ}, such that oi 6= oj . Furthermore, p ∈ θ(c), o∈cts(P )∪{ρ} where c is one of cts(P ) ∪ {ρ} and c is ρ if ρ ∈ / cts(P ). In every such state qo , it should hold that o and only o Intuitively Ap,P ρ,θ will accept forest models of p with respect is part of the label. Furthermore, the automaton justifies the to P encoded in a certain fashion: in particular, for every presence and absence of each unary predicate a and each root in the forest model, the root node will appear in its own adorned upward binary predicate in the label1 by entering label; function θ fixes a content for the label of each root of states qo,a , qo,o0 ,f , qo,a , and qo,o0 ,f resp. At the same time accepted forest models. every successor of the constant node is visited in state q1 . In the following, let d = deg(P ). We will also denote Let coP = cts(P ) ∪ {ρ} − {o}. Then: with PATP the set {∗} ∪ cts(P ) of term patterns, where ∗ stands for a generic anonymous individual: we say that ^ ^ ^ δ(qo , σ) = o ∈ σ ∧ o0 ∈ /σ∧ (ε, qo,a ) ∧ a term t matches a term pattern pt, and write t 7→ pt iff o0 ∈co a∈θ(o) a∈θ(o) / t = pt, when t is a constant. In all other cases, the match ^ P ^ (6) trivially holds. Term patterns will be used in our encoding as (ε, qo,a ) ∧ (ε, qo,o0 ,f ) ∧ (ε, qo,o0 ,f ) ∧ ([0], q1 ) a unification mechanism between terms occurring in a FoLP ↑o f 0 ∈θ(o) ↑o f 0 ∈θ(o) / (variables and constants) and elements in a universe (anony- mous individuals and constants): a variable will match with Whenever the automaton finds itself in state q1 it tries a constant or an anonymous individual, but a constant will to motivate the presence and absence of each unary and adorned binary predicate in its label and then it recursively match only with itself. The automata Ap,P ρ,θ will run on enters the same state into each successor of the current node. forests labelled using the following alphabet: Σ = 2S , where It also ensures that for each integer 1 6 k 6 d, the labels of S = upr (P ) ∪ {1, . . . , d} ∪ cts(P ) ∪ {ρ} ∪ {↑of | f ∈ each but one successor do not contain k: bpr (P )} ∪ {↓tf | f ∈ bpr (P ), t ∈ PATP }. ^ ^ ^ Unlike the case for forest models, the arcs of forests ac- δ(q1 , σ)=([0], q1 )∧ ([1], q¬k )∧ (ε, q∗,a ) ∧ (ε, q∗,a )∧ cepted by FEAs are not labelled: as such, binary predi- 16k6d a∈σ a∈σ / cates occur in the label of nodes in an adorned form. These ^ ^ ^ ^ (7) (ε, qt,∗,f ) ∧ (ε, qt,∗,f ) ∧ (ε, q∗,o0 ,f ) ∧ (ε, q∗,o0 ,f ) adorned predicates are either of the form ↓tf , in which case ↓tf ∈σ ↓tf ∈σ 0 0 / ↑o f ∈σ ↑o f ∈σ / they represent an f -link between the predecessor of the la- belled node, which has term pattern t and the node itself, or δ(q¬k , σ) = k ∈/σ (8) of the form ↑of , in which case the current node is linked to a constant o from P via the binary predicate f . Addition- To motivate the presence of a unary/binary predicate in ally, besides unary predicates, labels might contain natural the label of a node, the automaton checks whether the given numbers and constants, which will be used as an addressing predicate is free (we assume that f ree(a) evaluates to true mechanism for successors of a given node and nodes which if a is free, and, to false, otherwise) or finds a unary/binary stand for constants in accepted forests, resp. The set of states rule which supports the predicate. Note the distinction con- of the automaton are as follows: Q = Qi ∪ Q+ ∪ Q− , with: cerning the term pattern for the node where the predicate has to hold. In the case of unary predicates, if the node is a • Qi = {q0 , q1 , qo , q¬k }, constant, there is first a preliminary check that we are at the • Q+ = {qt,a , qt,ra , qt1 ,t2 ,u , qt1 ,t2 ,rf , qk,t,∗,u }, and right node - this is needed as later the automaton will visit all roots in this state. In the case of binary predicates, depending • Q− = {qt,a , qt,ra , qt1 ,t2 ,u , qt1 ,t2 ,rf , qk,t,∗,u }, on the term pattern, the label is checked for different types of adorned binary atoms. In all cases, only rules whose head where o ∈ cts(P ) ∪ {ρ}, a ∈ upr (P ), f ∈ bpr (P ), terms match the given term patterns are chosen to motivate u is of the form a, f , not a or not f , k ∈ {1, . . . , d}, the presence of predicates in the label. ra ∈ urul (P ), rf ∈ brul (P ), and t, t1 , t2 ∈ PATP . We will refer to Q+ and Q− as the positive and the negative  _  δ(q∗,a , σ) = a ∈ σ ∧ f ree(a) ∨ (ε, q∗,ra ) (9) states of Ap,P ρ,θ , resp. Intuitively, positive states are used to ra :a(s)←β 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 δ(qo,a , σ) = o ∈ / σ ∨ a ∈ θ(o) ∧ f ree(a) ∨ (ε, qo,ra ) (10) q0 , the initial state, q1 , a state which will be visited recur- ra :a(s)←β, s7→o sively in every node of the forest, qo , a state corresponding to the initial visit of constant nodes, and q¬k , a state which  _  δ(qt,∗,f , σ) =↓vf ∈ σ∧ f ree(f )∨ (ε, qv,∗,rf ) (11) asserts that for every node in an accepted forest there must rf :f (s,v)←β, be at most one successor which has k in the label. s7→t, We describe in detail the transition function of Ap,P ρ,θ . The v7→∗ initial transition prescribes that the automaton visits a root 1 As constants have no predecessors in the forest, there will be of the forest in state qo , for every o ∈ cts(P ) ∪ {ρ}: no adorned downward predicates in the label.  _  ^ ^ δ(qt,o,f , σ) =↑of ∈ σ ∧ f ree(f )∨ (ε, qt,o,rf ) (12) δ(qt,o,rf , σ) = (ε, q∗,t,u ) ∧ (ε, qt,o,u ) (22) rf :f (s,v)←β, u∈β u∈γ∪δ s7→t, v7→o In the following, we describe the transitions of the au- Let ra : a(s) ← β(s), (γi (s, vi ), δi (vi ))16i6m , ψ be a tomaton in the negative states, i.e. the states which are used unary rule. Then, we denote with Jra a multiset {ji | 1 6 to motivate the absence of certain unary/binary predicates in i 6 m, ji ∈ {1, . . . , d} ∪ cts(P )} s. t.: the labels of the forest. If one ignores the checks for the ab- • for every ji ∈ Jra , vi ∈ cts(P ) implies ji = vi , and sence of unary/adorned binary predicates in the label of the • for every ji , jl ∈ Jra , vi 6= vl ∈ ψ implies ji 6= jl . current node, the transition rules can be seen as dual versions of the ones for the counterpart positive states. Intuitively, a multiset provides a way to satisfy the successor part of a unary rule in a forest model by identifying the suc- ^ δ(q∗,a , σ) = a ∈ /σ∧ (ε, q∗,ra ) (23) cessor terms of the rule with either successors of the current ra :a(s)←β element in the model or constants in the program. We next describe the transition function for unary rules: δ(qo,a , σ) = o ∈ / σ∨a∈ / θ(o) ∧ ^ (ε, qo,ra ) (24) ra :a(s)←β, d ^ ^ s7→o ^ ^ δ(qt,ra , σ) = (ε, q∗,t,u ) ∧ ∃Jra . (h0i, ^ u∈β k=1ji =ku∈γi ∪δi δ(qt,∗,f , σ) =↓tf ∈ /σ∧ (ε, qv,∗,rf ) (25) ^ ^ ^  (13) rf :f (s,v)←β, qk,t,∗,u ) ∧ (ε, qt,o,u ) s7→t, v7→∗ o∈cts(P ) ji =o u∈γi ∪δi ^ δ(qt,o,f , σ) =↑of ∈ /σ∧ (ε, qv,∗,rf ) (26) State qk,t,∗,u enforces that the (possibly negated) unary or rf :f (s,v)←β adorned binary predicate u is (is not) part of the label of the s7→t, v7→o k-th successor of a given node; we thus define: _ d _ _ _ (ε, q∗,t,u ) ∨ ∀Jra . ^ δ(qk,t1 ,t2 ,u , σ) = k ∈ σ ∧ j∈ / σ ∧ (ε, qt1 ,t2 ,u ) (14) δ(qt,ra , σ) = ([0], u∈β k=1 ji =k u∈γi ∪δi j6=k _ _ _ (27) The state qt1 ,t2 ,u can be seen as a multi-state with differ- qk,t,∗,u ) ∨ (ε, qt,o,u ) o∈cts(P ) ji =o u∈γi ∪δi ent transitions depending on its arguments (two transitions have already been introduced as rules (11) and (12) above): δ(qk,t,∗,u , σ) = k ∈ / σ ∨ (ε, qt,∗,u ) (28) 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 (ε, q∗,a ),  if t2 = ∗ and u = a (29) to constant o: note that, as it is not possible to jump directly    ([root], qo,a ), if t2 = o and u = a (30) to a given root node in the forest, nor to enforce that there  a ∈ σ,  if t2 = ∗ and u = not a (31) will be a single root node corresponding to each constant, in δ(qt1 ,t2 ,u ), σ) = a ∈ θ(o), if t2 = o and u = not a (32) transition (17) we visit each root node in state qo,a :    t ↓f ∈ σ, if t2 = ∗ and u = not f (33)      o ↑f ∈ θ(o), if t2 = o and u = not f (34)    (ε, q∗,a ), if t2 = ∗ and u = a (15)     ([root], qo,a ), if t2 = o and u = a (16) _ _  a ∈ / σ, if t2 = ∗ and u = not a (17) δ(qt,∗,rf , σ) = (−1, q∗,t,u ) ∨ (ε, qt,∗,u ) (35)  δ(qt1 ,t2 ,u , σ) = u∈β u∈γ∪δ   a ∈/ θ(o), if t2 = o and u = not a (18)   ↓t ∈  if t2 = ∗ and u = not f (19) _ _   f / σ, δ(qt,o,rf , σ) = (ε, q∗,t,u ) ∨ (ε, qt,o,u ) (36)   o ↑f ∈ / θ(o), if t2 = o and u = not f (20) u∈β u∈γ∪δ For binary rules: rf : f (s, v) ← β(s), γ(s, v), δ(v), when Finally we specify the parity acceptance condition. The v is grounded using an anonymous individual, the check in- index of the automaton is 2, with F1 = {qt,a , qt1 ,t2 ,f | a ∈ volves looking to the predecessor node to see if the local part upr (P ), f ∈ bpr (P ), t, t1 , t2 ∈ PATP } and F2 = Q. Intu- of the rule is satisfied. When v is grounded using a constant, itively, paths in a run of the automaton correspond to depen- the local part of the rule is checked at the current node and dencies of literals in the accepted model and by disallowing the successor part at the respective constant. Note that the the infinite occurrence on a path of states associated to atoms first term pattern in the first conjunct in both rules (21) and in the model we ensure that only well-supported models are (22) is irrelevant as β contains only unary predicates: accepted. Theorem 2 Let P be a FoLP and let p be a unary predi- cate symbol. Then, p is satisfiable w.r.t. P iff there exists an ^ ^ δ(qt,∗,rf , σ) = (−1, q∗,t,u ) ∧ (ε, qt,∗,u ) (21) u∈β u∈γ∪δ automaton Ap,P p,P ρ,θ such that L(Aρ,θ ) 6= ∅. Proof Sketch. (⇒): Assume p is satisfiable w.r.t. P . Then, • r(w) = (y, qt,o,rf ) implies ↑of ∈ / l(y). by Prop. 1, p is satisfied by a forest model (U, M ). Let (EF, ef ), with EF = (F, ES) be the labelled forest which We show how the invariant is preserved in two cases of induces (U, M ), as in Definition 2. Then, let l : {Tc | c ∈ the construction: cts(P ) ∪ {ρ}} be a labelling function such that for every • Assume r(w) = (y, qt,a ), for some w ∈ Tr . Then, from y ∈ {Tc | c ∈ cts(P ) ∪ {ρ}}, l(y) is the least set con- the IH: a ∈ l(y), and a(y) ∈ M . Then, there must be a taining: (i) ef (y), (ii) {↑of | f ∈ ef (y, o), o ∈ cts(P )}, finite n such that level(a(y), M ) = n and some rule s in (iii) {↓yf | f ∈ ef (z, y), z = precF (y), z ∈ / cts(P )}, PUM such that maxb∈body(s) (level(b, M )) = n − 1 (from (iv) {↓zf | f ∈ ef (z, y), z = precF (y), z ∈ cts(P )}, which a(y) has been derived at iteration n). Let ra be the (v) {y}, when y ∈ cts(P ) ∪ ρ, and (vi) {i} if y = z · i. rule in P from which s has been derived and let w · i be We define an automaton Ap,P a successor of w in Tr such that r(w · i) = (y, qt,ra ). The ρ,θ which accepts (F, l). Let ρ be the same as its homonym in the considered forest invariant is preserved. model and let θ be such that θ(o) = l(o), for every o ∈ • Assume r(w) = (y, qt,ra ), for some w ∈ Tr . Then, cts(P ) ∪ {ρ}. We construct a run (Tc , r) of Ap,P ρ,θ on (F, l) from the IH: a ∈ l(y), a is not free, and there exists by first setting r(c) = (φ, q0 ), where φ is the root of some some rule s in PUM derived from ra : a(y) ← β + (y) ∪ S + + forest in F . Then, for each o ∈ cts(P ) ∪ {ρ}, we introduce 16i6m (γi (y, zi ) ∪ δi (zi )) such that M |= body(s) a successor of c, c · i, such that r(c · i) = (o, qo ). and maxb∈body(s) (level(b, M )) < level(a(y), M ). Note Sm We then proceed inductively with the construction by that M |= β(y) ∪ i=1 (γi (y, zi ) ∪ δi (zi )). As (U, M ) maintaining the following invariant, for each w ∈ Tr : is a forest model, each zm must be of the form y · k, for • r(w) = (y, q∗,a ) implies a ∈ l(y); some 1 6 k 6 d, or of the form o ∈ cts(P ). Let Jra be a multiset such that ji = zi , if zi ∈ cts(P ) and ji = k if • r(w) = (y, qo,a ) implies o ∈/ l(y) or a ∈ θ(o); zi = y · k. Then, we introduce the following successors • r(w) = (y, qt,ra ) implies a ∈ l(y), a is not free, and there of w in Tc (denoted just by their label): is a rule s ∈ PUM derived from ra such that head(s) = – (y, q∗,t,u ), for every u ∈ β: the invariant holds as M |= a(y), M |= body(s), and maxb∈body(s) (level(b, M )) < β(y). level(a(y), M ); – (y · k, qk,t,∗,u ), for every 1 6 k 6 d, i such that ji = k, • r(w) = (y, qt,∗,u ) implies a ∈ l(y), if u = a; a ∈ / l(y), if and u ∈ γi ∪ δi : the invariant holds as M |= γi (y, y · u = not a; ↓tf ∈ l(y), if u = f ; ↓tf ∈ / l(y), if u = not f ; k) ∪ δi (y · k). It is also the case that k ∈ l(y · k) and • r(w) = (y, qt,o,u ) implies a ∈ l(o), if u = a; a ∈ / l(o), if j∈/ l(y · k), for every 1 6 j 6= k leqd. u = not a; ↑of ∈ l(y), if u = f ; ↑tf ∈ / l(y), if u = not f ; – (y, qt,o,u ), for every o and i such that ji = o and u ∈ γi ∪ δi : the invariant holds as M |= γi (y, o) ∪ δi (o). • r(w) = (y, qk,t,∗,u ) implies k ∈ l(y), and j ∈ / l(y), for every 1 6 j 6= k 6 d; a ∈ l(y), if u = a; a ∈ / l(y), if The invariant ensures the existence of a run. We next u = not a; ↓tf ∈ l(y), if u = f ; ↓tf ∈ / l(y), if u = not f ; show that every run Tc constructed as above is accepting, i.e. on every path of Tc there are finitely many occurrences • r(w) = (y, qt,∗,rf ) implies ↓tf ∈ l(y), f is not free, of states of the form qt,a or qt1 ,t2 ,f . Assume that every ele- and there is a rule s ∈ PUM derived from r such ment w ∈ Tc for which r(w) = (y, qt,a ), r(w) = (y, qt,∗,f ), that head(s) = f (precF (y), y), M |= body(s), and or r(w) = (y, qt,o,f ) is annotated with level(a(y), M ), maxb∈body(s) level(b, M ) < level(f (precF (y), y), M ); level(f (prec(y), y), M ), or level(f (y, o), M ), resp. From • r(w) = (y, qt,o,rf ) implies ↑of ∈ l(y), f is not free, the invariant of the construction it follows that level anno- tations decrease along each path of Tc . But the level of ev- and there is a rule s ∈ PUM derived from r such that ery atom in an open answer set is finite. Thus, the number head(s) = f (y, o), M |= body(s), and maxb∈body(s) of level annotations, and consequently the number of occur- level(b, M ) < level(f (y, o), M ); rences of such states must be finite. • r(w) = (y, qt,a ) implies a ∈ / l(y); (⇐): Assume that there exists an automaton Ap,P ρ,θ such • r(w) = (y, qt,ra ) implies a ∈ / l(y); p,P that L(Aρ,θ ) 6= ∅. Then, there exists a labelled forest • r(w) = (y, qt,∗,u ) implies a ∈ / l(y), if u = a; a ∈ l(y), if (F 0 , f 0 ) and an accepting run (Tc , r) on (F 0 , f 0 ) such that t / l(y), if u = f ; ↓tf ∈ l(y), if u = not f ; u = not a; ↓f ∈ r(c) = (φ, q0 ), for some root φ in F 0 . Let F be the for- est containing the nodes y ∈ NF 0 for which either (i) • r(w) = (y, qt,o,f ) implies a ∈ / l(o), if u = a; a ∈ l(o), if there exists some w ∈ Tc such that r(w) = (y, qo ) or u = not a; ↑of ∈ / l(y), if u = f ; ↑tf ∈ l(y), if u = not f ; (ii) precF 0 (y) ∈ NF and there exists some w ∈ Tc such that r(w) = (y, qk,t1 ,t2 ,u ). Assume C is the set of • r(w) = (y, qk,t,∗,u ) implies k ∈ / l(y) or a ∈/ l(y), if roots in F . Then let η : NF → NF ∪ cts(P ) ∪ {ρ} be u = a; a ∈ l(y), if u = not a; ↓tf ∈/ l(y), if u = f ;  oi , if oi ∈ l(y), ↓tf ∈ l(y), if u = not f ; as follows: η(y) = and η(c) · s, if y = c · s, for c ∈ C • r(w) = (y, qt,∗,f ) implies ↓tf ∈ / l(y); let l be the following labeling function for NF : l(y) =  θ(η(y)), if η(y) ∈ cts(P ) Thus, in each case we obtained a contradiction and M |= . f 0 (y), if η(y) ∈ NF − cts(P ) a(η(y)): every unary rule is satisfied by M . Similarly it Also, let: U = {η(y) | y ∈ NF }, M = {a(η(y)) | a ∈ can be shown that every binary rule is satisfied as well. l(y)∩upr (P )∧y ∈ NF }∪{f (η(z), η(z)·i) |↓∗f ∈ l(y)∧y = (i) M is minimal: from the fact that (Tc , r) is accepting, it z · i ∧ y ∈ NF } ∪ {f (η(y), oi ) |↑ofi ∈ l(y) ∧ y ∈ NF }. follows that every path starting at a state in Q+ must be We show that (U, M ) is a forest model of P by showing finite. For every node w ∈ Tc , such that r(w) = (y, q), that: for some q ∈ Q+ , let: (i) M is a model of PUM , i.e every rule in PUM is satisfied by  0, if w has no successors in Tc , d(w) = M : we check that every rule in PUM is satisfied. 1 + maxw·i∈Tc (d(w · i)), otherwise. Let r0 : a(η(y)) ← β + (η(y)), (γi+ (η(y), η(yi )), δi+ ( η(yi )))16i6m be a rule in PUM derived from a unary rule We show by induction on d(w) that: r : a(s) ← β(s), (γi (s, ti ), δi (ti ))16i6m , ψ in P . Let Jr • r(w) = (y, qx,a ) implies a(η(y)) ∈ M(PUM ), be the multiset formed of elements ji , 1 6 i 6 m, such that: / l(y) or a(o) ∈ M(PUM ), • r(w) = (y, qo,a ) implies o ∈  η(yi ), if η(yi ) ∈ cts(P ), • r(w) = (y, qt,ra ) implies PUM contains a rule a(η(y)) ← ji = k, if η(yi ) = η(x) · k. β such that M(PUM ) |= β, Assume M |= body(r0 ), but M 6|= a(η(y)). Then, a ∈ / • r(w) = (y, qt,x,rf ) implies y = z · i, for some i, and PUM l(y) and there must be some w ∈ Tc such that either: contains f (η(z), η(z) · i) ← β such that M(PUM ) |= β, – r(w) = (y, qx,a ). Then, for every rule ra : a(s) ← • r(w) = (y, qt,o,rf ) implies PUM contains f (η(y), o) ← β β ∈ P , there must be a node wra ∈ Tc such that such that M(PUM ) |= β, r(wra ) = (y, qx,ra ). This holds also for rule r. Then, • r(w) = (y, qk,t,x,u ) implies y = z · i, k ∈ l(y), for every one of the following holds: j 6= k: j ∈/ l(y), and: a(η(y)) ∈ M(PUM ), if u = a; ∗ there exists w0 ∈ Tc such that r(w0 ) = (y, qx,x,u ), a(η(y)) ∈/ M(PUM ), if u = not a; f (η(z), η(z) · i) ∈ for some u ∈ β: then, either u = a and (y, q∗,a ) ∈ Tc M(PUM ), if u = f ; f (η(z), η(z) · i) ∈/ M(PUM ), if u = and thus a ∈ / l(y) or M 6|= a(η(y)) – contradiction, not f ; or for some u = not a, a ∈ l(y) or M |= a(η(y)) – contradiction. • r(w) = (y, qt,x,u ) implies y = z · i, and: a(η(y)) ∈ ∗ for every multiset Jra as in transition rule (14) (in- M(PUM ), if u = a; a(η(y)) ∈ / M(PUM ), if u = not a; cluding Jr above) and every ji ∈ Jra either: M f (η(z), η(z) · i) ∈ M(PU ), if u = f ; f (η(z), η(z) · i) ∈ / · there exist 1 6 k 6 d, 1 6 i 6 m, and M(PUM ), if u = not f ; u ∈ γi ∪ δi such that ji = k and for every y · g ∈ F , there is a node wg ∈ Tc such that • r(w) = (y, qt,o,u ) implies: a(o) ∈ M(PUM ), if u = a; r(wg ) = (y · g, qk,t,x,u ): then, there is wk ∈ Tc / M(PUM ), if u = not a; f (η(y), o) ∈ M(PUM ), if a(o) ∈ such that r(wk ) = (y · k, qk,t,x,u ) and either (1) / M(PUM ), if u = not f . u = f ; f (η(y), o) ∈ k∈ / l(y · k) – contradiction, (2) u = a, a ∈/ l(y · k): Induction base: assume w is a leaf in Tc and r(w) = a(η(y · k)) ∈ / M or M 6|= a(η(yi )), and thus (y, q), for some q ∈ Q+ (d(w) = 0). Then, one of the fol- M 6|= δi (η(yi )) – contradiction, (3) u = not a, lowing holds: a ∈ l(y · k): a(η(y · k)) ∈ M or M |= a(η(yi )), • r(w) = (y, qt,a ) and a is free: in this case a(η(y)) ∈ and thus M 6|= δi (η(yi )) – contradiction, (4) u = f , ↓tf ∈ / l(y · k): f (η(y), η(y · k)) ∈ / M or M 6|= M and thus PUM will contain rule a(η(y)) ←. Thus, f (η(y), η(yi )), and thus M 6|= γi (η(y), η(yi )) – a(η(y)) ∈ M(PUM ). contradiction, (5) for some u = not f , ↓tf ∈ l(y · k): • r(w) = (y, qt1 ,t2 ,f ) and f is free: similar to above. f (η(y), η(y · k)) ∈ M or M |= f (η(y), η(yi )), and • r(w) = (y, qt1 ,t2 ,u ) and u = not a or u = not f : from thus M 6|= γi (η(y), η(yi )) – contradiction. the fact that (Tr , t) is a run and transition rules (17-20), · there exists 1 6 i 6 m such that ji = o, for some it follows that a ∈/ l(y) or ↓tf2 (t2 = ∗)/ ↑of (t2 = o) ∈ / o ∈ cts(P ), a node wo ∈ Tc , and u ∈ γi ∪ δi such l(y). Then, the claim follows from the definition of M . that r(wo ) = (y, qt,o,u ): similar to above we reach a contradiction with the fact that M |= γi (η(y), o) ∪ Induction step: consider a non-leaf node w ∈ Tc (d(w) > δi (o). 0). We will analyse the case when r(w) = (y, qt,ra ): then, – r(w) = (y, qo,a ) with η(y) = o. Then, o ∈ / l(y) = for every u ∈ β there is a successor w · iβ,u of w such that θ(o) – contradiction or a ∈ / θ(o) and for every rule r(w · iβ,u ) = (y, qx,t,u ) and there exists a multiset Jra and ra : a(s) ← β ∈ P , such that s 7→ o there must be a successors w · mk,i,u and w · mo,i,u for w such that: node wra ∈ Tc such that r(wra ) = (y, qo,ra ) – similar • r(w·mk,i,u ) = (y ·zk,i,u , qk,t,x,u ), for all pairs (k, i) such to above. that ji = k and u ∈ γi ∪ δi ; • r(w · mo,i,u ) = (y, qt,o,u ), for all pairs (o, i) such that FEAs. This enabled us to establish a tight complexity bound ji = o and u ∈ γi ∪ δi . on this reasoning task for FoLPs. Other reasoning tasks like From the IH, it follows that: consistency checking of FoLPs and skeptical and brave en- tailment of ground atoms can be polynomially reduced to • M(PUM ) |= u(η(y)), for every u ∈ β, and thus satisfiability checking of unary predicates (Heymans 2006); M(PUM ) |= β(η(y)) (*1), thus, the complexity result applies to those tasks as well. • M(PUM ) |= u(η(y), η(y) · zk,i,u ), for every u ∈ γi Also, by virtue of the translation from fKBs to FoLPs, the re- sult applies to fKBs as well: satisfiability checking of unary and M(PUM ) |= u(η(y) · zk,i,u ), for every u ∈ δi predicates w.r.t. fKBs is E XP T IME-complete. Thus, reason- and k ∈ l(η(y) · zk,i,u ): as there is a unique succes- ing with FoLP rules and SHOQ ontologies is not harder sor y · zk of y such that k ∈ l(y · zk ), it follows that: than reasoning with SHOQ ontologies themselves. M(PUM ) |= u(η(y), η(y) · zk ), for every u ∈ γi and In the introduction, we mentioned the special form of M(PUM ) |= u(η(y) · zk ), for every u ∈ δi and thus forest model property as one of the reasons FoLPs cannot M(PUM ) |= γi (η(y), η(y) · zk ) ∪ δi (η(y) · zk ) (*2), be straightforwardly dealt with using 2ATAs. An additional • M(PUM ) |= u(η(y), o), for every u ∈ γi and M(PUM ) |= technical difficulty we had to overcome compared to both u(o)), for every u ∈ δi , where ji = o, and thus encodings using 2ATAs and other encodings using FEAs, M(PUM ) |= γi (η(y), o) ∪ δi (o) (*3). is the fact that FEAs, unlike 2ATAs, cannot explicitly ad- dress successor nodes in runs: they are suitable for encoding From (*1)-(*3) and the fact that ji 6= jl im- graded modalities/number restrictions where the same prop- plies zji 6= S zjl , it follows that M(PUM ) |= erty has to hold/not to hold at a given number of successors. β(η(y)) ∪ 16k6d (γi (η(y), η(y) · zk ) ∪ δi (η(y) · In our encoding, in order to assert that different properties S zk ))ji =k ∪ o∈cts(P ) (γi (η(y), o)∪ δi (o))ji =o , ψ, which hold at different successors (as the structure of FoLP rules is the body of a grounding of ra in PU with head allows), we had to devise an addressing mechanism for suc- a(η(y)). Then, by applying S the reduct one obtains that cessors. Furthermore, as terms occurring in any position in M(PUM ) |= β + (η(y)) ∪ 16k6d (γi+ (η(y), η(y) · zk ) ∪ FoLP rules might be constants, our encoding also made use δi+ (η(y) · zk ))ji =k ∪ o∈cts(P ) (γi+ (η(y), o) ∪ δi+ (o))ji =o , S of a unification mechanism. Finally, as our result shows that FoLPs have the same which is the body of a rule with head a(η(y)) in PUM . complexity as CoLPs, we plan to further investigate the ex- The other cases can be treated similarly. tension of the deterministic AND/OR tableau algorithm for Then, as a ∈ l(y) ∩ upr (P ) implies that there exists a CoLPs (Feier 2014) to FoLPs. As explained in (Feier 2014), node w ∈ Tr such that r(w) = (y, qt,a ), ↓tf ∈ l(y) implies such an extension is far from trivial. that there exists a node w ∈ Tr such that r(w) = (y, qt,x,f ), and ↑of ∈ l(y) implies that there exists a node w ∈ Tr such References that r(w) = (y, qt,o,f ) (from transition rule (7)), it follows Bonatti, P. A.; Lutz, C.; Murano, A.; and Vardi, M. Y. 2008. The that M ⊆ M(PUM ), and thus M is a minimal model of PUM . complexity of enriched µ-calculi. Logical Methods in Computer 2 Science 4(3). Theorem 3 Satisfiability checking of unary predicates w.r.t. Calı̀, A.; Gottlob, G.; and Lukasiewicz, T. 2009. Datalog± : A FoLPs is E XP T IME-complete. unified approach to ontologies and integrity constraints. In ICDT, volume 9, 14–30. Proof Sketch. That the task is E XP T IME-hard follows from Calvanese, D.; Eiter, T.; and Ortiz, M. 2007. Answering reg- the fact that satisfiability checking of unary concepts w.r.t. ular path queries in expressive description logics: An automata- SHOQ ontologies is E XP T IME-complete (Schild 1991); the theoretic approach. In Proc. AAAI, 391–396. latter has been reduced to satisfiability checking of unary predicates w.r.t. FoLPs in (Feier and Heymans 2013). Calvanese, D.; Eiter, T.; and Ortiz, M. 2009. Regular path queries in expressive description logics with nominals. IJCAI 714–720. For the upper bound, we observe that for a given P and p, Calvanese, D.; Giacomo, G. D.; and Lenzerini, M. 2002. 2ATAs there is an exponential number of automata Ap,P ρ,θ (as there make DLs easy. In Proc. DL, 107–118. are an exponential number of possible θ). Each such automa- ton can be constructed in exponential time, and emptiness Eiter, T., and Šimkus, M. 2009. Bidirectional answer set programs with function symbols. In Proc. IJCAI, 765–771. checking for Ap,Pρ,θ can be performed again in exponential Eiter, T.; Ianni, G.; Lukasiewicz, T.; Schindlauer, R.; and Tompits, time. The latter follows from Theorem 1 and the fact that H. 2008. Combining answer set programming with description the branching factor and the number of states of Ap,P ρ,θ are logics for the semantic web. AI 172(12-13). polynomial in the size of P , while its index is constant (viz. Fages, F. 1991. A new fix point semantics for generalized logic 2). Then, from Theorem 2 it follows that satisfiability check- programs compared with the well-founded and the stable model ing of unary predicates w.r.t. FoLPs is in E XP T IME. 2 semantics. New Generation Computing 9(4). Feier, C., and Heymans, S. 2009. Hybrid reasoning with Forest Discussion and Conclusion Logic Programs. In Proc. ESWC, volume 5554, 338–352. Springer. We have described a reduction of satisfiability checking Feier, C., and Heymans, S. 2013. Reasoning with Forest Logic of unary predicates w.r.t. FoLPs to emptiness checking of Programs and f-hybrid knowledge bases. TPLP 3(13):395–463. Feier, C. 2012. Worst-case optimal reasoning with Forest Logic Programs. In Proc. KR 2012. Feier, C. 2014. Reasoning with Forest Logic Programs. PhD thesis (http://tinyurl.com/pbtfsll), TU Wien. Gelfond, M., and Lifschitz, V. 1988. The stable model semantics for logic programming. In Proc. of ICLP’88, 1070–1080. Heymans, S.; Van Nieuwenborgh, D.; and Vermeir, D. 2006. Con- ceptual Logic Programs. AMAI 47(1–2):103–137. Heymans, S.; Van Nieuwenborgh, D.; and Vermeir, D. 2008. Open Answer Set Programming with guarded programs. Transactions on Computational Logic 9(4):1–53. Heymans, S. 2006. Decidable Open Answer Set Programming. PhD thesis, Vrije Universiteit Brussel. Krötzsch, M.; Rudolph, S.; and Hitzler, P. 2008. Description logic rules. In Proc. ECAI, 80–84. IOS Press. Magka, D.; Krötzsch, M.; and Horrocks, I. 2013. Computing stable models for nonmonotonic existential rules. In IJCAI. Motik, B., and Rosati, R. 2010. Reconciling description logics and rules. Journal of the ACM 57(5):30:1–30:62. Motik, B.; Sattler, U.; and Studer, R. 2005. Query answering for OWL-DL with rules. Journal of Web Semantics 3(1):41–60. Rosati, R. 2006. DL+log: Tight integration of description logics and disjunctive Datalog. In Proc. KR, 68–78. Rosati, R. 2008. On combining description logic ontologies and nonrecursive datalog rules. In Proc. RR. Schild, K. 1991. A correspondence theory for terminological log- ics: Preliminary report. In IJCAI, 466–471. Vardi, M. Y. 1998. Reasoning about the past with two-way au- tomata. In Proc. ICALP, 628–641. Springer.