Transcript CSE 291

Department of Computer Science & Engineering
University of California, San Diego
CSE-291: Ontologies in Data Integration
Spring 2004
Bertram Ludäscher
[email protected]
CSE-291: Ontologies in Data & Process Integration
Introduction to Reasoning in
First-order [Predicate] Logic
and Description Logic(s)
•
Introduction to FO (aka PL)
–
–
Syntax, Semantics
Two decidable fragments:
•
•
–
•
Reasoning w/ Tableaux
Description Logic Reasoning
–
•
propositional logic
description logic(s)
…
Discussion of Topics / Assignments
CSE-291: Ontologies in Data & Process Integration
Syntax vs Semantics
• Syntax
– a.k.a. “formation rules”; “grammar”; …
– prescribes what a well-formed formula is (syntactically)
• Semantics
– the “meaning” of well-formed formulas
– defined via a mapping called interpretation
CSE-291: Ontologies in Data & Process Integration
Propositional Logic: Syntax
propositional logic
logic> (or "propositional calculus") A system of symbolic logic using symbols to stand
for whole propositions and logical connectives. Propositional logic only considers
whether a proposition is true or false. In contrast to predicate logic, it does not consider
the internal structure of propositions. http://wombat.doc.ic.ac.uk/foldoc/foldoc.cgi?propositional+logic
<
• Logical symbols:
– conjunction: , disjunction: , negation: ,
– implication: , equivalence: , parentheses:  
• Non-logical symbols:
– propositional variables p, q, r, ...
– signature: set of propositional variables  = {p, q, r, ...}
• Formation rules for well-formed formulas (wff)
– an atomic formula (propositional variable) is a formula
– if F, G are formulas, so are:
• FG, F  G,  F, FG , FG,  F 
CSE-291: Ontologies in Data & Process Integration
Propositional Logic: Semantics
• Propositions can be assigned a truth-value:
– either true or false (classical 2-valued logic: tertium non
datur)
– other propositional logics exist: 3-valued, 4-valued,
temporal, … (modal logics), …, fuzzy logic
• An interpretation I over a signature  is a mapping
– I:   {true, false} , associating a truth value to every
propositional variable
• Truth tables describe how to extend I from atomic to
composite formulas (Boolean Algebra):
– FG, F  G,  F, FG , FG
CSE-291: Ontologies in Data & Process Integration
Boolean Algebra, Truth Tables
http://wombat.doc.ic.ac.uk/foldoc/foldoc.cgi?two-valued+logic
CSE-291: Ontologies in Data & Process Integration
Different Logical Bases
• Often:
– ,  , 
• Alternatively:
–
–
–
–
–
, 
, 
NAND
NOR
XOR
– What about: ite(A,B,C) … if A then B else C ?
CSE-291: Ontologies in Data & Process Integration
Reasoning in Propositional Logic
•
A formula F is …
– valid if it is true for all interpretations I
– satisfiable if it is true for some interpretation I
– unsatisfiable if it is true for no interpretation I
•
Try these:
1.
2.
3.
4.
5.
6.
pq
p  p
p  p
pp
p  p
pp
CSE-291: Ontologies in Data & Process Integration
Reasoning in Propositional Logic
•
Def. “models” relationship “|=”:
– If a formula F evaluates to true for an interpretation I then I
is called a model of F; written I |= F
– I is a model of {F1,…, Fk}, written I |= {F1,…, Fk},if I is a
model of each Fj
•
Automated deduction setting:
– Show that A1,,…, An (axioms) imply T (theorem), that is,
every model of the axioms is also a model of the theorem:
– That is: if I |= {A1,,…, An } then I |= T
– Short: {A1,,…, An } |= T
– Often: Show that A1  …  An  T is unsatisfiable
•
We need a procedure / reasoning algorithm:
– Predicate Calculus (in fact calculi: resolution, tableaux, …)
CSE-291: Ontologies in Data & Process Integration
Example
• {p, p  q } |= q
– Truth table
– Resolution
– Tableaux
CSE-291: Ontologies in Data & Process Integration
Example: Reasoning with Binary Decision Trees
(see also: Binary Decision Diagrams, or BDDs)
A
… B
A
A
if-false
A
if-true
0
1
false
true
0
1
B
0
A
0
1
0
true
false
B
0
CSE-291: Ontologies in Data & Process Integration
0
1
1
AB
A
if-true
1
B
0
…B
A
if-false
AB
A
1
B
0
1
1
Syntax of First-Order Logic (FO)
• Logical symbols:
– , , , , ,  ,  (“for all”),  (“exists”), ...
• Non-logical symbols: A FO signature  consists of
– constant symbols: a,b,c, ...
– function symbols: f, g, ...
– predicate (relation) symbols: p,q,r, ....
function and predicate symbols have an associated arity;
– we can write, e.g., p/3, f/2 to denote the ternary predicate p and the function
f with two arguments
• First-order variables: x, y, ...
• Formation rules for terms:
– constants and variables are terms
– if t1,…,tk are terms and f is a k-ary function symbols then f(t1,...,tk) is a term
CSE-291: Ontologies in Data & Process Integration
Syntax of First-Order Logic (FO)
• Formation rules for formulas:
– if t1,…, tk are terms and p/k is a predicate symbol (of arity k)
then p(t1, …, tk) is an atomic formula (short: atom)
• all variable occurrences in p(t1, …, tk) are free
– if F,G are formulas and x is a variable, then the following are
formulas:
– FG, F  G,  F, FG , FG,  F ,
– x: F (“for all x: F(x,...) is true”)
– x: F (“there exists x such that F(x,...) is true”)
– the occurrences of a variable x within the scope of a quantifier
are called bound occurrences.
CSE-291: Ontologies in Data & Process Integration
Examples
x man(x)  person(x).
man(bill).
child(marriage(bill,hillary),chelsea).
Variable: x
Constants (0-ary function symbols): bill/0, hillary/0, chelsea/0
Function symbols: marriage/2
Predicate symbols: man/1, person/1, child/2
CSE-291: Ontologies in Data & Process Integration
Semantics of Predicate Logic
• Let D be a non-empty domain (a.k.a. universe of discourse). A
structure is a pair I = (D,I), with an interpretation I that maps ...
– each constant symbols c to an element I(c) D
– each predicate symbol p/k to a k-ary relation I(p)  Dk,
– each function symbol f/k to a k-ary function I(f): DkD
• Let I be a structure,  : Vars  D a variable assignment. A
valuation valI, maps Term to D and Fml to {true, false}
–
–
–
–
–
–
–
–
valI, (x) =  (x) ; for x  Vars
valI, (f(t1,...,tk)) = I(f)( valI, (t1),..., valI, (tk) )
valI, (p(t1,...,tk)) = I(p)( valI, (t1),..., valI, (tk) )
valI, (F  G) = valI, (F) and valI, (G) are true
valI, (F  G) = valI, (F) or valI, (G) is true
valI, ( F) = true (false) if valI, (F) is false (true)
valI, ( x F) = valI,[x/t] (F) is true for some t  D
valI, ( x F) = valI,[x/t] (F) is true for all t  D
CSE-291: Ontologies in Data & Process Integration
; for f(t1,...,tk)  Term
; for p(t1,...,tk)  At
; for F,G Fml
; for F,G Fml
; for FFml
; for FFml
; for FFml
Example
Formula F = x man(x)  person(x).
Domain D = {b, h, c, d, e}
Let’s pick an interpretation I:
I(bill) = b, I(hillary) = h, I(chelsea) = c
I(person) = {b, h, c}
I(man) = {b}
Under this I, the formula F evaluates to true.
• If we choose I’ like I but I’(man) = {b,d}, then F evaluates to
false
• Thus, I is a model of F, while I’ is not:
– I |= F
I’ |=/= F
CSE-291: Ontologies in Data & Process Integration
FO Semantics (cont’d)
•
•
•
F entails G (G is a logical consequence of F) if every model of
F is also a model of G:
F |= G
F is consistent or satisfiable if it has at least one model
F is valid or a tautology if every interpretation of F is a model
Proof Theory:
Let F,G, ... be FO sentences (no free variables).
Then the following are equivalent:
1. F_1, ..., F_k |= G
2. F_1  ...  F_k  G is valid
3. F_1  ...  F_k   G is unsatisfiable (inconsistent)
CSE-291: Ontologies in Data & Process Integration
Proof Theory
• A calculus is formal proof system to establish
– F1,…, Fk |= T
• via formal (syntactic) derivations
– F1,…, Fk |– ... |– T, where the “|–” denotes allowed proof steps
• Examples:
– Hilbert Calculus, Gentzen Calculus, Tableaux Calculus, Natural
Deduction, Resolution, ...
• First-order logic is “semi-decidable”:
– the set of valid sentences is recursively enumerable, but not recursive
(decidable)
• Some inference engines:
– http://www.semanticweb.org/inference.html
CSE-291: Ontologies in Data & Process Integration
Querying vs. Reasoning
• Querying:
– given a DB instance I (= logic interpretation), evaluate a query
expression (e.g. SQL, FO formula, Prolog program, ...)
– boolean query: check if I |= 
(i.e., if I is a model of )
– (ternary) query: { (X, Y, Z) | I |=  (X,Y,Z) }
=> check happyFathers in a given database
• Reasoning:
– check if I |=  implies I |=  for all databases I,
– i.e., if  => 
– undecidable for FO, F-logic, etc.
– Descriptions Logics are decidable fragments
 concept subsumption, concept hierarchy, classification
 semantic tableaux, resolution, specialized algorithms
CSE-291: Ontologies in Data & Process Integration
Reasoning Example
• (1) p(0)
• (2) x p(x)  p(s(x))
• (3) p(s(s(0))).
• We want to show that (1) & ... & (2) implies (3)
• Approach: assume negation of (3) and show that it
leads to a contradiction with {(1), (2)}
– Question: Why is this sound?
CSE-291: Ontologies in Data & Process Integration
“Types” of Formulas
() rule for F = A  B
(and other conjunctions)
() rule for F = x: A(X,...)
substitute a -variable X with
an arbitrary term t
CSE-291: Ontologies in Data & Process Integration
() rule for F = A  B
(and other disjunctions)
() rules for F = x: A(X,...)
substitute a -variable X with a
new constant c
(Semantic) Tableaux Rules
• () rule for F = A  B
• () rule for F = A  B
• () rule for F = x: A(X,...)
– substitute a -variable X with an
arbitrary term t
t arbitrary
c new
• () rules for F = x: A(X,...)
– substitute a -variable X with a new
constant c
• A branch is closed if it contains complementary formulas
• A tableaux is closed if every branch is closed
CSE-291: Ontologies in Data & Process Integration
FO Tableaux Calculus
Theorem (Soundness, Completeness of Tableaux
calculus):
Let A1,..., Ak and F be first-order logic sentences.
(Recall: a sentence is a closed formula, i.e., has no free variables)
Then the following are equivalent:
1. A1, ..., Ak |= F
2. A1  ...  Ak  F is unsatisfiable (inconsistent)
3. There is a closed tableaux for {A1, ..., Ak ,  F}
CSE-291: Ontologies in Data & Process Integration
Reasoning with DLs
(Shawn Bowers)
CSE-291: Ontologies in Data & Process Integration