REASONING
Motivation
Technical Solution
Introduction to Theorem Proving and Resolution
Description Logics
Logic Programming
Summary
References
MOTIVATION
Computers can do reasoning
Theorem Proving and Resolution, Description Logics, and Logic Programming
Introduction to Theorem Proving and Resolution


P _{ 1 } … P _{ n }
____________
C

where C is a conclusion sequent, and P _{ i } ‘s are premises sequents .
Resolution is a refutation system .
To prove a statement we attempt to refute its negation
Basic idea: Given a consistent set of axioms KB and goal sentence Q , we want to show that KB ⊧ Q
This means that every interpretation I that satisfies KB also satisfies Q
Any interpretation I only satisfies either Q or ¬ Q, but not both
Therefore, if in fact KB ⊧ Q holds , an interpretation that satisfies KB , satisfies Q and does not satisfy ¬ Q
The resolution rule is a single inference that produces a new clause implied by two clauses (called the parent clauses) containing complementary literals
The resulting clause contains all the literals that do not have complements. Formally:
When the two initial clauses contain more than one pair of complementary literals, the resolution rule can be applied (independently) for each such pair
However, only the pair of literals that are resolved upon can be removed: All other pairs of literals remain in the resolvent clause
Modus ponens (see last lecture) can be seen as a special case of resolution of a oneliteral clause and a twoliteral clause
Example: Given clauses
P(x, f(a)) v P(x, f(y)) v Q(y) and ¬P(z, f(a)) v ¬ Q(z)
P(x, f(a)) and ¬P(z, f(a)) unify with substitution σ = {x/z}
Therefore, we derive the resolvent clause (to which σ is applied):
P(z, f(y)) v Q(y) v ¬ Q(z)
Convert all the propositions of a knowledge base KB to clause normal form (CNF)
Negate Q (the to be proven statement) and convert the result to clause form. Add it to the set of clauses obtained in step 1.
Repeat until either a contradiction is found, no progress can be made, or a predetermined amount of effort has been expended:
a) Select two clauses. Call these the parent clauses.
b) Resolve them together using the resolution rule . The resolvent will be the disjunction of all the literals of both parent clauses with appropriate substitutions.
c) If the resolvent is the empty clause , then a contradiction has been found. If it is not, then add it to the set of clauses available to the procedure.
procedure resolutionrefutation(KB, Q)
;; KB a set of consistent, true sentences
;; Q is a goal sentence that we want to derive
;; return success if KB ⊢ Q, and failure otherwise
KB = union(KB, ¬Q)
while false not in KB do
pick 2 sentences, S1 and S2, in KB that contain
literals that unify
if none return "failure“
resolvent = resolutionrule(S1, S2)
KB = union(KB, resolvnt)
return "success"
Step 3: Standardize by renaming all variables so that variables bound by different quantifiers have unique names
( ∀ X) a(X) ∨ ( ∀ X) b(X) = ( ∀ X) a(X) ∨ ( ∀ Y) b(Y)
Step 4: Move all quantifiers to the left to obtain a prenex normal form
A formula is inn prenex normal form if it is written as a string of quantifiers followed by a quantifierfree part
Step 5: Eliminate existential quantifiers by using skolemization


Predicate form

Clause form


1.
∀
(x) (dog(X)
→
animal(X))

¬
dog(X)
∨
animal(X)


2. dog(fido)

dog(fido)


3.
∀
(Y) (animal(Y)
→
die(Y))

¬
animal(Y)
∨
die(Y)

Also, the resolution cannot be used to prove that a given sentence is not entailed by a set of axioms
A search method is required
Worst case: Resolution is exponential in the number of clauses to resolve
Order of clause combination is important
N clauses → N^{2} ways of combinations or checking to see whether they can be combined
Search heuristics are very important in resolution proof procedures
Strategies
BreadthFirst Strategy
Set of Support Strategy
Unit Preference Strategy
Linear Input Form Strategy
Q is entailed by KB (a set of premises or assumptions) if and only if there is no logically possible world in which Q is false while all the premises in KB are true
Does a proof simply take too long or will the computation never halt anyway?
Due to its complexity and remaining limitations FOL is often not suitable for practical applications
Logic Programming
DESCRIPTION LOGICS
Concepts/classes (unary predicates/formulae with one free variable)
E.g. Person, Female
Roles (binary predicates/formulae with two free variables)
E.g. hasChild
Individuals (constants)
E.g. Mary, John
Constructors allow to form more complex concepts/roles
Union ⊔: Man ⊔ Woman
Intersection ⊓ : Doctor ⊓ Mother
Existential restriction ∃: ∃hasChild.Doctor (some child is a doctor)
Value(universal) restriction ∀: ∀hasChild.Doctor (all children are doctors)
Complement /negation¬: Man ⊑ ¬Mother
Number restriction ≥n, ≤n
Axioms
Subsumption ⊑ : Mother ⊑ Parent
Classes/concepts are actually a set of individuals
We can distinguish different types of concepts:
Atomic concepts: Cannot be further decomposed (i.e. Person)
Incomplete concepts (defined by ⊑)
Complete concepts (defined by ≡)
Example incomplete concept defintion:
Man ⊑ Person ⊓ Male
Intended meaning: If an individual is a man, we can conclude that it is a person and male.
Man(x) ⇒ Person(x) ∧ Male(x)
Example complete concept definition:
Man ≡ Person ⊓ Male
Intended meaning: Every individual which is a male person is a man, and every man is a male person.
Man(x) ⇔ Person(x) ∧ Male(x)
I.e. directedBy(Pool Sharks, Edwin Middleton), hasChild(Jonny, Sue)
Roles have a domain and a range
Given the above definitions we can conclude that Pool Sharks is a move and that Edwin Middleton is (was) a person.
A special case of (unqualified) number restriction ≤1 R
Transitivity can be captured in DLs by role hierarchies and transitive roles:
hasChild ≡ hasParent
Bear(Winni Puh)
From a theoretical point of view this division is arbitrary but it is a useful simplification
Restricted use of quantifiers: ∃, ∀
Provides (implicitly or explicitly) conjunction, union and negation of class descriptions
Person ⊓ ∀hasChild.(Doctor ⊔ ∃hasChild.Doctor)
Mary is a Woman.
E.g. Marry loves Peter.
E.g.: A Dog is an animal. A man is a male Person.
Semantics follow standard FOL model theory
Description Logics are a fragment of FOL
The vocabulary is the set of names (concepts and roles) used
I.e. Mother, Father, Person, knows, isRelatedTo, hasChild, …
An interpretation I is a tuple (∆^{I}, ⋅^{I})
∆^{I} is the domain (a set)
⋅^{I} is a mapping that maps:
Names of objects (individuals) to elements of the domain
Names of unary predicates (classes/concepts) to subsets of the domain
Names of binary predicates (properties/roles) to subsets of ∆^{I} x ∆^{I}
The semantics of DL are based on standard First Order Model theory
A translation is usually very straightforward, according to the following correspondences (for ALC):
A description is translated to a firstorder formula with one free variable
An individual assertion is translated to a ground atomic formula
An axiom is translated to an implication, closed under universal implication
More complex DLs can be handled in a similar way
Main reasoning tasks for DL systems:
Satisfiability : Check if the assertions in a KB have a model
Instance checking : Check if an instance belongs to a certain concept
Concept satisfiability : Check if the definition of a concept can be satisfied
Subsumption : Check if a concept A subsumes a concept B (if every individual of a concept B is also of concept A)
Equivalence : A ≡ B ⇔ B ⊑ A and A ⊑ B
Retrieval : Retrieve a set of instances that belong to a certain concept
Reasoning Task are typically reduced to KB satisfiability sat(A) w.r.t. to a knowledge base A
Instance checking : instance(a,C, A) ⇔¬sat(A ⋃ {a: ¬ C})
Concept satisfiability : csat(C) ⇔ sat(A ⋃ {a: ¬ C})
Concept subsumption : B ⊑ A ⇔ A ⋃ {¬B ⊓ C} is not satisfiable ⇔ ¬sat(A ⋃ {¬B ⊓ C})
Retrieval : Instance checking for each instance in the Abox
Note: Reduction of reasoning tasks to one another in polynomial time only in propositionally closed logics
DL reasoners typically employ tableaux algorithms to check satisfiability of a knowledge base
Pellet supports expected standard DL reasoning tasks
Consistency, classification, realization
Conjunctive query answering
Concept satisfiability
Additionally Pellet supports:
SPARQLDL queries
Datatype reasoning
Userdefined datatypes
Nary datatype predicates
Rules support (DLsafe SWRL rules)
Explanation and debugging features
Axiom pinpointing service
Explanation & Debugging support
Motivation: It is hard to understand large and/or complex ontologies
Examples:
Why is a specific subclass relation inferred?
Why is an ontology inconsistent?
Pellet provides axiom pinpointing service:
For any inference, returns the (minimal set of) source axioms that cause the inference
Applications can track additional provenance information
Axiom pinpointing is the first step to explanations
Precise justifications (pinpoint parts of axioms) are ongoing work in Pellet‘s developement
LOGIC PROGRAMMING
Logic Programming is based on a subset of First Order Logic called Horn Logic
Horn Logic can serve as a simple KR formalism and allows to express
IF <condition> THEN <result> rules
Under certain restrictions reasoning over knowledge bases based on such rules is decideable (in contrast to general ATP within First Order Logic)
A Herbrand Interpretation I is a subset of the Herbrand Base B for a program
The domain of a Herbrand interpretation is the Herbrand Universe U
Constants are assigned to themselves
Every function symbol is interpreted as the function that applies it
If f is an nary function symbol (n>0) then the mapping from U^{n} to U defined by (t_{1}, …, t_{n}) → f(t_{1}, …, t_{n}) is assigned to f
Logic Programs can also contain recursion
ancestor(x,z) : ancestor(x,y), ancestor(y,z).
This is a problem as soon as negation is allowed since the minimal model is not uniquely defined anymore
If the dependency graph contains a cycle then the program is recursive
Example: What is the meaning of win(x) : not win(x) ?
→ This guarantees a unique interpretation of a Logic Program using negation
Is turing complete
Prolog programs are not guaranteed to terminate
Datalog is such a subset
Originally a rule and query language for deductive databases
Extensional Database (EDB) consists of facts
Intentional Database(IDB) consists of nonground rules
Restrictions:
Datalog disallows function symbols
Imposes stratification restrictions on the use of recursion + negation
Allows only range restricted variables ( safe variables )
This limits evaluation of variables to finitely many possible bindings
Nonground query, i.e. ? loves(Mary, x)
Replace x by every possible value
A ⊧ loves(Mary, Joe)
Homepage: http://www.irisreasoner.org/
Various builtin predicates (Equality, inequality, assignment, unification, comparison, type checking, arithmetic, regular expressions,... )
Topdown evaluation by SLDNF resolution (backwardchaining)




IRIS performing computations using seminaiv evaluation in combination with stratification and complex datatypes
SUMMARY
Resolution is a sound and complete inference procedure for FirstOrder Logic
Due to its complexity and remaining limitations FOL is often not suitable for practical applications
Often formalisms expressivity and complexity results are more appropriate:
Description Logics
Logic Programming
Individuals
Many different Description Logics exist, depending on choice of constructs
Usually reasoning tasks in DLs can all be reduced to satisfiablity checking
The semantics of a Logic Program are however based on its minimal Herbrand Model
Negationasfailure introduced nonmonotonic behavior and pushes LP beyond the expressivity of First Order Logic
A typical inference task for LP engines is conjunctive query answering
REFERENCES
Questions?