Intelligent Systems
REASONING
Agenda

Motivation

Technical Solution

Introduction to Theorem Proving and Resolution

Description Logics

Logic Programming

Summary

References
MOTIVATION
Motivation
 Basic results of mathematical logic show:
 We can do logical reasoning with a limited set of simple (computable) rules in restricted formal languages like Firstorder Logic (FOL)

Computers can do reasoning
 FOL is interesting for this purpose because:
 It is expressive enough to capture many foundational theorems of mathematics
 Many realworld problems can be formalized in FOL
 It is the most expressive logic that one can adequately approach with automated theorem proving techniques
Motivation
 Due to its theoretical properties (decidability & complexity) FirstOrder Logic is not always an ideal solution
 This motivates research towards formalisms with more practically oriented computitional properties and expressivity
 Description Logics
 Syntactic fragments of FOL
 Focus on decidability and optimized algorithms key reasoning tasks (terminological reasoning / schema reasoning)
 Logic Programming
 Provides different expressivity than classical FOL (nonmonotonic reasoning with nonclassical negation)
 Provides a very intuitive way to model knowledge
 Efficient reasoning procedures for large datasets
TECHNICAL SOLUTIONS
Theorem Proving and Resolution, Description Logics, and Logic Programming
THEOREM PROVING
Introduction to Theorem Proving and Resolution
Introduction – Basic Notions
 A proof system is collection of inference rules of the form:


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

where C is a conclusion sequent, and P _{ i } ‘s are premises sequents .
 If an infererence rule does not have any premises that are taken to be true (called an axiom ), its conclusion automatically holds.

Example:
Modus Ponens: From P, P → Q infer Q,
Universal instantiation: From (∀x)p(x) infer p(A)
 Theorems:
 Expressions that can be derived from the axioms and the rules of inference.
Resolution  Principle

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

⇒
Hence KB
∪
{
¬
Q
}
is unsatisfiable, i.e., it is false under all interpretations
Resolution  Principle
 Resolution commonly requires sentences to be in clause normal form (also called conjunctive normal form or CNF)
 A clause is a disjunction of literals (implicitly universally quantified)
 E.g. : l_{1} ∨ … ∨ l_{n}
 A formula in clause normal form conjunction of a set of clauses
 E.g.: C_{1} ∧ … ∧ C_{n} = (l_{n} ∨ … ∨ l_{m}) ∧ … ∧ (l_{i} ∨ … ∨ l_{j})
 High level steps in a resolution proof:
 Put the premises or axioms into clause normal form (CNF)
 Add the negation of the to be proven statement, in clause form, to the set of axioms
 Resolve these clauses together, using the resolution rule , producing new clauses that logically follow from them
 Derive a contradiction by generating the empty clause.
 The substitutions used to produce the empty clause are those under which the opposite of the negated goal is true
Resolution  The Resolution Rule

The resolution rule is a single inference that produces a new clause implied by two clauses (called the parent clauses) containing complementary literals
 Two literals are said to be complements if one is the negation of the other (in the following, ai is taken to be the complement to bj).

The resulting clause contains all the literals that do not have complements. Formally:
 Where a_{1}, …, a_{n}, b_{1}, …, b_{m} are literals, and a_{i} is the complement to b_{j}
 The clause produced by the resolution rule is called the resolvent of the two input clauses.
 A literal and its negation produce a resolvent only if they unify under some substitution σ.
 σ Is then applied to the resolvent
Resolution  The Resolution Rule

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)
Resolution – Complete Resolution Algorithm

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.
Resolution – Algorithm in Pseudocode
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"
Resolution  Converting to Clause Normal Form
 Resolution expects input in clause normal form
 Step 1: Eliminate the logical connectives → and ↔
 a ↔ b = (a → b) ∧ (b → a)
 a → b = ¬ a ∨ b
 Step 2: Reduce the scope of negation
 ¬ ( ¬ a) = a
 ¬ (a ∧ b) = ¬ a ∨ ¬ b
 ¬ (a ∨ b) = ¬ a ∧ ¬ b
 ¬ ( ∃ X) a(X) = ( ∀ X) ¬ a(X)
 ¬ ( ∀ X) b(X) = ( ∃ X) ¬ b(X)
Resolution  Converting to Clause Normal Form

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
Resolution  Converting to Clause Normal Form
 Step 5: Skolemization
 Skolem constant
 (∃X)(dog(X)) may be replaced by dog(fido) where the name fido is picked from the domain of definition of X to represent that individual X.
 Skolem function
 If the predicate has more than one argument and the existentially quantified variable is within the scope of universally quantified variables, the existential variable must be a function of those other variables.

(∀X)(∃Y)(mother(X,Y)) ⇒ (∀X)mother(X,m(X))
(∀X)(∀Y)(∃Z)(∀W)(foo (X,Y,Z,W))
⇒ (∀X)(∀Y)(∀W)(foo(X,Y,f(X,Y),w))
Resolution  Converting to Clause Normal Form
 Step 6: Drop all universal quantifiers
 Step 7: Convert the expression to the conjunctions of disjuncts

(a ∧ b) ∨ (c ∧ d)

= (a ∨ (c ∧ d)) ∧ (b ∨ (c ∧ d))

= (a ∨ c) ∧ (a ∨ d) ∧ (b ∨ c) ∧ (b ∨ d)
 step 8: Split each conjunction into a separate clauses, which are just a disjunction of negated and nonnegated predicates, called literals
 step 9: Rename so that no variable symbol appears in more than one clause.

(∀X)(a(X) ∧ b(X)) = (∀X)a(X) ∧ (∀ Y)b(Y)
Resolution  Complete Example
 (Nearly) Classical example: Prove “Fido will die.” from the statements
 “Fido is a dog.”
 “All dogs are animals.”
 “All animals will die.”
 Changing premises to predicates
 ∀ (x) (dog(X) → animal(X))
 dog(fido)
 Modus Ponens and {fido/X}
 animal(fido)
 ∀ (Y) (animal(Y) → die(Y))
 Modus Ponens and {fido/Y}
 die(fido)
Resolution – Complete Example
 Equivalent proof by Resolution
 Convert predicates to clause normal form


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)

 Negate the conclusion

4.
¬
die(fido)
¬
die(fido)
Resolution  Complete Example
Resolution – Further Considerations
 Resolution can be used to establish that a given sentence is entailed by a set of axioms
 However, it cannot , in general, be used to generate all logical consequences of a set axioms

Also, the resolution cannot be used to prove that a given sentence is not entailed by a set of axioms
 Resolution defines a search space
 The decision which clauses will be resolved against which others define the operators in the space

A search method is required

Worst case: Resolution is exponential in the number of clauses to resolve
Resolution – Strategies

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
Concrete System: Prover9
 FirstOrder theorem prover
 Homepage: http://www.cs.unm.edu/~mccune/prover9/
 Successor of the well known “Otter” theorem prover
 Under active development, available for several platforms and released under the GPL
 Graphical userinterface and extensive documentation make Prover 9 comparatively user friendly
 Core of system builds on resolution / paramodulation as inference method
 Prover9 works in parallel with external component „Mace4“
 Mace4 searches for finite models and counterexamples
 This helps to avoid wasting time searching for a proof by first finding a counterexample
Concrete System: Prover9 Input
Concrete System: Prover9 Proof
Concrete System: Prover9 Options
Limitations of FirstOrderTheorem Proving
 Entailment: KB ⊧ Q
 Entailment is a relation that is concerned with the semantics of statements

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
 Entailment for FOL is only semidecidable : If a conclusion follows from premises, then a complete proof system (like resolution) will find a proof.
 If there’s a proof, we’ll halt with it (eventually)
 However, If there is no proof (i.e. a statement does not follow from a set of premises), the attempt to prove it may never halt
Limitations of FirstOrderTheorem Proving
 From a practical point of view this is problematic
 We cannot distinguish between the nonexistence of a proof or the failure of an implementation to simply find a proof in reasonable time.
 Theoretical completeness of an inference procedure does not make a difference in this cases

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
 Often less expressive (but decideable) formalisms or formalisms with different expressivity are more suitable:
 Description Logics

Logic Programming
DESCRIPTION LOGICS
Description Logic
 Most Description Logics are based on a 2variable fragment of First Order Logic
 Classes (concepts) correspond to unary predicates
 Properties correspond to binary predicates
 Restrictions in general:
 Quantifiers range over no more than 2 variables
 Transitive properties are an exception to this rule
 No function symbols (decidability!)
 Most DLs are decidable and usually have decision procedures for key reasoning tasks
 DLs have more efficient decision problems than First Order Logic
 We later show the very basic DL ALC as example
 More complex DLs work in the same basic way but have different expressivity
Description Logic Syntax

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
Description Logic Syntax  Concepts

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)
Description Logic Syntax Roles
 Roles relate to individuals to each other

I.e. directedBy(Pool Sharks, Edwin Middleton), hasChild(Jonny, Sue)

Roles have a domain and a range
 Example:
 Domain(directedBy, Movie)
 Range(directedBy, Person)

Given the above definitions we can conclude that Pool Sharks is a move and that Edwin Middleton is (was) a person.
 Functional Roles
 Roles which have exactly one value
 Usually used with primitive datavalues

A special case of (unqualified) number restriction ≤1 R
Description Logic Syntax Roles
 Transitive Roles

Example: hasAncestor
Simple in a rule language: hasAncestor(X,Z) : hasAncestor(X,Y), hasAncestor(Y,Z).
 Requires more than one variable!

Transitivity can be captured in DLs by role hierarchies and transitive roles:
 Symmetric Roles
 Roles which hold in both directions
 I.e. hasSpouse, hasSibling
 Inverse Roles
 Roles are directed, but each role can have an inverse

I.e. hasParent ≡ hasChild
hasChild(X,Y) ⇔ hasChild(Y,X)
Description Logic Knowledge Bases
 Typically a DL knowledge base (KB) consists of two components
 Tbox (terminology): A set of inclusion/equivalence axioms denoting the conceptual schema/vocabulary of a domain
 Bear ⊑ Animal ⊓ Large
 transitive(hasAncestor)

hasChild ≡ hasParent
 Abox (assertions): Axioms, which describe concrete instance data and holds assertions about individuals
 hasAncestor(Susan, Granny)

Bear(Winni Puh)

From a theoretical point of view this division is arbitrary but it is a useful simplification
A basic Description Logic  ALC
 Smallest propositionally closed DL is ALC
 Only atomic roles
 Concept constructors: ⊔ , ⊓, ¬

Restricted use of quantifiers: ∃, ∀
 “Propositionally closed” Logic in general:

Provides (implicitly or explicitly) conjunction, union and negation of class descriptions
 Example:

Person ⊓ ∀hasChild.(Doctor ⊔ ∃hasChild.Doctor)
A basic Description Logic  ALC
 What can we express in ALC?
 ALC concept descriptions can be constructed as following:
A basic Description Logic  ALC
 Individual assertions :
 a ∈ C

Mary is a Woman.
 Role assertions:
 〈a, b〉 ∈ R

E.g. Marry loves Peter.
 Axioms:
 C ⊑ D
 C ≡ D, because C ≡ D ⇔ C ⊑ D and D ⊑ C

E.g.: A Dog is an animal. A man is a male Person.
The Description Logic Family
 Description Logics are actually a family of related logics
 Difference in expressivity and features, as well as complexity of inference
 Description Logics follow a naming schema according to their features
 ALC = Attributive Language with Complements
 S often used for ALC extended with transitive roles
 Additional letters indicate other extensions, e.g.:
 H for role hierarchy
 O for nominals, singleton classes
 I for inverse roles (e.g., isChildOf ≡ hasChild–)
 N for number restrictions
 Q for qualified number restrictions
 F for functional properties
 R for limited complex role inclusion axioms, role disjointness
 (D) for datatype support
Description Logic  Semantics

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}
Description Logic  Semantics

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
Description Logic  Semantics
 Mapping ALC to First Order Logic:
Description Logic  Reasoning

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
Description Logic  Reasoning

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
Concrete System: Pellet
 Description Logic reasoner
 Homepage: http://clarkparsia.com/pellet
 Written in Java and available from Duallicensed AGPL license for opensource applications
 Proprietary license available for commercial applications
 Sound and complete reasoner aimed at OWLDL inference based on tableaux procedure
 Covers all constructs in OWLDL
 Supporting major part of OWL 2 specification
 Integrates with popular toolkits and editors
 E.g. Jena, Protege, TopBraid Composer
 Comprehensive handson tutorial available:
 http://clarkparsia.com/pellet/tutorial/iswc09
Concrete System: Pellet

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
Concrete System: Pellet

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
Concrete System: Pellet
 Pellet is integrated in OwlSight and performs classification of loaded ontologies
 Lightweight , webbased ontology browser: http://pellet.owldl.com/owlsight/
Concrete System: Pellet
 Classification Results in the Protege Editor
LOGIC PROGRAMMING
Logic Programming
 What is Logic Programming?
 Various different perspectives and definitions possible:
 Computations as deduction
 Use formal logic to express data and programs
 Theorem Proving
 Logic programs evaluated by a theorem prover
 Derivation of answer from a set of initial axioms
 High level (nonprecedural) programming language
 Logic programs do not specifcy control flow
 Instead of specifying how something should be computed, one states what should be computed
 Procedural interpretation of a declarative specification of a problem
 A LP systems procedurally interprets (in some way) a general declarative statement which only defines truth conditions that should hold
Logic Programming Basics

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)
Logic Programming Basics – Horn Logic
 Syntactically a LP rule is a First Order Logic Horn Clause
 The semantics of LP are different form the standard Tarski style FOL semantics (details later)
 Herbrand semantics differ from FOL smeantics in the structures it considers to be models (details later)

→ Minimal model semantics
 A FOL Horn clause is a disjunction of literals with one positive literal, with all variables universally quantified:
 (∀) ¬C_{1} ∨ … ∨ ¬C_{n} ∨ H
 This can be rewritten to closer correspond to a rulelike form:
 (∀) C_{1} ∧ … ∧ C_{n} → H
 In LP systems usually the following (non First Order Logic) syntax is used:
 H : C_{1},...,C_{n}
 Such rules can be evaluated very efficiently , since the resolution of two Horn clauses is a again a Horn clause
Logic Programming – Syntax
 The LP vocabulary consists of:
 Constants: b, cow, “somestring”
 Predicates: p, loves
 Function symbols: f, fatherOf
 Variables: x, y
 Terms can be:
 Constants
 Variables
 Constructed terms (i.e. function symbol with arguments)
 Examples:
 cow, b, Jonny,
 loves(John)
Logic Programming – Syntax
 From terms and predicates we can build atoms:
 For nary predicate symbol p and terms t_{1}, ..., t_{n}, p(t_{1}, ..., t_{n}) is an atom
 A ground atom is an atom without variables
 Examples:
 p(x)
 loves(Jonny, Mary), worksAt(Jonny, SomeCompany)
 worksAt(loves(Mary), SomeCompany)
 Literals
 A literal is a an atom or its negation
 A positive literal is an atom
 A negative literal is a negated atom
 A ground literals is a literal without variables
Logic Programming – Syntax
 Rules
 Given a rule of the form H : B_{1},...,B_{n} we call
 H the head of the rule (its consequent)
 B_{1} …. B_{n} the body of the rule (the antecedent or conditions)
 The head of the rule consists of one positive literal H
 The body of the rule consists of a number of literals B_{1}, ..., B_{n}
 B_{1}, …, B_{n} are also called subgoals
 Examples:
 parent(x) : hasChild(x,y)
 father(x) : parent(x), male(x)
 hasAunt(z,y) : hasSister(x,y), hasChild(x,z)
Logic Programming – Syntax
 Facts denote assertions about the world:
 A rule without a body (no conditions)
 A ground atom
 Examples:
 hasChild(Jonny, Sue)
 Male(Jonny)).
 Queries allow to ask questions about the knowledge base:
 Denoted as a rule without a head:
 ? B_{1},...,B_{n}.
 Examples:
 ?  hasSister(Jonny,y), hasChild(Jonny , z) gives all the sisters and children of Jonny
 ?  hasAunt(Mary,y) gives all the aunts of Mary
 ? father(Jonny) ansers if Jonny is a father
Logic Programming – Semantics

There are two main approaches to define the semantics of LP
 Model theoretic semantics
 Computional semanitcs
 Modeltheoretic semantics
 Defines the meaning of a model in terms of its minimal Herbrand model
 Computational semantics (proof theoretic semantics)
 Define the semantics in terms of an evaluation strategy which describes how to compute a model
 These two semantics are different in style, but agree on the minimal model
 LP semantics is only equivalent to standard FOL semantics
 Concerning ground entailment
 As long as LP is not extended with negation
Logic Programming – Semantics
 Semantics of LP vs Semantics of FOL
 Semantics LP defined in terms of minimal Herbrand model
 Only one minimal model
 Semantics FOL defined in terms of FirstOrder models
 Typically, infinitely many FirstOrder models
 The minimal Herbrand model is a FirstOrder model
 Every Herbrand model is a FirstOrder model
 There exist FirstOrder models which are not Herbrand models
 Example:
 p(a), p(x) → q(x)
 The Minimal Herbrand model: {p(a), q(a)}
 This is actually the only Herbrand model!
 FirstOrder models: {p(a), q(a)}, {p(a), q(a), p(b)}, etc.
Logic Programming – Semantics
 Recall:
 Terms not containing any variables are ground terms
 Atoms not containing any variables are ground atoms
 The Herbrand Universe U is the set of all ground terms which can be formed from
 Constancts in a program
 Function symbols in a program
 Example: a, b, c, f(a)
 The Herbrand Base B is the set of all ground atoms which can be built from
 Predicate symbols in a program
 Ground terms from U
 Example: p(a), q(b), q(f(a))
Logic Programming – Semantics

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 Programming – Semantics
 A Herbrand Model M is a Herbrand Interpretation which makes every formula true, so:
 Every fact from the program is in M
 For every rule in the program: If every positive literal in the body is in M, then the literal in the head is also in M
 The model of a Logic Program P is the minimal Herbrand Model
 This least Herbrand Model is the intersection of all Herbrand Models
 Every program has a Herbrand Model. Thus every model also has a minimal Herbrand Model.
 This model is uniquely defined only for programs without negation

⇒ A very intuitive and easy way to capture the semantics of LP
 As soon as negation is allowed a unique minimal model is not guaranteed anymore
Logic Programming  Negation
 How do we handle negation in Logic Programs?
 Horn Logic only permits negation in limited form
 Consider (∀) ¬C_{1} ∨ … ∨ ¬C_{n} ∨ H
 Special solution: Negationasfailure (NAF):
 Whenever a fact is not entailed by the knowledge base, its negation is entailed
 This is a form of “Default reasoning”
 This introduces nonmonotonic behavior (previous conclusions might need to be revised during the inference process)
 NAF is not classical negation and pushes LP beyond classical First Order Logic
 This allows a form of negation in rules:
 (∀) C_{1} ∧ … ∧ C_{i} ∧ not C_{n} → H
 H : B_{1}, … B_{i}, not B_{n}
Logic Programming  Negation

Logic Programs can also contain recursion
 Example:
 ancestor (x,y) : hasParent(x, y)

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
 It is useful to consider this using a dependency graph
 A predicate is a node in the graph
 There is a directed edge between predicates q and p if they occur in a rule where q occurs in the head and p in the body.

If the dependency graph contains a cycle then the program is recursive
Logic Programming  Negation
 As soon as negation is allowed, cycles in a dependency graph become problematic.

Example: What is the meaning of win(x) : not win(x) ?
 A Solution: Stratification
 Mark edges with negation in the dependency graph
 Separate predicates which are connected through a positive edge in a individual stratum
 Strata can be (partially) ordered
 If each predicate occurs only in one stratum, then the program is called stratifiable
 Each stratum can be evaluated as usual and independently from other strata
→ This guarantees a unique interpretation of a Logic Program using negation
Logic Programming  Subsets
 Classical Logic Programming
 Allows function symbols
 Does not allow negation

Is turing complete
 Full Logic Programming is not decideable

Prolog programs are not guaranteed to terminate
 Several ways to guarantee the evaluation of a Logic Program
 One is to enforce syntactical restrictions
 This results in subsets of full logic programming

Datalog is such a subset
Logic Programming  Datalog
 Datalog is a syntactic subset of Prolog

Originally a rule and query language for deductive databases
 Considers knowledge bases to have two parts

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 )

 Safe Variables:
 Only allows range restricted variables, i.e. each variable in the conclusion of a rule must also appear in a not negated clause in the premise of this rule.

This limits evaluation of variables to finitely many possible bindings
Logic Programming  Reasoning Tasks
 The typical reasoning task for LP systems is query answering
 Ground queries, i.e. ? loves(Mary, Joe)

Nonground query, i.e. ? loves(Mary, x)
 Nonground queries can be reduced to a series of ground queries
 ? loves(Mary, x)

Replace x by every possible value
 In Logic Programming ground queries are equivalent to entailment of facts
 Answering ? loves(Mary, Joe) w.r.t. a knowledge base A is equivalent to checking
A ⊧ loves(Mary, Joe)
Concrete Logic Programming System: IRIS
 Java based Datalog reasoner
 Developed at STI Innsbruck
 Freely available open source project

Homepage: http://www.irisreasoner.org/
 Extensions:
 Stratified / Wellfounded default negation
 XML Schema data types

Various builtin predicates (Equality, inequality, assignment, unification, comparison, type checking, arithmetic, regular expressions,... )
 Highly modular and includes different reasoning strategies
 Bottomup evaluation with Magic Sets optimizations (forwardchaining)

Topdown evaluation by SLDNF resolution (backwardchaining)
Concrete Logic Programming System: IRIS




Concrete Logic Programming System: IRIS
 Example program (also see online demo at http://www.irisreasoner.org/demo):

man('homer').

woman('marge').

hasSon('homer','bart').

isMale(?x) : man(?x).

isFemale(?x) : woman(?x).

isMale(?y) : hasSon(?x,?y).
 Query:

?isMale(?x).
 Output:

Init time: 14ms



Query: ? isMale(?x). ==>> 2 rows in 1ms

Variables: ?x

('bart')

('homer')
Concrete Logic Programming System: IRIS

IRIS performing computations using seminaiv evaluation in combination with stratification and complex datatypes
SUMMARY
Theorem Proving 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
Description Logic Summary
 Description Logics are a syntactic fragment of First Order Logic, based on basic building blocks
 Concepts
 Roles

Individuals
 Limited constructs for building complex concepts, roles, etc.

Many different Description Logics exist, depending on choice of constructs
 Inference in Description Logics focuses on consistency checking and classification
 Main reasoning task: Subsumption

Usually reasoning tasks in DLs can all be reduced to satisfiablity checking
 Efficient Tbox (schema) reasoning
 ABox reasoning (query answering) do not scale so well
Logic Programming Summary
 Logic Programming (without negation) is syntactically equivalent to Horn subset of First Order Logic

The semantics of a Logic Program are however based on its minimal Herbrand Model
 Logic Programming comes in various variants for different applications (as programming language, for knowledge representation)
 Full Logic Programming including function symbols is not decidable
 Datalog is a syntactic restriction of LP, with desirable computational properties

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
References and Further Information
 Mandatory Reading:
 Schöning, U., Logic for Computer Scientists (2nd edition), 2008, Birkhäuser
 Chapter 1 & 2:Normal Forms, Resolution
 Chapter 3: Horn Logic, Logic Programming
 Baader, F. et al., The Description Logic Handbook, 2007, Cambridge University Press
 Chapter 2: Basic Description Logics
 Further Reading:
 Lloyd, J.W. , Foundations of logic programming, 1984, Springer
 Robinson, A. and Voronkov, A. Handbook of Automated Reasoning, Volume I, 2001, MIT Press
 Chapter 2: Resolution Theorem Proving
 Ullman, J. D., Principles of Database and KnowledgeBase Systems, Volume I, 1988, Computer Science Press
 Chapter 3: Logic as a Data Model (Logic Programming & Datalog)
 Wikipedia links:
 http://en.wikipedia.org/wiki/Logic_programming
 http://en.wikipedia.org/wiki/Description_logic
 http://en.wikipedia.org/wiki/Theorem_proving
Questions?