FREE ELECTRONIC LIBRARY - Dissertations, online materials

Pages:   || 2 |

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

-- [ Page 1 ] --

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



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 unification algorithm handling existentiality without the need of skolemization in first-order logic. Its idea follows from general resolution with existentiality for first- 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- fication, 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 unification for first-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 first-order logic (FOL) [Ba97], [Mu82]. The system may handle formulas without any trans- formation algorithms. It requires only more complex unification algorithm based on polarity criteria and quantifier 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 first-order logic

2.1 General resolution - brief overview For the purposes of (RRT PDL ) we will use generalized principle of resolution, which is defined 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 first-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 first 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 refine the general resolution rule into first-order logic and description logic, it is important to devise sound unification algorithm. Standard unification algorithms require variables to be treated only as universally quantified ones. We will present more general unification algorithm, which simulates skolemization without the need of real performation of it. It should be stated that the following unification 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 first-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 (∧, ∨, →, ¬), quantifiers (∃, ∀) and logical constants (⊥, ).

Definition 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 defined 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 reflexive and transitive closures Sub∗ and Sup∗ are

defined 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 quantifiers 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 - unification 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 quantification subformula has negative polarity).

Sound unification requires further definitions on variable quantification.

Definition 2. Variable assignment, substitution and significance 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(quantifier assignment), Sbt (variable substitution) and Sig(significance) are defined 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 iff variable is significant, Sig(α) = 0 iff variable is not significant w.r.t. existential substitution.

Note that with Qnt mapping (assignment of first name matching quantifier 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 quantifier and there is no need to rewrite all occurrences of a variable when working with this mapping within unification. It is also clear that if Qnt(α) = ∅ then α is a free variable. These variables could be simply avoided by introducing new universal quantifiers to F. Significance mapping is important for differentiating 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 quantification 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 unification algorithm, we should formulate variable unification 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.

Definition 3. Global quantification and variable unification restriction Let F be a formula without free variables and α be a variable occurring in a term of F.

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

2. α is globally existential variable iff (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 Unification

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 define the most general unification algorithm based on recursive conditions (extended unification in contrast to standard MGU [Lt93]).

Definition 4. Most general unifier 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 unifier (MGU)(substitution mapping) σ is obtained by following atom and term unification steps or the algorithm returns fail-state for unification.

Atom unification

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

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

3. In any other case unifier doesn’t exist (fail-state).

Term unification (t, u )

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

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

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

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

5. In any other case unifier doesn’t exist (fail-state).

With above defined notions it is simple to state the general resolution rule for FOL (without the equivalence connective). It extends the definition 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 unification 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 specific 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 unifier. 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 unifier 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 definitions by introduction of refutational theorem proving with the rule GRF OL. We assume standard notions and theorems stated in [Ba01].

Definition 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 simplification 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 simplification 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 quantifier for a variable not occurring in the formula.

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

Pages:   || 2 |

Similar works:

«WP/04/53 Sovereign Debt Defaults and Financing Needs Mark Kruger and Miguel Messmacher © 2004 International Monetary Fund WP/04/53 IMF Working Paper IMF Executive Director for Antigua and Barbuda, The Bahamas, Barbados, Belize, Canada, Dominica, Grenada, Ireland, Jamaica, St. Kitts and Nevis, St. Lucia, and St. Vincent and the Grenadines, and IMF Institute Sovereign Debt Defaults and Financing Needs Prepared by Mark Kruger and Miguel Messmacher1 Authorized for distribution by Ian E. Bennett...»

«Proceedings on applied botany, genetics and breeding, volume 176, issue 2 M. A. Vishnyakova. Do not let laurels carry you away, they are cheap stuff. (Vavilov’s role in the formation of G. D. Karpechenko as a leader of genetic research at VIR). Proceedings on applied botany, genetics and breeding. Vol. 176. I. 2. 2015. рр. 131–145. Background: The article is devoted to the 90th anniversary of genetic investigations in the Vavilov Institute. In April 1925, a young scientist G. D....»

«Statically Safe Program Generation with SafeGen Shan Shan Huang, David Zook, and Yannis Smaragdakis College of Computing, Georgia Institute of Technology Atlanta, GA 30332, USA {ssh|dzook|yannis}@cc.gatech.edu Abstract. SafeGen is a meta-programming language for writing statically safe generators of Java programs. If a program generator written in SafeGen passes the checks of the SafeGen compiler, then the generator will only generate well-formed Java programs, for any generator input. In other...»

«INDEPENDENT, NEVER MARRIED PEOPLE IN THEIR THIRTIES: REMAINING SINGLE ÁGNES UTASI INDIVIDUALISATION AND THE SPREAD OF SINGLE LIFESTYLE In the majority of countries with a high level of development, demographic statistical data show that the age at which people make their first marry is becoming increasingly delayed. One of the likely determining reasons for this is that societies living in relative prosperity are going through an increasing degree of individualisation, the period of education...»

«THE COMPLETE CRITICAL GUIDE TO ALEXANDER POPE Was Alexander Pope the poet of reason, or a daring anti-establishment prophet What can a study of Pope tell us about the eighteenth century How did this outsider, subject to debilitating illness, become the leading poet of his generation So many questions surround the key figures in the English literary canon, but most books focus on one aspect of an author’s life or work, or limit themselves to a single critical approach. The Complete Critical...»

«6º CONGRESSO BRASILEIRO DE ENGENHARIA DE FABRICAÇÃO th 6 BRAZILIAN CONFERENCE ON MANUFACTURING ENGINEERING 11 a 15 de abril de 2011 – Caxias do Sul – RS Brasil th th April 11 to 15, 2011 – Caxias do Sul – RS – Brazil ADDITIVE MANUFACTURING TO BUILD POLYCAPROLACTONE SCAFFOLDS Ana Lívia Chemeli Senedese, ana-livia.senedese@cti.gov.br1,2,3 Arnaldo Luis Lixandrão Filho, arnaldo.filho@cti.gov.br1 Jorge Vicente Lopes da Silva, jorge.silva@cti.gov.br1,3 Paulo Inforçatti Neto,...»

«Regulatory role of proheparanase with peri-synaptic heparan Title sulfate proteoglycan and AMPA-type glutamate receptor in synaptic plasticity Author(s) Lam, YL; Cham, WC; Ma, CW; Chan, YS; Shum, DKY The Hong Kong-Taiwan Physiology Symposium 2012 and the Joint Scientific Meeting of Hong Kong Society of Neurosciences Citation and the Biophysical Society of Hong Kong, Hong Kong, 14-15 June 2012. In Abstracts Book of the Joint Scientific Meeting, 2012, p. 73-74, Abstract no. P59 Issued Date 2012...»

«(Page 1 of 5) Technician Training Tutorial: Dispensing Oral Blood Thinners Warfarin (Coumadin, Jantoven-U.S., others) is an oral “anticoagulant” blood thinner used to help prevent blood clots that can lead to problems such as heart attacks and strokes. Its name originates from the Wisconsin Alumni Research Foundation (WARF), which funded its development many years ago. Warfarin was actually used in the past as a rat poison and is structurally similar to many pesticides used today. Warfarin...»

«Journal of Religious Culture Journal für Religionskultur Ed. by / Hrsg. Von Edmund Weber Institute for Irenics / Institut für Wissenschaftliche Irenik Johann Wolfgang Goethe-Universität Frankfurt am Main ISSN 1434-5935© E.Weber – E.Weber@em.uni-frankfurt.de No. 27-11 (1999) The Life of Jetsun Lochen Rinpoche (1865-1951) By Hanna Havnevik, Oslo Jetsun Lochen Rinpoche was presumably born in 1865 and died in 1951 and was one of the most famous female religious masters in traditional Tibet....»

«The Official Newsletter DEPARTMENT OF Campus Foals Are Future Thoroughbreds DEPARTMENT OF 2013 Cover Story Campus Foals find new homes at Thoroughbred Auction Dr. Amy Burk announced that Amazin Terp (aka Tessie) and Diamondback Fire (aka Rebel), the weanlings foaled on campus last spring as part of the department’s new equine breeding program, have new owners. They joined 133 other Thoroughbreds at the Fasig-Tipton Midlantic December Mixed Sale on Monday, December 9, 2013 in Timonium, MD....»

«A TesTAmenT AgAinsT The World: The lord’s rebuke By YAHUSHUA-YAHUWAH Through His servant, Timothy Modern Scripture Spoken to This Generation 1 This book may be distributed With the following guidelines: NO word(s) may be changed, added to or omitted from this publication and/or Letters from God and His Christ™. This publication and Letters from God and His Christ™ are NOT to be resold for profit, under any circumstance. A TESTAMENT AGAINST THE WORLD: THE LORD’S REBUKE By...»

«F o u n dat ion s of E va n g e l ic a l T h e olo g y Sojourners and Strangers The Doctrine of the Church 8 Gregg R. Allison John S. Feinberg, general Editor “I believe that the doctrine of the church will be the most urgent locus of theological reflection over the next generation. In Sojourners and Strangers, Gregg Allison clears the ground by presenting a thoroughly biblical ecclesiology, at once comprehensive in scope and sensitive to nuance. A welcome addition to an important series.”...»

<<  HOME   |    CONTACTS
2016 www.dissertation.xlibx.info - Dissertations, online materials

Materials of this site are available for review, all rights belong to their respective owners.
If you do not agree with the fact that your material is placed on this site, please, email us, we will within 1-2 business days delete him.