Our method is an alternative to existing combinations of DL with probabilities that impose deterministic restrictions on probabilities. For example, [LS10] assigns probabilities to concepts over a fixed interpretation, forcing the probability 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.

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 others 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 p ub that leave the knowledge base satisfiable; this problem is also outside the scope of this work.

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.

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 N C , N R , and N I of concept names, role names, and individual names, respectively. The set of EL-concepts is given by the following syntax rules:

where A ranges over N C , C and D over EL-concepts and r over N R . 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

where C and r are as before, a, b ∈ N I and A, A ′ range over ABoxes.

The standard EL semantics is used for TBoxes and ABoxes, based on interpretations I = (∆ I , • I ), where ∆ I is a non-empty set called domain and • I is an interpretation function that maps each each A ∈ N C to a subset A I ⊆ ∆ I , each r ∈ N R to a subset r I ⊆ ∆ I × ∆ I , and each a ∈ N I to an element a I ∈ ∆ I ; see [BBL05]. We extend the interpretation I for all concepts in the usual way. So , A) is satisfiable in EL can be solved in polynomial time [Bra04].

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

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

Then the pair T , PA 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 satisfiability 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 I T of all interpretations of a TBox T is uncountably infinite.

For that, define an equivalence relation

that is, I and I ′ satisfy the same ABoxes in PA in a context of TBox T . 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 T , PA . We will write I(A) = 1 for I |= A and I(A) = 0 for I |= A.

Let n be the number of atomic elements in PA, |PA| = k. Consider I 1 , . . . ,

The probabilistic satisfiability problem for an ELPA-knowledge base K = T , PA is to decide if there is a probability vector π of dimension n ′ that obeys the ELPA-restrictions:

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, p 1 = 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 p ub = 0.3, where the probability of John having Lyme is at most 30%. We consider only the 3 ABox with probabilistic 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.

It is easy to verify that the interpretations I 1 -I 4 are all consistent with T 0 , A 0 , so all probability relations are verified by π, so probabilistic database for p ub = 0.3 is satisfiable. Some important questions remain: how to compute a probability distribution when one exists, and whether that probabilistic knowledge base remains satisfiable when p ub = 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:

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.

For the sake of providing a normal form, we add a few new convenient definitions. Let N 0 be a set of 0-ary atomic propositions. A propositional rule is an expression of the form q → A 1 or A 2 → q, where q ∈ N 0 and A 1 , A 2 ABoxes, with the obvious semantic that I |= q → A 1 iff I |= q or I |= A 1 ; and I |= A 2 → q iff I |= q or I |= A 2 . We extend the notion of ABox such that

such that q ∈ N 0 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 Isatisfiability of R ∪ A reduces to the I-satisfiability of the atomic positive formulas 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 propositional rules. For the rest of this paper, an extended ELPA-knowledge base is a 4-tuple K e = T , R, A, PA , in which the probabilistic assignment of ABoxes PA is evaluated in an (deterministic) evaluation context consisting of a triple C = T , R, A of TBox, propositional rules and deterministic ABox A; we also represent K e = C, PA . Clearly, an ELPA-knowledge base K is a special case of an extended ELPA-knowledge base K e the previous view in which R = ∅ and A is part of PA. Now we define the normal form. A knowledge base

In this case, PA is an atomic probability assignment evaluated in context C = T , R, A . 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 K e there exists an atomic normal form knowledge base K e nf that is satisfiable iff K e 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 T 0 and deterministic ABox A 0 remain the same. We introduce atoms q 1 , q 2 , q 3 for ABoxes A 1 , A 2 , A 3 respectively, which generates the following set or rules R 0 : q1 → ∃hasCause.Lyme(s1), q2 → ∃hasCause.Lyme(s2), ∃suspectOf.Lyme(john) → q3 C 0 = T 0 , R 0 , A 0 is the evaluation context; the atomic probability assignment is PA 0 = { P (q 1 ) = 0.1, P (q 2 ) = 0.2. P (q 3 ) = p ub }.

The normal form knowledge base is K e 0 = C 0 , PA 0 . Note that the probability distribution of Example 2.2 does not satisfy K e 0 when p ub = 0.3, but by Theorem 2.5 there must exist other interpretations involving q 1 , q 2 , q 3 and rules R 0 and another probability distribution π that satisfies K e 0 . The following result allows us to see a satisfiable normal form knowledge base K e nf as an interaction between a solution to assignments PA constrained by the EL-decisions of context T , R, A . An interpretation I is T , R, A -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 ELPAsatisfiability solving algorithm that we present in the next section.

Lemma 2.7 A normal form knowledge base K e = T , R, A, PA is satisfiable iff there is a binary (k + 1) × (k + 1)-matrix A K e , such that all of its {0, 1}columns represent interpretations that are T , R, A -consistent and A K e • π = p has a solution π ≥ 0.

We present a logic-algebraic algorithm to verify the satisfiability of a normal form knowledge base K e = T , R, A, PA 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, A j is its j-th column and A i 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.

We always assume that the lines of A are ordered such that the input probabilities p 1 , . . . , p k in (2) are in decreasing order. By Lemma 2.7, C, PA has a solution iff there is a partial solution A satisfying (2) such that if π j > 0 then a 1,j , . . . , a k,j represent C-consistent interpretations for 1 ≤ i ≤ k, 1 ≤ j ≤ k + 1. We usually abuse terminology calling A j a C-consistent column. This method is based on PSAT-solving method of [FB11], which is an improvement on the methods of [KP90,HJ00]; it consists of an algebraic optimisation problem in the form of a special linear program of the form

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 receives a matrix A (s) and employs a column generation method that solves an auxiliary problem; the latter is a logic-based satisfiability problem that employs EL-decision procedure, generates a column that replaces some column in A (s) , obtains A (s+1) and decreases the objective function |J|, f , where

In the iterative method, some columns are not C-consistent and the process is done such that the number of C-consistent columns A j 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 ∅, PA . As the elements of p are in decreasing order, consider the {0, 1}-matrix I * = [a i,j ] 1≤i,j≤k+1 where a i,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 ∅, PA and is called a relaxed solution for C, PA . 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 p ub = 0.3 (left) and p ub = 0.05 (right). An initial feasible solution for it is A (0) •π (0) = p, with atoms ordered in decreasing probability, namely

On the left, all columns are C-consistent, so the problem is satisfiable with solution 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

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.

In a feasible solution A such that Aπ = p and π ≥ 0, some columns may not be C-consistent. Let J = {j|A j 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 The second component of the 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 |J|, f 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 C, PA associated to program (3) is satisfiable iff the objective function is minimal at 0, 0 .

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 C, PA (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 0, 0 .

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 A j associated to π j > 0, a new C-consistent column b = [1 y 1 . . . y k ] ′ to substitute A j must satisfy the set of linear inequalities:

Such a column is here obtained by a combination of a SAT solver, which guarantees 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 second 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 0, 0 Therefore the corresponding ELPA-knowledge base is unsatisfiable.

Theorem 3.3 Algorithm 3.1 with column generation as above is correct and always terminates.