Predicate Logic
or FOL
Chapter 8
Syntax
• See text for formal rules.
• All of propositional + quantifiers, predicates,
functions, and constants.
• Variables can take on values of constants or terms.
• Term = reference to object
• Variables not allowed to be predicates.
– that’s 2nd order logic
• Notation: unlike Prolog, variables are lower case,
etc.
Term
• A term with no variables is a ground term.
• Composite Objection: function of terms or
primitives
– Convenience: we don’t want to give names to
all objects
– e.g. nounphrase(det(the),adj(tall),noun(tree)).
– E.g. LeftLeg(John).
– Successor of 1 may be s(1), but we write 2.
– Successor of 2 s(s(1)), but we write 3.
Goldbach’s Conjecture
• For all n, if integer(n), even(n), greater(n,2)
then there exists p1, p2, integer(p1),
integer(p2), prime(p1),prime(p2), and
equals(n,sum(p1,p2)).
• Quantifiers: for all, there exists
• Predicates: integer, greater, prime, even,
equals.
• Constants: 2
• Functions: sum.
Semantics
• Validity = true in every model and every
interpretation.
• Interpretation = mapping of constants,
predicates, functions into objects, relations,
and functions.
• For Goldbach wrt to standard integer
model: interpretation = mapping n to an
even integer. (Context).
Representing World in FOL
• All kings are persons.
• for all x, King(x) => Person(x). OK.
• for all x, King(x) & Person(x). Not OK.
– this says every object is a king and a person.
• In Prolog: person(X) :- king(X).
• Everyone Likes icecream.
• for all x, Likes(x, icecream).
Negating Quantifiers
• ~ there exist x, P(x)
• ~ for all x, P(x)
For all x, Likes(x,Icecream)
No one likes liver.
For all x, not Likes(x,Liver)
• For all x, ~P(x)
• There exists x, ~P(x)
• There does not exist an x,
not Likes(x,Icecream)
• Not there exists x,
Iikes(x,Liver).
More Translations
• Everyone loves
someone.
• There is someone that
everyone loves.
• Everyone loves their
father.
• See text.
• For all x, there is a y such
that Loves(x,y).
• There is an M such that
for all y, Loves(x,M).
• M is skolem constant
• For all x,
Loves(x,Father(x)).
• Father(x) is skolem
function.
Inference: almost complete
• Propositionalization: Grounding out the variables
– For x, King(x) and Greedy(x) => Evil(x).
– King(John). Greedy(John).
– Replace all variables by given constants =>
• Evil(John) and replace fully instantiate predicates by propositional
variables.
• If process finite, then propositional completeness =>
predicate completeness.
• Function symbols yield infinite number of terms, but
theorem almost true.
• Semidecidable. If entailed, eventually find a proof,
but if not entailed, proof search is unbounded.
Unification
• If p and q are logical expressions, then
Unify(p,q) = Substitution List S if using S
makes p and q identical or fail.
• Standardize apart: before unifying, make
sure that p and q contain different variable
names.
Most General Unifier (MGU)
• f(X,g(Y)) unifies with f(g(Z),U) with
substitutions {X/g(a), Y/b, U/g{b)}.
• But also if {X/g(Z), U/g(Y)}.
• The MGU is unique up to renaming of
variables.
• All other unifiers are unify with the MGU.
• Use Prolog with = for unification.
Occurs Checking
• When unifying a variable against a complex
term, the complex term should not contain
the same variable, else non-match.
• Prolog doesn’t check this.
• Ex. f(X,X) and f(Y,g(Y)) should not unify.
Modeling with Definite Clauses:
one positive literal
1. It is a crime for an american to sell
weapons to a hostile country.
1’. American(x)&Weapons(y)&Hostile(z) &
Sell(x,y,z) => Criminal (x).
2. The country Nono has some missiles.
There exists x Owns(Nono,x)&Missile(x).
2’. Missile(M1). … Constant introduction
2’’. Owns(Nono,M1).
Prove: West is a criminal
3. All of its missiles where sold to it by Colonel
West.
3’. Missile(x)&Owns(Nono,x) =>
Sells(West,x,Nono).
4’. Missile(x) => Weapon(x). .. “common sense”
5’. Enemy(x,America) => Hostile(x).
6’. American(West).
7’. Enemy(Nono,American).
Forward Chaining
• Start with facts and apply rules until no new facts
appear. Apply means use substitutions.
• Iteration 1: using facts.
• Missile(M1),American(West), Owns(Nono,M1),
Enemy(Nono,America)
• Derive: Hostile(Nono), Weapon(M1),
Sells(West,M1,Nono).
• Next Iteration: Criminal(West).
• Forward chaining ok if few facts and rules, but it
is undirected.
Resolution gives forward chaining
• Enemy(x,America)
=>Hostile(x)
• Enemy(Nono,America)
• |- Hostile(Nono)
• Not Enemy(x,America)
or Hostile(x)
• Enemy(Nono,America)
• Resolve by {x/Nono}
• To Hostile(Nono)
Backward Chaining
• Start with goal, Criminal(West) and set up
subgoals. This ends when all subgoals are
validated.
• Iteration 1: subgoals American(x),
Weapons(y) and Hostile(z).
• Etc. Eventually all subgoals unify with
facts.
Resolution yeilds
Backward Chaining
• A(x) &W(y)&H(z)&
S(x,y,z) =>C(x)
• -A(x) or –W(y) or
–H(z) or –S(x,y,z) or C(x).
• Add goal –C(West).
• Yields –A(West) or
-W(y) or –H(z) or
-S(West,y,z). Etc.
Resolution is non-directional
• Both a power (inference representation) and
a weakness (no guidance in search)
• -a or –b or –c or d or e equals
• a,b,c =>d or e and
• a,b,c, -d => e etc.
• Prolog forces directionality and results in an
incomplete theorem prover.
FOL -> Conjuctive Normal Form
•
•
•
•
•
Similar to process for propositional logic, but
Use negations rules for quantifiers
Standarize variables apart
Universal quantification is implicit.
Skolemization: introduction of constants and
functions to remove existential quantifiers.
Skolemization
• Introduction of constants or functions when
removing existential quantifier.
• There exists an x such that P(x) becomes:
P(A) for some new constant symbol A.
• Everyone has someone who loves him
• For all x, Loves(F(x),x) where F(x) is a new
function.
Resolution in CNF
• Just like propositional case, but now
complimentary first order literals unify.
• Theorem (skipping proof):
FOL with resolution is refutation complete,
i.e. if S is a set of unsatisfiable clauses,
then a contradiction arises after a finite
number of resolutions.
• Let’s take in on faith!
Results
• Proof of theorems in:
– Lattice Theory
– Group theory
– Logic
• But didn’t generate the theorem.
• Lenat’s phd thesis AM generated
mathematical theorems, but none of interest.
Limitations
• 2nd order: What is the relationship between Bush and
Clinton?
• Brittle: If knowledge base has contradiction, then
anything derivable. (false |= P)
• Scaleability
– Expensive to compute
– Difficult to write down large number of statements that are
logically correct.
• Changing World (monotoncity): what was true, is not
longer.
• Likelihoods: What is likelihood that patient has
appendicitis given high temp.
• Combining Evidence
Monotonicity
•
•
•
•
•
•
Unluckily, the pilot’s plane caught on fire.
Luckily, he jumped out with his parachute.
Unluckily the parachute didn’t work.
Luckily he landed in a swimming pool.
Unluckily it had no water.
Luckily is was all a dream.
Situation Calculus/Planning
• The world changes and actions change it.
• What to do?
• Early approach: Define Actions via:
–
–
–
–
Preconditions : conjunctions of predicates
Effects: changes to world if operator applied
Delete conditions: predicates to delete
Add conditions: predicates to add
Blocks World Example
• Action: Move(b,x,y)…move b from x to y
• Preconditions:
– On(b,x)&Clear(y)&Block(b)& Clear(b)
– Careful: and b \= y else problems ( b to b)
• Postconditions:
– On(b,y) & Clear(x) & not On(b,x) & not Clear(y)
• Similar for other operators/actions.
• Now search: better plan searchers possible.
More Extensions
• Special axioms for time, space, events,
processes, beliefs, goals
• Try to do any simple story, e.g. Goldilocks
and three bears.
• How would you know you did it?
• Problems:
– Represent what’s in story
– Represent what’s not in story but relevant.
– Inferencing
Example Questions
•
•
•
•
Was Goldilocks hungry?
Was Goldilocks tired?
Why did the bed break?
Could the baby bear say “Papa, don’t talk
unless you are spoken too”.
Expert Systems:
Engineering Approach
• We can keep the representation language of FOL,
but do not adopt the semantics.
• Attach to each fact and rule a belief (#)
• Provide an ad hoc calculus for combining beliefs.
• Now multiple proofs valuable since they will add
evidence.
• This worked, if domain picked carefully. The hard
part: getting the rules or knowledge.
Mycin: by Shortliffe
• First rule based system that performed
better than average physician at blood
disease diagnosis.
• Required 500+ rules that were painful to
capture. (Knowledge Acquisition)
• Used ad hoc calculus to combine
“confidences” in rules and facts.
Soy Bean Disease Diagnosis
• Expert diagnostician built a rule-based
expert system for the task.
• System worked, but not as good as he was.
• Some knowledge was not captured.
• Using Machine Learning, rules were create
from a large data base.
• The ML rules did better than the expert
rules, but did not perform as well as the
expert.
Descargar

Document