Satisfiability in EL with sets of Probabilistic ABoxes⋆ Marcelo Finger, Renata Wassermann, and Fabio G. Cozman University of São Paulo, São Paulo, Brazil mfinger@ime.usp.br,renata@ime.usp.br,fgcozman@usp.br Abstract. We present ELPA, a probabilistic extension of the lightweight DL EL with a fixed TBox and a set of probabilistic ABoxes, and study the problem of satisfiability in such context. 1 Introduction This work studies an extension of Description Logic EL, called ELPA, that allows for probabilistic assessments on ABoxes. We concentrate on the problem of veri- fying the satisfiability of an ELPA-knowledge base, proposing algorithms for this problem based on recent advances on probabilistic satisfiability (PSAT) [FB11]. Consider an example, adapted from [LS10]. Example 1.1 Two symptoms of Lyme disease are fever and fatigue. As these symptoms are common and the disease is rare, the chance that they are indeed caused by Lyme disease is small. Nevertheless, because the disease is of difficult diagnosis, patients get treated if there is a chance that they have it. The TBox T0 contains the following axioms: And the following ABox A0 : Fatigue ⊑ Symptom Fever(s1 ) Fever ⊑ Symptom hasSymptom(john, s1 ) Lyme ⊑ Disease Fatigue(s2 ) Symptom ⊑ ∃hasCause.Disease hasSymptom(john, s2 ) Patient ⊑ ∃suspectOf.Disease Patient(john) Patient ⊑ ∃hasSymptom.Symptom ∃hasSymptom.(∃hasCause.Lyme)⊑ ∃suspectOf.Lyme Consider also the following probabilistic statements originating from medical experience on symptoms that are caused by Lyme disease. A1 = ∃hasCause.Lyme(s1 ), P (A1 ) ≥ 0.1 A2 = ∃hasCause.Lyme(s2 ), P (A2 ) ≥ 0.2 Now we want to know whether we can consistently assert an upper bound pub for the probability of John having Lyme disease: A3 = ∃suspectOf.Lyme(john), P (A3 ) ≤ pub  The set of statements in the example above is a probabilistic knowledge base. It contains four probability assignments; A0 , which is the conjunction of 5 atomic statements, is assigned probability 1; the other three atomic ABoxes A1 , A2 and A3 get probabilities smaller than 1. ⋆ Work supported by Fapesp Thematic Project 2008/03995-5 (LOGPROB). Authors supported by CNPq grants PQ 302553/2010-0, 304043/2010-9, 305395/2010-6. Our method is an alternative to existing combinations of DL with probabili- ties that impose deterministic restrictions on probabilities. For example, [LS10] assigns probabilities to concepts over a fixed interpretation, forcing the proba- bility of ABoxes to be either 0 or 1. No such deterministic “side effects” occur in our method. Our goal in this work is to formally define the notion of ELPA-knowledge bases and its satisfiability problem and provide algorithms to verify it. Adding probabilities to logic sentences usually adds complexity; e.g. probabilistic 2SAT is NP-complete [GKP88]. We show that ELPA-satisfiability is in NP. 1.1 Related work There have been several proposals to add probabilities to description logics in recent years [LS08]; most of this work is based on various kinds of probabilistic logic [GT07,Hal03]. Probabilistic description logics differ in several dimensions. Some approaches associate probabilities with elements of TBoxes [Jae94,KLP97,CP09], while oth- ers associate probabilities with ABoxes [DS05], and still others combine both kinds of assessments [Luk08]. In this paper we focus on probabilities over ABoxes. As an alternative classification scheme, some logics assign probabilities over elements of the domain [DPP06,DS05,Hei94,Jae94,KLP97,Luk08], while others assign probabilities over interpretations [CL06,DFL08,LS10], with some logics in between [Seb94]. In this paper we focus on probabilities over interpretations. Yet another classification is possible, as we have probabilistic description logics that allow for assessments of stochastic independence, often organized through graphs [CL06,DPP06,KLP97,CP09], and logics that do not allow for assessments of stochastic independence [DS05,Hei94,Jae94,Luk08,LS10]. In this paper we do not allow for stochastic independence. In a sense, our work is a refinement of First Order Probabilistic Logic by Jaumard et al [JFSS06]; however, we use the decidable and tractable logic EL, and we show that our probabilistic version remains in NP. Note that probability assignments remain external to the logic EL; this has the advantage of making it capable of dealing with conditional probabilities of ABox statements in a classical manner, as P (A(a)|B(b)) = P (A(a) ∧ B(b))/P (B(b). A complete treatment of conditional probabilities remains outside the scope of this work. Another related problem is probability inference; that is, determining the maximal and minimal values for pub that leave the knowledge base satisfiable; this problem is also outside the scope of this work. 1.2 Organization of the paper The remainder of the paper is organized as follows. In the next section, we introduce the logic ELPA. We first define the probabilistic assignments that are allowed in the ABox, and then formalise the satisfiability problem for ELPA, showing that it is in NP. We show that the probabilistic knowledge base in ELPA can be translated into a normal form that is used in Section 3, where an algorithm for testing the satisfiability of ELPA is presented. 2 The Probabilistic DL ELPA We introduce ELPA, a probabilistic extension of the polynomial-time Description Logic EL with a fixed TBox and a set of probabilistic ABoxes. We first establish a regular EL vocabulary. Fix countably infinite sets NC , NR , and NI of concept names, role names, and individual names, respectively. The set of EL-concepts is given by the following syntax rules: C ::= A | C ⊓ D | ∃r.C where A ranges over NC , C and D over EL-concepts and r over NR . No negation or disjunction of concepts is expressible in this language. A TBox is a finite set of concept inclusions (CIs) of the form C ⊑ D; TBoxes usually represent an ontology. On the other hand, ABoxes represent instance data and obey the following syntax rules A ::= C(a) | r(a, b) | A ∧ A′ where C and r are as before, a, b ∈ NI and A, A′ range over ABoxes. The standard EL semantics is used for TBoxes and ABoxes, based on inter- pretations I = (∆I , ·I ), where ∆I is a non-empty set called domain and ·I is an interpretation function that maps each each A ∈ NC to a subset AI ⊆ ∆I , each r ∈ NR to a subset rI ⊆ ∆I × ∆I , and each a ∈ NI to an element aI ∈ ∆I ; see [BBL05]. We extend the interpretation I for all concepts in the usual way. So (C ⊓ D)I = C I ∩ DI and (∃r.C)I = {x ∈ ∆I |∃y ∈ ∆I : (x, y) ∈ rI ∧ y ∈ C I }. Then concept inclusion C ⊑ D is satisfied by interpretation I, represented by I |= C ⊑ D iff C I ⊆ DI . Similarly TBox T is satisfied by interpretation I, I |= T , iff I |= C ⊑ D for every C ⊑ D ∈ T . For ABoxes, we say that C(a) is satisfied by I, represented by I |= C(a) iff aI ∈ C I ; similarly, I |= r(a, b) iff (aI , bI ) ∈ rI ; and I |= A ∧ A′ if both I |= A and I |= A′ . If both a TBox T and an ABox A are true under I, we say that the pair (T , A), called a (deterministic) knowledge base, is satisfied by I. The problem of deciding if a deterministic knowledge base (T , A) is satisfiable in EL can be solved in polynomial time [Bra04]. 2.1 Probability Assignments to ABoxes We now introduce probabilities in ABoxes. We deal with probability distribution π over the set of interpretations endowed with a suitable algebra. Let T be a TBox. Given a probability distribution π over the set of all interpretations I, the probability of an ABox A in the context of T is given by the probability of all interpretations that satisfy all of T and A, that is, the probability of {I|I |= A and I |= T }. A probability assignment to an ABox, is an expression of the form P (A) ⊲⊳ p, where A is an ABox, ⊲⊳∈ {≤, ≥, =} and p ∈ Q, 0 ≤ p ≤ 1. Note that probability assignments are external to the logic EL, and are not statements in the logic. Let PA be a set of k probability assignments PA = {P (Ai ) ⊲⊳i pi |1 ≤ i ≤ k}. Then the pair hT , PAi is a probabilistic knowledge base in the DL EL with sets of probability assignments, ELPA. Clearly, all probability assignments in PA are to be evaluated in the context T . The main problem of this work is, given an ELPA probabilistic knowledge base, determine whether there exists a probability distribution π such that, in the context of the TBox T , π satisfies all the assignments in PA; this is the satis- fiability problem for an ELPA-knowledge base. Before we formalize this problem, we must “finitize” the set of all interpretations of a TBox T , as the set IT of all interpretations of a TBox T is uncountably infinite. For that, define an equivalence relation ≃PA ⊆ IT ×IT , where PA = {P (Ai ) = pi |1 ≤ i ≤ k} is a set of probabilistic assignments, such that I ≃PA I ′ iff for every k, 1 ≤ i ≤ k, I |= Ai if and only if I ′ |= Ai ; that is, I and I ′ satisfy the same ABoxes in PA in a context of TBox T . Lemma 2.1 Let n be the number of atomic elements in PA. The relation ≃PA is an equivalence relation on IT × IT and the set of equivalence classes IT /≃PA has at most 2n distinct equivalence classes. Each equivalence class of I/≃PA will be represented by any interpretation I in it. We can now formalise the satisfiability problem for an ELPA-knowledge base hT , PAi. We will write I(A) = 1 for I |= A and I(A) = 0 for I 6|= A. 2.2 The Satisfiability of Probabilistic Knowledge Bases Let n be the number of atomic elements in PA, |PA| = k. Consider I1 , . . . , In′ , n′ ≤ 2 be all the ≃PA -distinct interpretations that satisfy T . Consider a k × n′ matrix A = [aij ] such that aij = Ij (Ai ). The probabilistic satisfiability problem for an ELPA-knowledge base K = hT , PAi is to decide if there is a probability vector π of dimension n′ that obeys the ELPA-restrictions: X Aπ ⊲⊳ p, πi = 1, π ≥ 0. (1) An ELPA-knowledge base K is satisfiable iff its associated ELPA-restrictions (1) have a solution. If π is a solution to (1) we say that π satisfies K. The last two conditions of (1) force π to be a probability distribution. It is convenient to assume that first two conditions of (1) are joined, A is a (k + 1) × n′ matrix with 1’s at its first line, p1 = 1 in vector p(k+1)×1 , so ⊲⊳1 -relation is “=”; we will keep this convention in the rest of the paper. Example 2.2 Recall Example 1.1 with pub = 0.3, where the probability of John having Lyme is at most 30%. We consider only the 3 ABox with prob- abilistic assignments, and only interpretations of these atoms that are jointly consistent with the fixed TBox and the fixed (probability 1) ABox formulas. Consider the following probability distribution π and the probability it assigns to the ABoxes in Example 1.1. π A1 A2 A3 I1 0.75 0 0 0 I2 0.10 0 1 1 I3 0.03 1 0 1 I4 0.12 1 1 1 1.00 0.15 0.22 0.25 It is easy to verify that the interpretations I1 –I4 are all consistent with hT0 , A0 i, so all probability relations are verified by π, so probabilistic database for pub = 0.3 is satisfiable.  Some important questions remain: how to compute a probability distribu- tion when one exists, and whether that probabilistic knowledge base remains satisfiable when pub = 0.05 or not, and how to verify it. This paper presents algorithms for that. An important result of [GKP88] guarantees that a satisfiable knowledge base has a “small” witness: Fact 2.3 If ELPA-restrictions (1) for knowledge base K = hT , PAi with PA = {P (Ai ) = pi |1 ≤ i ≤ k} have a solution, then there are k + 1 columns of matrix A such that the system A(k+1)×(k+1) π = p(k+1)×1 has a solution π ≥ 0. This result is a consequence of Caratheodory’s Theorem [Eck93], which states that if a k-dimensional point is a convex combination of m points, then it is a convex combination of at most k + 1 points among them. Fact 2.3 gives an NP-certificate for the satisfiability of an ELPA-knowledge basel; hence: Corollary 2.4 The ELPA-satisfiability problem is in NP. Finding polynomial-sized certificates is the heart of the matter. We will now study algorithms that solve the ELPA-satisfiability problem. We start by defining a normal form for ELPA-knowledge base. Note that Fact 2.3 is stated for equality only, and we also allow inequalities; the normal form will be useful both for the algorithms and for showing that all those cases can be reduced to equality only, with all probabilistic assignments over atoms only. 2.3 A Normal Form for Probabilistic Knowledge Base For the sake of providing a normal form, we add a few new convenient definitions. Let N0 be a set of 0-ary atomic propositions. A propositional rule is an expression of the form q → A1 or A2 → q, where q ∈ N0 and A1 , A2 ABoxes, with the obvious semantic that I |= q → A1 iff I 6|= q or I |= A1 ; and I |= A2 → q iff I |= q or I 6|= A2 . We extend the notion of ABox such that A ::= C(a) | r(a, b) | q | A ∧ A′ such that q ∈ N0 and C(a), r(a, b), A, A′ are as before; we call q, C(a), r(a, b) atomic ABoxes. If R is a set of propositional rules and A an ABox, R ∪ A is a set of Horn clauses, and thus has a polynomial-time computable minimal model; so the I- satisfiability of R ∪ A reduces to the I-satisfiability of the atomic positive for- mulas in its minimal model. Thus the satisfiability problem of EL with TBoxes, ABoxes and sets of propositional rules can be achieved in polynomial time. We also distinguish deterministic ABoxes, which are assigned probability 1, from probabilistic ABoxes, which are assigned probabilities < 1. We then extend previous definitions with the notion of a set of proposi- tional rules. For the rest of this paper, an extended ELPA-knowledge base is a 4-tuple Ke = hT , R, A, PAi, in which the probabilistic assignment of ABoxes PA is evaluated in an (deterministic) evaluation context consisting of a triple C = hT , R, Ai of TBox, propositional rules and deterministic ABox A; we also represent Ke = hC, PAi. Clearly, an ELPA-knowledge base K is a special case of an extended ELPA-knowledge base Ke the previous view in which R = ∅ and A is part of PA. Now we define the normal form. A knowledge base Ke = hT , R, A, PAi is in (atomic) normal form if PA is of the form PA = {P (yi ) = pi | yi is an atom, 1 ≤ i ≤ k}, with 0 < pi < 1. In this case, PA is an atomic probability assignment evaluated in context C = hT , R, Ai. Clearly, C is a small generalisation of the deterministic knowledge bases of, for instance, [BBL05]. By adding a small number of propositional rules, any knowledge base can be brought into atomic normal form. Theorem 2.5 (Normal Form) For every extended ELPA-knowledge base Ke e there exists an atomic normal form knowledge base Knf that is satisfiable iff Ke is; the former can be obtained from the latter in polynomial time O(k × ℓ), where k = |PA| and ℓ is the largest number of conjuncts in an ABox in PA.  Example 2.6 We transform the knowledge base(s) of Example 1.1 into the normal form. The TBox T0 and deterministic ABox A0 remain the same. We introduce atoms q1 , q2 , q3 for ABoxes A1 , A2 , A3 respectively, which generates the following set or rules R0 : q1 → ∃hasCause.Lyme(s1 ), q2 → ∃hasCause.Lyme(s2 ), ∃suspectOf.Lyme(john) → q3 C0 = hT0 , R0 , A0 i is the evaluation context; the atomic probability assignment is PA0 = { P (q1 ) = 0.1, P (q2 ) = 0.2. P (q3 ) = pub }. The normal form knowledge base is K0e = hC0 , PA0 i. Note that the probability distribution of Example 2.2 does not satisfy K0e when pub = 0.3, but by Theo- rem 2.5 there must exist other interpretations involving q1 , q2 , q3 and rules R0 and another probability distribution π that satisfies K0e .  The following result allows us to see a satisfiable normal form knowledge base e Knf as an interaction between a solution to assignments PA constrained by the EL-decisions of context hT , R, Ai. An interpretation I is hT , R, Ai-consistent if I jointly satisfies T , R and A. Recall that we represent the binary I-evaluation of ABoxes such that I(A) = 1 iff I |= A. Lemma 2.7 is the basis for the ELPA- satisfiability solving algorithm that we present in the next section. Lemma 2.7 A normal form knowledge base Ke = hT , R, A, PAi is satisfiable iff there is a binary (k + 1) × (k + 1)-matrix AKe , such that all of its {0, 1}- columns represent interpretations that are hT , R, Ai-consistent and AKe · π = p has a solution π ≥ 0. 3 An Algorithm for ELPA Satisfiability We present a logic-algebraic algorithm to verify the satisfiability of a normal form knowledge base Ke = hT , R, A, PAi and, if the answer is positive, present a satisfying model in the form of a set of k+1 EL-interpretations, where k = |PA|, and a probability distribution over them. We first establish some terminology. If A is a matrix, Aj is its j-th column and Ai is its i-th line; A(s) is the state of matrix A at step s. If A is a matrix and b a column of compatible dimension, A[j := b] is obtained by replacing A’s j-th column with b. A square matrix that has an inverse is non-singular. A matrix A that satisfies conditions (2) is a feasible solution for PA.       1 ··· 1 π1 1  a1,1 · · · a1,k+1   π2   p1   .. . . ..  ·  ..  =  ..  ,        . . .   .   .  (2) ak,1 · · · ak,k+1 πk+1 pk ai,j ∈ {0, 1}, A is non-singular, πj ≥ 0 We always assume that the lines of A are ordered such that the input probabilities p1 , . . . , pk in (2) are in decreasing order. By Lemma 2.7, hC, PAi has a solution iff there is a partial solution A satisfying (2) such that if πj > 0 then a1,j , . . . , ak,j represent C-consistent interpretations for 1 ≤ i ≤ k, 1 ≤ j ≤ k + 1. We usually abuse terminology calling Aj a C-consistent column. This method is based on PSAT-solving method of [FB11], which is an im- provement on the methods of [KP90,HJ00]; it consists of an algebraic optimisa- tion problem in the form of a special linear program of the form minimize objective functionh|J|, P fi subject to Aπ = p, π ≥ 0, f = j∈J πj and (3) J = {j|Aj is C-inconsistent, πj > 0} which is solved iteratively by the simplex algorithm [BT97]. Matrix A is a (k + 1) × (k + 1) {0,1}-matrix, whose columns represents an EL-interpretations and whose lines represent the atoms occurring in PA. An iterative step s re- ceives a matrix A(s) and employs a column generation method that solves an auxiliary problem; the latter is a logic-based satisfiability problem that em- ploys EL-decision procedure, generates a column that replaces some column in A(s) , obtains A(s+1) and decreases the objective function h|J|, f i, where h|J1 |, f1 i > h|J2 |, f2 i iff 0 ≤ |J1 | < |J2 | or |J1 | = |J2 | and f1 < f2 , until its minimum is reached. The objective function is discussed in Section 3.1. In the iterative method, some columns are not C-consistent and the process is done such that the number of C-consistent columns Aj associated to πj > 0 never decreases. We now define A(0) , the starting feasible solution. For that, consider an empty context C = ∅, that is a knowledge base h∅, PAi. As the elements of p are in decreasing order, consider the {0, 1}-matrix I ∗ = [ai,j ]1≤i,j≤k+1 where ai,j = 1 iff i ≤ j, that is, I ∗ is all 1’s in and above the diagonal, 0’s elsewhere. As p is in decreasing order, I ∗ satisfies h∅, PAi and is called a relaxed solution for hC, PAi. Clearly, I ∗ is a feasible for PA. Make A(0) = I ∗ . Example 3.1 Consider the form of knowledge base in Example 2.6 with pub = 0.3 (left) and pub = 0.05 (right). An initial feasible solution for it is A(0) ·π (0) = p, with atoms ordered in decreasing probability, namely 1 1 1 1 0.7 1 1 1 1 1 0.8 1              0 1 1 1   0.1   0.3  q3  0 1 1 1   0.1   0.2  q2  0 0 1 1  ·  0.1  =  0.2  q  0 0 1 1  ·  0.05  =  0.1  q 2 1 0 0 0 1 0.1 0.1 q1 0 0 0 1 0.05 0.05 q3 On the left, all columns are C-consistent, so the problem is satisfiable with so- lution A(0) and π as above. On the right, the second and third columns of A(0) are C-inconsistent, so the decision is not yet made. The relaxed solution is the initial feasible solution of our method. Further feasible solutions are obtained by generating new {0, 1}-columns and substituting them into a feasible solution, as shown by the following. It is well known from the pivoting in the simplex algorithm that given any {0, 1}-column of the form b = [1 b1 · · · bk ]′ , A[j := b] is a feasible solution. So we simply assume there is a function merge(A, b) that computes it. Our method moves through feasible solutions, at each step generating a column b that decreases the value of the objective function. 3.1 The Objective Function In a feasible solution A such that Aπ = p and π ≥ 0, some columns may not be C-consistent. Let J = {j|Aj is C-inconsistent and πj > 0}; J is the set of column indexes in A corresponding to C-inconsistent columns with non-null associated probability; clearly |J| ≤ k + 1. If J = ∅, we call A a solution. As |J| = 0 when a solution is found, it is one component of the objective function. However, it is Algorithm 3.1 ELPA-satisfiability solver Input: A normal form ELPA knowledge base hT , R, A, PAi. Output: Solution A; or “No”, if unsatisfiable. 1: p := sortDecrescent({1} ∪ {pi |P (yi ) = pi ∈ PA}; 2: A(0) := I ∗ ; s := 0; compute h|J(s) |, f(s) i; 3: while h|J(s) |, f(s) i = 6 h0, 0i do 4: b(s) = GenerateColumn(A(s) , p, C); (s) 5: return “No” if b1 < 0; /* instance is unsat */ 6: A(s+1) = merge(A(s) , b(s) ); 7: increment s; compute h|J(s) |, f(s) i; 8: end while 9: return A(s) ; /* PSAT instance is satisfiable */ not guaranteed that, if a solution exists, we can find a sequence of iterations in which |J| decreases at every step s. The second component of the P objective function is the sum of probabilities of C-inconsistent columns, f = j∈J πj . Note that f and |J| become 0 at the same time, which occurs iff a positive decision is reached. The simplex algorithm with appropriate column generation ensures that, if there is a solution, it can be obtained with finitely many steps of non-increasing f -values. We thus use a combined objective function h|J|, f i ordered lexicographically. We first try to minimise the number of C-inconsistent columns; if this is not possible, then minimise f , keeping J constant. So a knowledge base instance hC, PAi associated to program (3) is satisfiable iff the objective function is min- imal at h0, 0i. Assume there is a function GenerateColumn(A, p, C), presented at Section 3.2, that generates a C-consistent column that decreases the objective function, if one exists; otherwise it returns an illegal column of the form [−1 · · · ]. Algorithm 3.1 presents a method that decides a PSAT instance by solving problem (3). Algorithm 3.1 starts with a relaxed solution for hC, PAi (line 2), and via column generation (line 4) generates another feasible solution (line 6), decreasing the objective function, until either the search fails (line 5) or a solution is found; the latter only occurs with the termination of the loop in lines 3–8, when the objective function reaches h0, 0i. 3.2 Column Generation for ELPA Algorithm 3.1 is, unsurprisingly, almost the same algorithm for PSAT solving in [FB11]; the only difference between the two rests in the column generation method GenerateColumn(A, p, C). It has been shown in [FB11] that to eliminate a C-inconsistent column Aj associated to πj > 0, a new C-consistent column b = [1 y1 . . . yk ]′ to substitute Aj must satisfy the set of linear inequalities: (LRij ) (A−1 −1 ′ j πi − Ai πj )[1 y1 . . . yk ] ≥ 0, 1≤i≤k+1 (4) Such a column is here obtained by a combination of a SAT solver, which guar- antees that (4) is verified, with an EL-solver to guarantee that b is C-consistent. This combination can be done in several ways. (a) By coding the polynomial time EL-decision in a SAT solver. (b) By using EL-theories as an SMT (SAT Modulo Theories) engine. (c) By coupling an EL-solver at the end of the SAT solver, rejecting C-inconsistent answers, and proceeding with the SAT solver after the rejection. The latter option is perhaps the most straightforward and is the one we employ here. Example 3.2 Recall the matrix A(0) in Example 3.1 on the right, whose sec- ond and third columns were C inconsistent. Applying Algorithm 3.1 with column generation as above, all 3 columns generated by the SAT solver were rejected by the EL-solver, so no column could be generated that minimised the objective function in h0, 0i. Therefore the corresponding ELPA-knowledge base is unsatis- fiable.  Theorem 3.3 Algorithm 3.1 with column generation as above is correct and always terminates. 4 Conclusions and Further Work We have introduced the notion of ELPA-knowledge bases and its satisfiability problem, and we have shown that the problem has a finite version that can be tacked by algorithms that resemble PSAT solvers. We have also provided complexity upper bounds for these algorithms. Algorithm 3.1 has the theoretical possibility of generating an exponential number of steps. It remains an open problem to find an example in which such an exponential number of steps occur. It also remains an open problem whether a polynomial time algorithm exists for ELPA-satisfiability. Our plan for future work is to investigate the practical behavior of our algorithms, and to explore logics that allow for probability over TBoxes and for stochastic independence. References [BBL05] Franz Baader, Sebastian Brandt, and Carsten Lutz. Pushing the EL envelope. In IJCAI05, 19th International Joint Conference on Artificial Intelligence, pages 364–369, 2005. [Bra04] Sebastian Brandt. Polynomial time reasoning in a description logic with existential restrictions, gci axioms, and - what else? In Proceedings of the 16th Eureopean Conference on Artificial Intelligence, ECAI’2004, pages 298– 302, 2004. [BT97] Dimitris Bertsimas and John N. Tsitsiklis. Introduction to linear optimization. Athena Scientific, 1997. [CP09] FG Cozman and RB Polastro. Complexity analysis and variational inference for interpretation-based probabilistic description logics. In Proceedings of the Twenty-Fifth Conference on Uncertainty in Artificial Intelligence (UAI), 2009. [Eck93] J. Eckhoff. Helly, Radon, and Caratheodory type theorems. In P. M. Gru- ber and J. M. Wills, editors, Handbook of Convex Geometry, pages 389–448. Elsevier Science Publishers, 1993. [FB11] Marcelo Finger and Glauber De Bona. Probabilistic satisfiability: Logic-based algorithms and phase transition. In To appear on IJCAI2011, 2011. [GKP88] G. Georgakopoulos, D. Kavvadias, and C. H. Papadimitriou. Probabilistic satisfiability. J. of Complexity, 4(1):1–11, 1988. [HJ00] P. Hansen and B. Jaumard. Probabilistic satisfiability. In Handbook of Defea- sible Reasoning and Uncertainty Management Systems, vol.5. Springer, 2000. [JFSS06] B. Jaumard, A. Fortin, I. Shahriar, and R Sultana. First order probabilistic logic. In NAFIPS 2006, pages 341–346, 2006. [KP90] D. Kavvadias and C. H. Papadimitriou. A linear programming approach to reasoning about probabilities. AMAI, 1:189–205, 1990. [LS10] Carsten Lutz and Lutz Schröder. Probabilistic description logics for subjec- tive uncertainty. In KR 2010, 12th International Conference of Knowledge Representation and Reasoning. AAAI Press, 2010. [Luk08] T Lukasiewicz. Expressive probabilistic description logics. Artificial Intelli- gence, 172(6-7):852–883, 2008. [GM10] O. Gries, and R. Möller. Gibbs sampling in probabilistic description logics with deterministic dependencies. First International Workshop on Uncer- tainty in Description Logics (Uni-DL), 2010. [CL06] P. C. G. Costa and K. B. Laskey. PR-OWL: A framework for probabilistic ontologies. Conf. on Formal Ontology in Information Systems, 2006. [DFL08] C. D’Amato, N. Fanizzi, and T. Lukasiewicz. Tractable reasoning with Bayesian description logics. Int. Conf. on Scalable Uncertainty Management (LNAI 5291), pages 146–159, 2008. [DPP06] Z. Ding, Y. Peng, and R. Pan. BayesOWL: Uncertainty modeling in semantic web ontologies. Soft Computing in Ontologies and Semantic Web, pages 3–29. Springer, Berlin/Heidelberg, 2006. [DS05] M. Dürig and T. Studer. Probabilistic ABox reasoning: preliminary results. Description Logics,pages104–111,2005. [GT07] L. Getoor and B. Taskar. Introduction to Statistical Relational Learning. MIT Press, 2007. [Hal03] J. Y. Halpern. Reasoning about Uncertainty. MIT Press, Cambridge, Mas- sachusetts, 2003. [Hei94] J. Heinsohn. Probabilistic description logics. Conf. Uncertainty in AI, page 311-318, 1994. [Jae94] M. Jaeger. Probabilistic reasoning in terminological logics. Principles of Knowledge Representation, pages 461–472, 1994. [KLP97] D. Koller, A. Y. Levy, and A. Pfeffer. P-CLASSIC: A tractable probablistic description logic. AAAI Conf. on AI, pages 390–397, 1997. [LS08] T. Lukasiewicz and U. Straccia. Managing uncertainty and vagueness in de- scription logics for the semantic web. Journal of Web Semantics, 6(4):291– 308, November 2008. [Seb94] F. Sebastiani. A probabilistic terminological logic for modelling information retrieval. 17th Conf. on Research and Development in Information Retrieval, pages 122–130, Dublin, Ireland, 1994. Springer-Verlag.