# «Abstract. The article presents refutational resolution theorem proving system for De- scription Logic (DL) based on general (non-clausal) resolution ...»

Non-clausal Resolution Theorem Proving

for Description Logic

Hashim Habiballa

Institute for Research and Applications of Fuzzy Modeling

and Department of Computer Science

University of Ostrava

30. dubna 22

Ostrava, Czech Republic

Hashim.Habiballa@osu.cz

http://www.volny.cz/habiballa/index.htm

Abstract. The article presents refutational resolution theorem proving system for De-

scription Logic (DL) based on general (non-clausal) resolution rule. There is also pre-

sented uniﬁcation algorithm handling existentiality without the need of skolemization in ﬁrst-order logic. Its idea follows from general resolution with existentiality for ﬁrst- order logic. When the prover is constructed it provides the deductive system, where existing resolution strategies and its implementations may be used.

keywords: Automated theorem proving, non-clausal resolution, general resolution, uni- ﬁcation, description logic.

1 Introduction Description logic covers several deductive systems like well studied tableaux al- gorithm [Lu05] or clausal form resolution [Hu00]. Tableaux algorithm doesn’t require any transformations (it may use some rewrite rules), but from the im- plementation point of view this procedure is slightly ”non-deterministic”, when one performs usage of γ and δ rules. On the other hand there is more practical deductive system based on resolution principle with uniﬁcation for ﬁrst-order logic, which allows to use variety of strategies, techniques and also implementa- tions. Conversion to clausal form destroys the original meaning of a formula and requires removal of existentiality, which is also present in DL. We will present refutational resolution theorem proving system for enriched ALC-like DL (RRT PDL ) based on general (non-clausal) resolution principle in ﬁrst-order logic (FOL) [Ba97], [Mu82]. The system may handle formulas without any trans- formation algorithms. It requires only more complex uniﬁcation algorithm based on polarity criteria and quantiﬁer mapping. The below presented idea have its origin in implementation of non-clausal resolution theorem prover [Ha05].

This work was supported by research grant of Czech Ministry of Education - MSM 6198898701 2 Background from ﬁrst-order logic

2.1 General resolution - brief overview For the purposes of (RRT PDL ) we will use generalized principle of resolution, which is deﬁned in the Handbook [Ba01] concerning basics of the theory (or [Ba97]).

General resolution F [G] F [G] (1) F [G/⊥] ∨F [G/ ] where F and F’ are formulas - premises of ﬁrst-order logic and G represents an occurrence of a subformula (we may consider atoms only) of F and F’. The expression below the line means the resolvent of premises on G. Every occurrence of G is replaced by false in the ﬁrst formula and by true in the second one.

It is also called F the positive, F’ the negative premise, and G the resolved subformula.

Example 1. General resolution with equivalence

1. a ∧ c ↔ b ∧ d (axiom)

2. a ∧ c (axiom)

3.¬[b ∧ d] (axiom) - negated goal 4. [a ∧ ⊥] ∨ [a ∧ ] (resolvent from (2), (2) on c) ⇒ a 5. [a ∧ ⊥] ∨ [a ∧ ↔ b ∧ d] ((2), (1) on c) ⇒ a ↔ b ∧ d 6. ⊥ ∨ [ ↔ b ∧ d] ((4), (5) on a) ⇒ b ∧ d 7. ⊥ ∧ d ∨ ∧ d ((6), (6) on b) ⇒ d

8. b ∧ ⊥ ∨ b ∧ ((6), (6) on d) ⇒ b 9. ⊥ ∨ ¬[ ∧ d] ((8), (3) on b) ⇒ ¬d 10. ⊥ ∨ ¬ ((7), (9) on d) ⇒ ⊥ (refutation) When trying to reﬁne the general resolution rule into ﬁrst-order logic and description logic, it is important to devise sound uniﬁcation algorithm. Standard uniﬁcation algorithms require variables to be treated only as universally quantiﬁed ones. We will present more general uniﬁcation algorithm, which simulates skolemization without the need of real performation of it. It should be stated that the following uniﬁcation process doesn’t allow an occurrence of the equivalence connective. It is needed to remove equivalence by the following rewrite rule: A ↔ B ⇒ [A → B] ∧ [B → A].

We assume that the language and semantics of ﬁrst-order logic (FOL) is standard. We use terms - individuals (a, b, c,...), functions (with n arguments) (f, g, h,...), variables (X, Y, Z,...), predicates(with n arguments) (p, q, r,...), logical connectives (∧, ∨, →, ¬), quantiﬁers (∃, ∀) and logical constants (⊥, ).

Deﬁnition 1.

**Structural notions of a FOL formula Let F be a formula of FOL then the structural mappings Sub (subformula), Sup (superformula), Pol (polarity) and Lev (level) are deﬁned as follows:**

F = G ∧ H or F = G ∨ H ⇒ Sub(F ) = {G, H}, Sup(G) = F, Sup(H) = F P ol(G) = P ol(F ), P ol(H) = P ol(F ) F =G→H ⇒ Sub(F ) = {G, H}, Sup(G) = F, Sup(H) = F P ol(G) = −P ol(F ), P ol(H) = P ol(F ) F = ¬G ⇒ Sub(F ) = {G}, Sup(G) = F P ol(G) = −P ol(F ) F = ∃αG or F = ∃αG ⇒ Sub(F ) = {G}, Sup(G) = F (α is a variable) P ol(G) = P ol(F ) Sup(F ) = ∅ ⇒ Lev(F ) = 0, P ol(F ) = 1 F is a formula Sup(F ) = ∅ ⇒ Lev(F ) = Lev(Sup(F )) + 1 For mappings Sub and Sup reﬂexive and transitive closures Sub∗ and Sup∗ are

**deﬁned recursively as follows:**

1. Sub∗ (F ) ⊇ {F }, Sup∗ (F ) ⊇ {F }

2. Sub∗ (F ) ⊇ {H|G ∈ Sub∗ (F ) ∧ H ∈ Sub(G)}, Sup∗ (F ) ⊇ {H|G ∈ Sup∗ (F ) ∧ H ∈ Sup(G)} These structural mappings provide framework for assignment of quantiﬁers to variable occurrences. Subformula and superformula mappings and its closures encapsulate essential hierarchical information of a formula structure. Level gives the ordering with respect to the scope of variables (which is essential for skolemization simulation - uniﬁcation is restricted for existential varibles). Polarity enables to decide the global meaning of a variable (e.g. globally an existential variable is universal if its quantiﬁcation subformula has negative polarity).

Sound uniﬁcation requires further deﬁnitions on variable quantiﬁcation.

Deﬁnition 2. Variable assignment, substitution and signiﬁcance Let F be a formula of FOL, G = p(t1,..., tn ) ∈ Sub∗ (F ) atom in F and α a variable occurring in ti.

**Variable mappings Qnt(quantiﬁer assignment), Sbt (variable substitution) and Sig(signiﬁcance) are deﬁned as follows:**

Qnt(α) = {QαH|Q = ∃ ∨ Q = ∀, H, I ∈ Sub∗ (F ), QαH ∈ Sup∗ (G), ∀QαI ∈ Sup∗ (G) ⇒ Lev(QαI) Lev(QαH)}

**For substitution of term t into α in F (F [α/t ]) it holds:**

Sbt(Qnt(α)) = t Sig(α) = 1 iﬀ variable is signiﬁcant, Sig(α) = 0 iﬀ variable is not signiﬁcant w.r.t. existential substitution.

Note that with Qnt mapping (assignment of ﬁrst name matching quantiﬁer variable in a formula hierarchy from bottom) we are able to distinguish between variables of the same name and there is no need to rename any variable. Sbt mapping holds substituted terms in a quantiﬁer and there is no need to rewrite all occurrences of a variable when working with this mapping within uniﬁcation. It is also clear that if Qnt(α) = ∅ then α is a free variable. These variables could be simply avoided by introducing new universal quantiﬁers to F. Signiﬁcance mapping is important for diﬀerentiating between original formula universal variables and newly introduced ones during proof search (an existential variable can’t be bounded with it).

** Lemma 1. Free variables quantiﬁcation Let F be a formula of FOL and α be a free variable in F (Qnt(α) = ∅), then the formula F = ∀αF is equivalent to F.**

Before we can introduce standard uniﬁcation algorithm, we should formulate variable uniﬁcation restriction for existential and universal variable through the notion of globally universal and globally existential variable (it simulates conversion into prenex normal form).It is clear w.r.t. skolemization technique that an existential variable can be substituted into an universal one only if all globally universal variables over the scope of it have been already substituted by a term.

Skolem functors function in the same way.

Deﬁnition 3. Global quantiﬁcation and variable uniﬁcation restriction Let F be a formula without free variables and α be a variable occurring in a term of F.

1. α is globally universal variable iﬀ (Qnt(α) = ∀αH ∧ P ol(Qnt(α)) = 1) or (Qnt(α) = ∃αH ∧ P ol(Qnt(α)) = −1)

2. α is globally existential variable iﬀ (Qnt(α) = ∃αH ∧ P ol(Qnt(α)) = 1) or (Qnt(α) = ∀αH ∧ P ol(Qnt(α)) = −1) Let F1 be a formula and α be a variable occurring in F1, F2 be a formula, t be a term occurring in F2 and β be a variable occurring in F2. Variable Uniﬁcation

**Restriction (VUR) for (α,t) holds if one of the conditions 1. and 2. holds:**

1. α is a globally universal variable and t = β, where β is a globally existential variable and α not occurring in t (non-existential substitution)

2. α is a globally universal variable and t = β, where β is a globally existential variable and ∀F ∈ Sup∗ (Qnt(β)), F = QγG, Q ∈ {∀, ∃}, γ is a globally universal variable, Sig(γ) = 1 ⇒ Sbt(γ) = ∅ (existential substitution) Now we can deﬁne the most general uniﬁcation algorithm based on recursive conditions (extended uniﬁcation in contrast to standard MGU [Lt93]).

Deﬁnition 4. Most general uniﬁer algorithm Let F1, F2 be formulas of FOL, G = p(t1,..., tn ) be an atom occurring in F1 and G = r(u1,..., un ) be an atom occurring in F2. Most general uniﬁer (MGU)(substitution mapping) σ is obtained by following atom and term uniﬁcation steps or the algorithm returns fail-state for uniﬁcation.

Atom uniﬁcation

1. if n = 0 and p = r then σ = ∅ and the uniﬁer exists (success-state).

2. if n 0 and p = r then perform term uniﬁcation for every pair (t1, u1 ); if for every pair uniﬁer exists then M GU (G, G ) = σ (success state).

3. In any other case uniﬁer doesn’t exist (fail-state).

Term uniﬁcation (t, u )

1. if t = a, u = b are individual constants and a = b then for (t’,u’) uniﬁer exist (success-state).

2. if t = f (t1,..., tm ), u = g(u1,..., un ) are function symbols with arguments and f = g then uniﬁer for (t, u ) exists iﬀ uniﬁer exists for every pair (t1, u1 ),..., (tn, un ) (success-state).

3. if t = α is a variable and VUR for (t, u ) holds then uniﬁer exists for (t, u ) holds and (Sbt(α) = u ) ∈ σ (success-state).

4. if u = α is a variable and VUR for (u, t ) holds then uniﬁer exists for (t, u ) holds and (Sbt(α) = t ) ∈ σ (success-state).

5. In any other case uniﬁer doesn’t exist (fail-state).

With above deﬁned notions it is simple to state the general resolution rule for FOL (without the equivalence connective). It extends the deﬁnition from [Ba97].

Note that with Qnt mapping we are able to distinguish variables not only by its name (which may not be unique), but also with this mapping (it is unique).

Sig property enables to separate variables, which were not originally in the scope of an existential variable. When utilizing the rule it should be set the Sig mapping for every variable in axioms and negated goal to 1. We present a very simple example of existential variable uniﬁcation before we introduce the refutational theorem prover for FOL.

** Example 2. It doesn’t hold ∀X∃Y p(X, Y ) |= ∃Y ∀Xp(X, Y ) and it holds ∃Y ∀Xp(X, Y ) |= ∀X∃Y p(X, Y ).**

(General Y for all X can’t be deduced from Y speciﬁc for X but contrary it holds)

**Source formulas (axioms) :**

F0 : ∀X∃Y p(X, Y ). F1 (¬query) : ∀Y ∃X¬p(X, Y ).

R[F1&F1] : ⊥ ∨. R[F0&F0] : ⊥ ∨.

In this example F0 and F1 can’t resolve, since ∀X∃Y p(X, Y ) and ∀Y ∃X¬p(X, Y ) have no uniﬁer. It is impossible to substitute universal X from F0 with X from F1, because X from F1 is existential and its superior variable Y is not assigned with a value. Counter-example with variable Y is the same instance and it is not allowed to substitute anything into an existential variable. However, in the next example a uniﬁer exists.

**Source formulas (axioms) :**

F0 : ∃Y ∀Xp(X, Y ). F1 (¬query) : ∃X∀Y ¬p(X, Y ).

R[F1&F0] : YES. R[F0&F1] : YES.

In the second case the universal variable X from F0 could be assigned with existential Y because Y in F1 has no superior variable. Then existential Y from F0 can substitute the universal Y from F1 for the same reason.

Now we entail above presented deﬁnitions by introduction of refutational theorem proving with the rule GRF OL. We assume standard notions and theorems stated in [Ba01].

Deﬁnition 6. Refutational resolution theorem prover for FOL Refutational non-clausal resolution theorem prover for FOL (RRT PF OL ) is the inference system with the inference rule GRF OL and sound auxiliary simpliﬁcation rules for ⊥, (standard equivalencies for logical constants). A refutational proof of the goal G from the set of axioms N = {A1,..., Am } is a sequence of formulas F1, F2,..., Fn, ⊥, where Fi is an axiom from N, ¬G or a resolvent from premises Fk and Fl (k, l i), where simpliﬁcation rules may be applied to the resolvent. It is assumed that Sig(α) = 1 for ∀α in F ∈ N ∪ ¬G formula, every formula in a proof has no free variable and has no quantiﬁer for a variable not occurring in the formula.

** Theorem 1. RRT PF OL system is a sound inference system.**