Transcript Inference Methods

Inference Methods
Propositional and Predicate
Calculus
Propositional Logic
• A declarative statement such as “Bill is a CS student”
has a truth value of T or F and is denoted by P (a truth
variable)
• Propositions may be combined with logical operators
and the composite statement has value as shown below.
P  Q is true if either P or Q are true and false if both are false
P  Q is true if both P and Q are true and false if either is false.
¬ P is true if P is false and false if P is true
P  Q is true if P and Q have the same truth value and false if
their values differ
– P  Q is false if P is true and Q is false and true otherwise.
–
–
–
–
• A tautology is always true.
– P  Q  ¬ P  Q is a tautology.
– P  (Q  R)  (P  Q)  (P  R) is a tautology.
Terminology
•  is negation,  is conjunction,  is disjunction,  is
conditional,  is equivalence
• Atomic expression is P,Q,etc representing a declarative
statement having value of True or False, or True or False
• A fully parenthesized expression fpe is a well-formed
formula and is constructed according to following rules
– Any atomic expression
– If A is a fpe, so is A
– If A,B are fpe’s, so are (AB), (AB), (AB) and (AB)
Precedence Relations and Truth Tables
 has highest precedence, then , , , and  .
Every logical operatior is left associative.
A truth table gives the values of an logical expression for every
combination of truth values of the atomic statements. It can be
used to prove a tautology:
•
•
•
P  (Q  R)  (P  Q)  (P  R)
–
P
Q
R
F
F
F
F
F
T
F
T
F
F
T
T
T
F
F
T
F
T
T
T
F
T
T
T
QR
P Q
PR
P  (Q  R)
(P  Q)  (P  R)

Proof by Truth Table
P  (Q  R)  (P  Q)  (P  R)
P
Q
R
QR
P Q
PR
P  (Q  R)
(P  Q)  (P  R)

F
F
F
F
F
F
F
F
T
F
F
T
F
F
T
F
F
T
F
T
F
F
T
F
F
F
T
F
T
T
T
T
T
T
T
T
T
F
F
F
T
T
T
T
T
T
F
T
F
T
T
T
T
T
T
T
F
F
T
T
T
T
T
T
T
T
T
T
T
T
T
T
Contradiction & Proof by Contradiction
• A contradiction is always false
• Suppose A are axioms assumed to be true.
– Want to show A  T
– If T  A  False is a tautology, then
• T  A must be false
• So, since A is true, T must be false and so T is true.
Rules of Inference
•
•
•
•
P , P  Q then Q - modus ponens
¬ Q, P  Q then ¬ P - modus tollens
P  Q, Q  R then P  R - chaining
(¬ P  Q), (P  R)  (Q  R) – resolution
– P  R  ¬R  P
–¬PQ PQ
– ¬R  Q  Q  R
Resolution In Propositional Calculus
• Refutation
– Resolution is not complete since
P  Q  P  Q but cannot infer from P,Q.
– However can show that  (P  Q) is
inconsistent with P  Q.
•  (P  Q)  P, Q which resolve with P,Q to give
the empty clause
• Since P  Q is assumed to be true and the empty
clause is false, P  Q follows from P  Q (proof by
contradiction)
Resolution Refutation
• Resolution Refutation
– Let W be a set of wffs. Want to show that
Wt
• Convert W to clause form C.
• Convert t to clause form c .
• Iteratively apply resolution to C U {c}, adding the
resolvent until either no more resolvents can be
added or until the empty clause Ø is produced.
• If Ø is produced, then W  t else t does not follow
from W
Modeling Clauses with CLIPS
(deftemplate term
(slot cid) (slot tid) (slot sign) (slot pSym) (slot Proc)
)
(deftemplate match-fact
(multislot match))
(deffacts clauses
(term (cid 1) (tid 1) (sign T) (pSym P) (Proc N))
(term (cid 1) (tid 2) (sign T) (pSym Q) (Proc N))
(term (cid 2) (tid 3) (sign F) (pSym P) (Proc N))
(term (cid 2) (tid 4) (sign T) (pSym R) (Proc N))
(term (cid 2) (tid 5) (sign T) (pSym S) (Proc N))
(maxCID 2)
(not-matched)
)
Resolution Rule
(defrule match
(term (cid ?i) (tid ?r1) (sign T) (pSym ?X) (Proc N))
(term (cid ?j) (tid ?r2) (sign F) (pSym ?X) (Proc N))
(test (not (= ?i ?j)))
?idx <- (not-matched)
?jdx <- (maxCID ?n)
=>
(printout t "Matched clause " ?i " with clause " ?j crlf)
(retract ?idx )
(retract ?jdx )
(assert (matched))
(assert (maxCID (+ ?n 1)))
(assert (match ?i ?j))
(assert (omit1 ?r1))
(assert (omit2 ?r2))
)
Mark Terms in two clauses
(defrule mark-terms-in-resolved-clauses
(match ?i ?j)
?mrk <- (term (cid ?c) (tid ?t) (sign ?s) (pSym ?p) (Proc N))
(test (or (= ?c ?i) (= ?c ?j)))
=>
(retract ?mrk)
(assert (term (cid ?c) (tid ?t) (sign ?s) (pSym ?p) (Proc Y)))
)
Add other terms to resolvent from 1st clause
(defrule build-resolventfrom1
(match ?i ?j)
(term (cid ?i) (tid ?t) (sign ?s) (pSym ?X) (Proc Y))
(maxCID ?mc)
(omit1 ?r1)
(test (not (= ?t ?r1)))
=>
(assert (term (cid ?mc) (tid ?t) (sign ?s) (pSym ?X) (Proc N)))
(printout t "Resolvent clause " ?mc " with terms " ?t crlf)
)
Add other terms to resolvent from 2nd clause
(defrule build-resolventfrom2
?idx <- (match ?i ?j)
(term (cid ?j) (tid ?t) (sign ?s) (pSym ?X) (Proc Y))
(maxCID ?mc)
(omit2 ?r2)
(test (not (= ?t ?r2)))
=>
(assert (term (cid ?mc) (tid ?t) (sign ?s) (pSym ?X) (Proc N)))
(printout t "Resolvent clause " ?mc " with terms " ?t crlf)
)