Logic

Zhaoyu Luo bio photo By Zhaoyu Luo

Relations

  • Formal System = Formal Language + Inference Rules
  • Propositional Calculus vs FOPC
    • Propositional Calculus is Formal System
    • FOPC is Formal System
    • FOPC has quantifier while Propositional Calculus does not
      • Once we have rules for inferring nonquantified sentences from quantified sentences, it becomes possible to reduce first-order inference to propositional inference.
    • In Ontological Commitment, While propositional logic commits only to the existence of facts, first-order logic commits to the existence of objects and relations and thereby gains expressive power.
  • Logical Consequence (entailment)
    • Syntactic Consequence: therefore, -
      • KB -i A, A is derived from KB by i
      • The study of the syntactic consequence (of a logic) is called (its) proof theory
      • sequent
    • Semantic Consequence: entails, models, =
      • The formal definition of entailment is this: α |= β if and only if, in every model in which α is true, β is also true.
    • Material Consequence (Conditional): ->; p -> q; if p then q
  • logic cs540 Chuck Dyer
  • FOPC cs540 Chuck Dyer

Logic

  1. Represent world knowledge in logic
    • Perform inferences; i.e. deduce what logically follows. Why?
  • first order predicate calculus (FOPC)
    • Seeing if a logical sentence is satisfiable
    • Seeing what logically follows from some given logical sentences
    • well defined
    • sound (inferences are correct)
    • complete (all possible deduction can be mechanically produced)
  • Propositional calculus
    • Components are Atomic Sentences: it is cold, it is raining, etc. P, Q, etc (evaluate to TRUE or FALSE)
  • Theorem proving called “model checking” in computer security

Connectives create compound sentences

  • If P and Q are logical sentences then so are
    • (P) - can add parens
    • ^P - negation
    • P^Q - conjunction
    • PvQ - disjunction
    • P=>Q - implication, rules, if then
    • P<=>Q - equivalence, if and only if, == (triple bar恒等于)
Truth Tables that Define the Connectiver

P   Q   ^P  P^Q PvQ P->Q(**^PvQ**)  P<->Q
F   F   T   F   F   T               T
F   T   T   F   T   T               F
T   F   F   F   T   F               F
T   T   F   T   T   T               T
  • R: it is raining, V: take umbrella
    • Translate: If it is raining, take your umbrella
    • Wrong R^U: it is currently raining and you should take your umbrella
    • Right R->: if it is raining, then you should take your umbrella

A grammatically correct logical sentence is called a well formed formula (WFF)

Some jargons

  • a model is a “possible world” where the truth value of each primitive is given/specified
  • a model of a set of WFF is one that makes all the sentences true
  • a valid (or tauta logical) WFF is true in all world states
  • a satisfiable WFF is true in at least one world state

  • an unsatisfiable WFF is never true

      WFF     Valid   Satisfiable Unsatisfiable
  P               if p=true
  Pv^P    Yes
  P^^P                        Yes

Is (P^Q) -> (PvQ) valid, satisfiable or unsatisfiable? show via a truth table

PvQ is the same with [^(P^Q)]v[PvQ]

P   Q   (P^Q)   (PvQ)   P^Q->PvQ
F   F   F       F       T
F   T   F       T       T
T   F   F       T       T
T   T   T       T       T

So (P^Q) -> (PvQ) is valid
Using Search to Find What Logically Follows

Task: Given WFF1, WFF2 … WFFn, show WFFz

  1. Viewing as a search space
    • using valid logical operatori (i = [1, n])
    • Keep going until we add WFFz

Inference rules

Natural Deduction

  • Deduction ins Propositional Calculus
    • Notation, if we believe these WFF(s) - then these WFF(s) logical follow
    • [ - sequent calculus](http://en.wikipedia.org/wiki/Sequent_calculus#Natural_deduction_systems)
  • AND Elimination (AE)
    • (a1 ^ a2 ^…^ an) - ai, i means All items in an AND are true
  • AND Introduction (AI)
    • (a1, a2, a3,…, an) - (a1 ^ a2 ^…^ an)
  • OR Introduction (OI)
    • alpha - (alpha v beta), for any WFF beta
  • Double-Negation Elimination (DNE)
    • ^(^alpha) - alpha
  • Double-Negation Introduction (DNI)
    • alpha - ^(^alpha)
  • Modus Ponens (MP)
    • (a -> b, a) - b
    • (^a v b, a) - b
  • Unit Resolution (UR)
    • (a v b, ^b) - a
  • Resolution
    • (a v b, ^b v c) - (a v c), via “cast analysis” of b being true of false
    • (^a v b, ^b v c) - (^a v c), if we preprocess our “givens” we only need this inference rule
  • Equivalence Elimination (EE)
    • a <-> b - (a->b) ^ (b->a)
  • Some Implicit Rules
    • a ^ b - b ^ a
    • a v b - b v a
    • a - (a)
    • (a) - a
Example

Given:

  1. P
    • !Q
    • P->(R ^ W)
    • (R ^ !Q)-> S

show S:

WFF         Justification

P           Given
!Q          Given
P->(R^W)    Given
(R^!Q)->S   Given
R^W         MP on **1** + **3**
R           AE on **5**
(R^!Q)      AI on **2** + **6**
S           MP on **4** + **7**

Operator Precedence for FOPC (Figure 7.7): !, ^, v, ->, <->

FOPC

Extensions to propositional calculus

  1. have “terms” that refer to (or represent) objects in the world, e.g. John, Marry, Fido
    • propositions now have arguments: married(John, Marry)
    • can quantify over variables
    • Vx, for all valueable(x) - a “big AND”
      • One cannot say VP P(John), this would be 2nd order
    • Ex, exists valueable(x) - a “big OR” - Functions represent terms, not truth values
    • motherOf(Aaron Rodgers), motherOf: function, it “represent” a term
    • functions are also terms: motherOf(fatherOf(John))
      • Notes: the arguments to predicates and functions are terms

To recap

Terms are

  1. constants such as John, Marry, etc
    • variables, used in V’s and E’s
    • functions, e.g. fatherOf(x)
  • we will have one special “in fix” predicate =, e.g. Fred=fatherOf(Marry)
    • <-> is equivalent truth values
    • = is same object
  • Note, we could have used equals(Fred, fatherOf(Marry))

Example: Marry has two sisters, Alice and Sue

  • Alice=SisterOf(Marry) ^ Sue=SisterOf(Marry) is WRONG
  • Instead we can use predicates instead of functions, sisters(Marry, Alice) ^ sisters(Marry, Sue) RIGHT
Examples                WFF (needs to have a *truth value*)

Mary                    N
motherOf(John)          N
motherOf(John, Mary)    Y
f(p(1)^q(2))            N(no connectives inside function)

English-to-FOPC

  • Everybody knows some body else:
    • V x human(x) -> Exists(y) Knows(x, y) ^ human(y) ^ x!=y
  • Every rational number is also a real number:
    • V x [rational(x) ^ number(x)] -> [real(x) ^ number(x)]
  • There is a prime number greater than 100:
    • Exists x number(x) ^ prime(x) ^ greater(x, 100)
      • Aside Exists x [p(x) -> q(x)] is same as Exists x [^p(x) v q(x)] (would be true if for some x p(x) is false)
  • There is no largest prime
    1. V x [number(x) ^ prime(x)] -> [Exists y prime(x) ^ number(y) ^ greater(y, x)]
      • ! Exists x largest_prime(x) <- assume too much in the predicate name, which limits interesting
  • Mary has a sister:
    1. sister(mary, sisterOf(mary)) // does not woole if mary has two sisters
      • Exists y [sister(mary, y) ^ person(y)]
  • Mary is the sister of John father
  • Everybody likes a dog (the same dog or a different dog or some combo?):
    • V x person(x) -> Exists y [dog(y) ^ likes(x, y)]
    • Exists y dog(y) ^ [V x person(x) -> likes(x, y)]

Unification Algorithm

  • p(John), V x p(x) -> q(x)
    • q(x) <- incorrect, too general
    • q(John) <- OK
    • Theta={x John} // a binding list
  • The unification algorithm finds the fewest constraints that make two logical expression match (i.e. char by char identical)
  • all variables are universal(i.e. “for all” variables)
A       B       Theta(binding list)
P(?x)   P(Mary) {?x/Mary}
P(?x)   P(?y)   {?x/?y} or {?y/?x}
P(?y)   P(?x)   {}
P(John) P(Mary) FAIL
P(1)    Q(1)    FAIL since pred or tuneto name
P(?x?y?z)   P(1,2)  FAIL
One Subroutine and One Data structure
Theta = binding list 
Substitute(Theta, expression) - repeatedly replace all the bound variables

subst({?x/John, ?y/Mary}, p(?x, ?y))
= p(John, Mary, ?z)

subst({?x/?y, ?y/1}, p(?x, ?y))
= p(1, 1)
Simple Way to do unification
  • make sure pred/function names match and H args is the same
  • walk through argument-by-argument
    • if can not match fail, e.g. p(sue), p(motherOf(John)) fail
    • otherwise add constraint to Theta
    • replace the bound variable by the matched term in all places (except in Theta)
    • when done, either FAILs or name two identical expression
Unify(p(?x, ?x, A), p(?z, f(?y), ?y)) Theta={?x/?z, ?z/f(?y), ?y/A} (Aside: "standardizing part" [V x p(x)] [V x q(x)])
Unify(p(?z, ?z, A), p(?z, f(?y), ?y))
Unify(p(f(?y), f(?y), A), p(f(?y), f(?y), ?y))
Unify(p(f(A), f(A), A), p(f(A), f(A), ?y))
The “Occurs Check”
  • we cannot unify ?x and f(?x)
    • consider ?x and succesorOf(?x): 无限合一，无限迭代，造成死循环

Some more Inference Rules for FOPC

  • Universal Instantiation (UI)
    • V x P(x) |- P(constant) with Theta = {x/constants}
  • Existential Instantiation (EI)
    • Exists x P(x) |- P(SkolemConstant+101) (need to generate a new constant)
    • V y Exists x P(x) |- P(skolemFunction102(?y))
  • P(?x, ?y), P(?z, ?w) -> q(?z) |- subst(unify(P(?x, ?y), P(?z, ?w)), q(?z))
    • Alternate Form: replace P(?z, ?w) -> q(?z) with ^P(?z, ?w) v q(?z)
  • Generalised Resolution Rule

    • P(?x, ?y) v alpha(?y, ?z), !P(?a, ?b), beta(?b, ?c, ?d) |- SUBST(unify(P(?x, ?y), !P(?a, ?b)), alpha(?y, ?z) v beta(?b, ?c, ?d))

        ex> P(?x) v Q(?x), !P(John) v R(John) v Z(Mary, John)
  Using Theta={?x/John}
      Q(John) v R(John) v Z(Mary, John)
  • alpha(constant) |- Exists x alpha(x)
Unique names assumption
  • different constants refer to different objects
    • so unique(P(Joe), P(Joseph)) fails even if we tell our AI logic system John=Joseph

Clausal Form (aka, CNF = Conjunctive Normal Form)

  • an algorithm exists for putting a set of WFF into this form, but all you need to know is P->Q becomes !P v Q
  • a conjunct (“AND”) of disjuncts (“OR”) where the disjuncts only contain atomic predicates or their negations

Proof by contradiction

To show alpha, we assume !alpha and show it leads to a contradiction (beta, !beta) beta v false, !beta v false |- false v false

Given:
[p(?x1) v !q(?x1)] ^ [r(?x2) v !p(?x2)] ^ [!r(John)] ^ [q(John)] ^ [a(?x3) v !b(?x3)] ^ [!a(Mary)]

Show r(John):
Theta={?x3/Mary}
[p(?x1) v !q(?x1)] ^ [r(?x2) v !p(?x2)] ^ [!r(John)] ^ [q(John)] ^ [!b(Mary)]
Theta={?x1/John}
[p(John)] ^ [r(?x2) v !p(?x2)] ^ [!r(John)] ^ [!b(Mary)]
Theta={?x2/John}
[p(John)] ^ [!p(John)] ^ [!b(Mary)]
Theta={}
[!b(Mary)]

Prolog

Prolog does resolution theorem proving, plus can call Std code like in Java.Math class such as add, subtract, etc

Negation as failure (to prove true)

If we can not prove P assume !P (not logically valid, but useful in practice)

e.g. KB: P->Q, Q->R, a->b
ASK Prolog: did I write This predicate?: No

Semidecidability

If a proof exists, resolution theorem proving will find it. But the code might not halt if Search Space is infinite

Key goal of logical reasoning

go beyond fact lookup to performing chains of inference to answer queries

Representing MOVE(x, y) in logic

  • Useful BK: V x, s {![Exists y on(y, x, s)]} -> clearTop(x, s)
  • V x, y, z, s {block(x) ^ block(y) ^ state(s) ^ clear(x, s) ^ clear(y, s) ^ x!=y ^ on(x, z, s0)} -> s1 = result(move(x, y), s1) ^ on(x, y, s1) ^ !clearTop(y, s1) ^ clearTop(z, s1)
    • si is timestamp

Frame Axioms

  • stating what is unchanged between world states
  • “Things not moved, stay where they are.” V on(z, w, s, x, y) ^ z!=x -> on(z,w, result(move(x, y, s))

Qualification Problem

Will car start? If gas in tank ^ starter works ^ bananas in tail pipe ^ (where to stop?)

Probability Logic - MLN, Markov Logic Networks

  • All WFFs have a weight (if all weights=INFINITE, MLN becomes standard logic)
    • higher the weight, the stronger the WFF

    • sum of weights of all WFFs that are true in this world state

        Prob(world state) = e / z
  ex>
  weight=2 P->Q
  weight=5 P

  P   Q   Prob in MLN Prob in Pure Logic
  F   F   e**(2+0)/z  0
  F   T   e**(2+0)/z  0
  T   F   e**(0+5)/z  0
  T   T   e**(2+5)/z  1
  where z = e**2 + e**2 + e**5 + e**7