Transcript logic-to-prolog

From Propositional Logic to
PROLOG
CSE P573
Applications of Artificial Intelligence
Henry Kautz
Fall 2004
Tonight
•
•
Discussion of assignment 1
Games of chance
1. Basic elements of logic
2. Resolution
• Ground [Application: diagnosis]
• With variables
• With function symbols
3. Prolog
Nondeterministic Games
Involve chance:
dice, shuffling, etc.
Chance nodes:
calculate the
expected value
E.g.: weighted
average over all
possible dice rolls
In Practice...
Chance adds dramatically to
size of search space
Backgammon: number of distinct
possible rolls of dice is 21
Branching factor b is usually around
20, but can be as high as 4000 (dice
rolls that are doubles)
Alpha-beta pruning is generally
less effective
Best Backgammon programs
use other methods
Imperfect Information
E.g. card games, where
opponents’ initial cards are
unknown
Idea: For all deals
consistent with what you
can see
compute the minimax value
of available actions for each
of possible deals
compute the expected value
over all deals
Probabilistic STRIPS
Planning
domain: Hungry Monkey
shake:
if (ontable)
Prob(2/3) -> +1 banana
Prob(1/3) -> no change
else
Prob(1/6) -> +1 banana
Prob(5/6) -> no change
jump: if (~ontable)
Prob(2/3) -> ontable
Prob(1/3) -> ~ontable
else
ontable
What is the expected
reward?
[1] shake
[2] jump; shake
[3] jump; shake; shake;
[4] jump; if (~ontable){ jump;
shake}
else { shake; shake }
ExpectiMax
ExpectiMax (n) 
U (n) if n is a terminal node
max{ ExpectiMax ( s ) | s  children (n)} if n is max node
 P(s)ExpectiMax (s) if n is a chance node
schildren( n )
Hungry Monkey: 2-Ply Game Tree
shake
jump
jump
1/6
1/3
2/3
shake
jump
shake jump
5/6
shake jump
shake
2/3 1/3 2/3 1/3 2/3 1/3 1/6 5/6 2/3 1/3 1/6 5/6 2/3 1/3 1/6 5/6
0
0
1
0
0
0
1
0
1
1
2
1
0
0
1
0
ExpectiMax 1 – Chance Nodes
shake
jump
jump
1/6
1/3
2/3
shake
jump
shake jump
2/3
5/6
shake jump
shake
7/6
0
1/6
2/3 1/3 1/6 5/6
2/3 1/3 2/3 1/3 2/3 1/3 1/6 5/6
2/3 1/3
1/6 5/6
0
0
0
1
0
0
0
0
1
1/6
1
0
1
1
2
1
0
0
1
0
ExpectiMax 2 – Max Nodes
shake
jump
2/3
jump
1/6
1/3
2/3
2/3
1/6
7/6
1/6
shake
jump
shake jump
5/6
shake jump
shake
7/6
0
1/6
2/3 1/3 1/6 5/6
2/3 1/3 2/3 1/3 2/3 1/3 1/6 5/6
2/3 1/3
1/6 5/6
0
0
0
1
0
0
0
0
1
1/6
1
0
1
1
2
1
0
0
1
0
ExpectiMax 3 – Chance Nodes
shake
jump
1/2
1/3
2/3
jump
1/6
1/3
2/3
2/3
1/6
7/6
1/6
shake
jump
shake jump
5/6
shake jump
shake
7/6
0
1/6
2/3 1/3 1/6 5/6
2/3 1/3 2/3 1/3 2/3 1/3 1/6 5/6
2/3 1/3
1/6 5/6
0
0
0
1
0
0
0
0
1
1/6
1
0
1
1
2
1
0
0
1
0
ExpectiMax 4 – Max Node
1/2
shake
jump
1/2
1/3
2/3
jump
1/6
1/3
2/3
2/3
1/6
7/6
1/6
shake
jump
shake jump
5/6
shake jump
shake
7/6
0
1/6
2/3 1/3 1/6 5/6
2/3 1/3 2/3 1/3 2/3 1/3 1/6 5/6
2/3 1/3
1/6 5/6
0
0
0
1
0
0
0
0
1
1/6
1
0
1
1
2
1
0
0
1
0
Policies
The result of the ExpectiMax analysis is a
conditional plan (also called a policy):
Optimal plan for 2 steps: jump; shake
Optimal plan for 3 steps:
jump; if (ontable) {shake; shake}
else {jump; shake}
Probabilistic planning can be generalized
in many ways, including action costs and
hidden state
The general problem is that of solving a
Markov Decision Process (MDP)
Summary
Deterministic games
Minimax search
Alpha-Beta pruning
Static evaluation functions
Games of chance
Expected value
Probabilistic planning
Strategic games with large
branching factors (Go)
Relatively little progress
Desiderata for Knowledge
Representation
1. Declarative
• Separate knowledge from specific use
2. Expressive
• General rules as well as facts
• Incomplete information
3. Concise
• Can draw many new conclusions
4. Effectively computable
• Unambiguous
How does STRIPS
measure up?
Basic Idea of Logic
By starting with true assumptions, you can
deduce true conclusions.
Francis Bacon (1561-1626)
No pleasure is comparable to
the standing upon the
vantage-ground of truth.
Blaise Pascal (1623-1662)
We know the truth, not only
by the reason, but also by the
heart.
Thomas Henry Huxley (18251895)
Irrationally held truths may be
more harmful than reasoned
errors.
François Rabelais (c. 14901553)
Speak the truth and shame
the Devil.
John Keats (1795-1821)
Beauty is truth, truth beauty;
that is all
Ye know on earth, and all ye
need to know.
Daniel Webster (1782-1852)
There is nothing so powerful
as truth, and often nothing so
strange.
The Big Three



Entailment
m – something that determines whether a
sentence S is true or false – a “possible world”
mS
• S is true in m
• m is a model of S
ST
• S entails T
• Every model of S is a model of T
• When S is true, then T must be true
Implication
xy
0
0
1
1
0
1
0
1
1
1
0
1
xy
0
0
1
1
0
1
0
1
1
1
0
1
Consequence
A logic includes a set of mechanical rules
for determining which sentences can be
derived from other sentences
S T
T is a consequence of S
Sound:
if S  T then S  T
Complete:
if S  T then S  T
Resolution
P v Q,
Q
~P
P v Q,
~P v R
QvR
PvQvS,
PvS
~Q v S
Bush or Kerry will get a popular
majority. Bush won’t get a
popular majority.
Bush or Kerry will get a popular
major. If Bush gets a popular
majority, the country will unite.
If neither Bush or Kerry get a
popular majority, the Supreme
Court will pick the president.
If Kerry gets a popular majority,
the Supreme Court will pick the
president.
Conjunctive Normal Form
• Any sentence is equivalent to one where:
• Top level is a conjunction of clauses
• Each clause is a disjunction of literals
• Each literal is a proposition or its
negation
In the worst-case, how much
larger is the CNF form of a
sentence?
What can
we do about it?
New Variable Trick
Putting a formula in clausal form may increase its
size exponentially
But can avoid this by introducing dummy variables
(abc)(def) {(ad),(ae),(af),
(bd),(be),(bf),
(cd),(ce),(cf) }
(abc)(def)  {(gh),
(abcg),(ga),(gb),(gc),
(defh),(hd),(he),(hf)}
Dummy variables don’t change satisfiability!
Proof by Refutation
ST
iff (S   T)  false
Model theory:
ST
iff S   T has no
models (is unsatisfiable)
Resolution Proof
DAG, where leaves are input clauses
• Internal nodes are resolvants
If the unicorn is
• Root is false (empty clause)
mythical, then it is
immortal, but if it is not
mythical, it is a mortal
mammal. If the
( A  H)
(I  H)
( H)
unicorn is either
immortal or a
(M  A)
(A)
(I)
( M  I)
mammal, then it is
horned.
Prove: the unicorn is
(M)
( M)
horned.
()
Expert System for Automobile
Diagnosis
Knowledge Base:
GasInTank  FuelLineOK  GasInEngine
GasInEngine  GoodSpark  EngineRuns
PowerToPlugs  PlugsClean  GoodSpark
BatteryCharged  CablesOK  PowerToPlugs
Observed:
 EngineRuns,
GasInTank, PlugsClean, BatteryCharged
Prove:
 FuelLineOK   CablesOK
Solution by Resolution
Knowledge Base and Observations:
( GasInTank   FuelLineOK  GasInEngine)
( GasInEngine   GoodSpark  EngineRuns)
( PowerToPlugs   PlugsClean  GoodSpark)
( BatteryCharged   CablesOK  PowerToPlugs)
(EngineRuns)
(GasInTank)
(PlugsClean)
Unit propagation =
(BatteryCharged)
Resolution where
Negation of Conclusion:
one clause must be
(FuelLineOK)
a single literal
(CablesOK)
How Do You Know What to
Prove?
In this example were given the diagnosis we
wanted to prove:
FuelLineOK   CablesOK
But, in general, how do you know what to
prove?
A powerful and widely-used technique for
finding an hypothesis that explains an
observed system fault ( EngineRuns) is
Consistency Based Diagnosis.
Consistency-Based Diagnosis
1. Make some Observations O.
2. Initialize the Assumption Set A to assert that
all components are working properly.
3. Check if the KB, A, O together are
inconsistent (can deduce false).
4. If so, delete propositions from A until
consistency is restored (cannot deduce
false). The deleted propositions are a
diagnosis.
There may be many possible diagnoses
Example
Is KB Observations Assumptions consistent?
KB { EngineRuns, GasInTank, PlugsClean,
BatteryCharged}  { FuelLineOK, CablesOK }  false
• Must restore consistency!
KB { EngineRuns,GasInTank, PlugsClean,
BatteryCharged}  {CablesOK }  false
• So  FuelLineOK is a possible diagnosis!
KB { EngineRuns,GasInTank, PlugsClean,
BatteryCharged}  {FuelLineOK}  false
• So  CablesOK is a possible diagnosis!
Complexity of Diagnosis
If KB is Horn, then each consistency test takes
linear time.
Complexity = ways to delete propositions from
Assumption Set that are considered.
• Single fault diagnosis – O(n2)
• Double fault diagnosis – O(n3)
• Triple fault diagnosis – O(n4)
…
Deep Space One
• Autonomous diagnosis & repair “Remote
Agent”
• Compiled systems schematic to 7,000 var SAT
problem
Started: January 1996
Launch: October 15th, 1998
Experiment: May 17-21
Tonight
•
•
Discussion of assignment 1
Games of chance
1. Basic elements of logic
2. Resolution
• Ground [Application: diagnosis]
• With variables
• With function symbols
3. Prolog
First-Order Logic
All men are mortal.
 x . (man(x)  mortal(x))
No man is not mortal.
  x . (man(x)   mortal(x) )
Everybody has somebody they lean on.
 x . (person(x)   y . (person(y)  leans_on(x,y))
A number is less than it’s successor.
 n . (number(x)  less_than(x, successor(x)) )
Nothing is less than zero.
  x . less_than(x, ZERO)
Quantifiers
Variables
Constants
Function Symbols
First-Order Clausal Form
•
•
•
•
Begin with universal quantifiers (implicit)
Rest is a clause
No , but may use function symbols instead
Variables in each clause are unique
 man(x)  mortal(x)
person(x)  person(friend(x))
person(y)  leans_on(friend(y))
 number(x)  less_than(x, successor(x))
Unification
Can resolve clauses if can unify one pair of literals
• Same predicate, one positive, one negative
• Match variable(s) to other variables,
constants, or complex terms (function
symbols)
• Carry bindings on variables through to all
the other literals in the result!
(Mortal(HENRY))
(Mortal(y)Fallible(y))
(Fallible(HENRY))
Unification with Multiple
Variables
You always hurt the ones you love.
Politicians love themselves.
Therefore, politicians hurt themselves.
 love(x,y)hurt(x,y)
politician(z)love(z,z)
politician(w)hurt(w,w)
Unification with Function
Symbols
A number is less than
its successor
(Less(a,suc(a)))
“Less than” is transitive
(Less(b,c) Less(c,d) Less(b,d))
{c/a, d/suc(a)}
(Less(b,a) Less(b,suc(a)))
rename variables:
{e/a,f/suc(a)}
(Less(e,f) Less(e,suc(f)))
Less(a,suc(suc(a)))
A number is less than the
successor of its successor
Tonight
•
•
Discussion of assignment 1
Games of chance
1. Basic elements of logic
2. Resolution
• Ground [Application: diagnosis]
• With variables
• With function symbols
3. Prolog
Making FOL Practical
Barriers to using FOL:
• Choice of clauses to resolve
• Huge amount of memory to store DAG
• Getting useful answers to queries (not just
“yes” or “no”)
PROLOG’s answers:
• Simple backward-chaining resolution
strategy – left/right, first to last clause
• Tree-shaped proofs – no need to store entire
proof in memory at one time
• Extract answers to queries by returning
variable bindings
Prolog Interpreter
binding_list disprove(literal neglit){
choose (clause c) such that
(binding = unify(head(c),neglit))
if (no choice possible){
backtrack to last choice;}
for (each lit in body(c)){
binding = binding U
disprove(substitute(lit,binding));
}
return binding;
}
Example
•
•
•
•
Rich people are happy.
People who love happy people are happy.
Your spouse loves you.
Your mother loves you.
•
•
•
•
•
•
Bill is rich.
Melinda is Bill’s spouse.
Elaine is Melinda’s mother.
Mary is Bill’s mother.
Paul is rich.
Barbara is Henry’s mother.
run prolog,
consult(happy)
happy.pl
happy(X) :- rich(X).
happy(X) :- loves(X,Y),happy(Y).
loves(X,Y) :- spouse(X,Y).
loves(X,Y) :- mother(X,Y).
rich(bill).
spouse(melinda,bill).
mother(elaine,melinda).
mother(mary,bill).
rich(paul).
mother(barbara,henry).
Prolog Limitations
• Only handles definite clauses (exactly one
positive literal per clause)
• No true disjuction: cannot express e.g.
happy(bill) v happy(henry)
• Tree-shaped proofs means some sub-steps
may be repeatedly derived
• DATALOG: does forward-chaining
inference and caches derived unit
clauses
• Interpreter can get into an infinite loop if care
is not taken in form & order of clauses
toohappy.pl
happy(X) :- rich(X).
happy(X) :- loves(X,Y),happy(Y).
loves(X,Y) :- spouse(X,Y).
loves(X,Y) :- mother(X,Y).
rich(bill).
spouse(melinda,bill).
mother(elaine,melinda).
mother(mary,bill).
rich(paul).
mother(barbara,henry).
loves(bill,melinda).
loves(henry,barbara).
Exercise
You have just been hired by snacks.com, an Internet
startup that provides snacking recommendations.
Your first assignment is to create an expert system
that will recommend snacks according to the
following rules:
• Every snack should contain one beverage and one
munchie.
• Sweet beverages are good with salty munchies.
• Bitter beverages are good with sweet munchies or
salty munchies.
Define a predicate snack(X,Y) that makes such
recommendations.
Get started with: prolog/snack.pl
Next Week
Data structures in Prolog
Natural language processing