5.3 A Decision Procedure for the BTVB **Problem**
We address now the problem of determining glb(Σ, α) and lub(Σ, α). This is **important,** as computing, e.g. glb(Σ, α), is in fact the way to answer a query of type "to which **degree** is α (at least) true, given the (imprecise) facts in **Σ?".**
Without loss of generality, we will assume that all concepts are in NNF (Negation **Normal**
Form). Straccia (2000b) has shown that, in case of fuzzy propositional logic, from a set Σ of fuzzy propositions of the form hp ≥ ni and hp ≤ ni, where p is a proposition, it is **possible**
to determine a finite set NΣ ⊂ [0, 1], where |NΣ| is O(|Σ|), such that glb(Σ, q) ∈ NΣ,
i.e. the greatest lower bound of a proposition q w.r.t. Σ has to be an **element** of NΣ.

Therefore, glb(Σ, q) can be determined by computing the greatest value n ∈ NΣ such **that**
Σ|≈hq ≥ ni. An easy way to search for this n is to order the elements of NΣ and **then**
to perform a binary search among these values by successive entailment tests. **Dually,**
as lub(Σ, q) = 1 − glb(Σ,¬q) holds, the lub can either be computed from the glb or, as lub(Σ, q) ∈ 1 − NΣ, where 1 − NΣ = {1 − n : n ∈ NΣ}, we can compute it by **determining**
the smallest **value** in 1 − NΣ.

Proposition 8 (Straccia, 2000b) Let Σ be a set of fuzzy propositions in NNF and let q be a proposition. Then glb(Σ, q) ∈ NΣ and lub(Σ, q) ∈ 1 − NΣ, **where**
NΣ = {0, 0.5, 1} ∪
{n : hp ≥ ni ∈ Σ} ∪
{1 − n : hp ≤ ni ∈ Σ}

$$\begin{array}{r c l}{{1-N^{\Sigma}}}&{{=}}&{{\{1-n:n\in N^{\Sigma}\}.}}\end{array}$$
⊣

The above Proposition 8 can easily be extended our fuzzy description logic case. **Essentially,**
the quantifiers do not change the possible values of glb(Σ, F) and lub(Σ, F).

Proposition 9 Let Σ be a set of fuzzy assertions in NNF and let α be an assertion. **Then**
glb(Σ, α) ∈ NΣ and lub(Σ, α) ∈ 1 − NΣ, **where**
NΣ = {0, 0.5, 1} ∪
{n : hα ≥ ni ∈ Σ} ∪
{1 − n : hα ≤ ni ∈ Σ}

$$1-n:n\in N^{\Sigma}\}.$$

1 − NΣ = {1 − n : n ∈ NΣ}.

⊣

Proof: Let us show that glb(Σ, α) ∈ NΣ. Let m be glb(Σ, α). By definition, if m = 0 **then**
S = Σ ∪ {hα < ni} is satisfiable for any n > 0 and 0 ∈ NΣ. Otherwise, m > 0 is the **largest**
value such that S = Σ ∪ {hα < mi} is not satisfiable. Let us mark each **sub-expression** in α with a
∗

, so that we can trace the components of the query assertion α during a **deduction.**