Transcript 9 - Duke University

Computability and Complexity
9-1
Logic Reminder (Cnt’d)
Computability and Complexity
Andrei Bulatov
Computability and Complexity
• Propositional logic
• Conjunctive normal forms
• Predicates, functions and quantifiers
• Terms
• Formulas
9-2
Computability and Complexity
Models (First Order Semantics)
Let  be a vocabulary. A model appropriate to  is a pair M=(U,)
consisting of
• the universe of M, a non-empty set U
• the interpretation, a function  that assigns
- to each predicate symbol P a concrete predicate P M on U
M
- to each function symbol f a concrete function f on U
• the equality predicate symbol is always assigned the equality
predicate on U
9-3
Computability and Complexity
Meaning of terms
Let t be a term and let T be an assignment of variables in t with
values from U
• if t is a variable, say, t = X, then t T is defined to be X T
• if t  f (t1 ,, tk ) then t T is defined to be f M (t1T ,  , t T )
k
9-4
Computability and Complexity
A model M and a variable assignment T satisfy a formula 
(written M, T |= ) if
• if P(t1 ,, tk ) is an atomic formula, then M,T |=  if
P M (t1T ,  , t kT )  1
• if  =  then M,T |=  if M,T | 
• if   1   2 then M,T |=  if M , T |  1 and M , T |  2
• if   1   2 then M,T |=  if M , T |  1 or M , T |  2
• if  = X  then M,T |=  if, for every u  U,
T  X  u | 
where T  X  u is the assignment that is identical to T,
except that T  X  u( X )  u
• if  = X  then M,T |=  if, there exists u  U such that
T  X  u | 
9-5
Computability and Complexity
Examples
A model of the vocabulary of graph theory is a pair G=(U,E), where
U is a set and E is a binary relation, that is a graph
A model of the vocabulary of number theory
U = N, the predicate and function symbols have their usual sense
U = Z, the predicate and function symbols have their usual sense
U = Q, the predicate and function symbols have their usual sense
U = R, the predicate and function symbols have their usual sense
U = C, the predicate and function symbols have their usual sense
U = {0,…,n-1}, the predicate symbols have their usual sense, the
function symbols are interpreted by operations modulo n
9-6
Computability and Complexity
9-7
Types of First Order Formulas
A formula  is said to be valid if M,T   for any model M and assignment T
A formula  is said to be satisfiable if M,T   for some M and T
A formula  is said to be unsatisfiable if M,T   for no M and T
valid
unsatisfiable
satisfiable
Formulas  and  are said to be equivalent,   , if they have the
same satisfying models and assignments
Computability and Complexity
Valid Formulas
Boolean tautologies
X Y ( E ( X ,Y )  E ( X ,Y ))
Equality
X ( X  1  X  1)
( X  X 2  Y )  (( Z  X  X 2 )  ( Z  Y ))
Quantifiers
P(1, X )  (Y P(Y , X ))
(Y P(Y , X ))  P(1, X )
9-8
Computability and Complexity
Models and Theories
Let  be a vocabulary.
For a sentence (set of sentences) , Mod() denotes the class of all
models satisfying 
For a model (set of models) M, Th(M) denotes the set all sentences
satisfied by M (each model from M)
It is called the elementary theory of M
If   Th(Mod(1 ,,  k )) then  is called a valid consequence of
1 ,,  k written 1 ,,  k | 
9-9
Computability and Complexity
Examples
(X ( X  X  X )) | (X ( X  X  X  X ))
(X Y (( X  Y )  (( E ( X , Y )  E (Y , X )))) |
((X 1 X 2  X n (( X 1  X 2 )  ( X 1  X 3 )    ( X n1  X n ))) 
(Y1 Y2  Yn ((Y1  Y2 )  (Y1  Y3 )    (Yn1  Yn )
 E (Y1 , Y2 )    E (Yn1 , Yn ))))
Let  be a first order description of a computer chip,
 states that a deadlock never occurs
 is the question “Can the chip be deadlocked?”
9-10
Computability and Complexity
Proof Systems
A proof system consists of
•
a set axioms 1 ,  2 ,
•
a collection of proof rules
1 ,  2 ,,  k | 
A proof is a sequence of formulas 1 ,  2 , , where every formula is
Either an axiom or obtained from preceding formulas using a rule
A theorem is any formula occurring in a proof
9-11
Computability and Complexity
Propositional Logic
Axioms:
the main tautologies
Proof rules:
• substitution
Let  and  be propositional formulas and let  | X  denote
the formula obtained from  by replacing every occurrence of
X with .
Then  |  | X  is a proof rule
• modus ponens
,  | 
Theorems:
the tautologies
9-12
Computability and Complexity
9-13
Predicate Calculus
Let  be a vocabulary with plenty of predicate and function symbols
Axioms:
AX0 Any Boolean tautology
AX1 Any expression of the following forms:
AX1a: t=t
AX1b: (t1  t '1   tk  t 'k )  ( f (t1 ,, tk )  f (t '1 ,, t 'k ))
AX1c: (t1  t '1   tk  t 'k )  ( P(t1 ,, tk )  P(t '1 ,, t 'k ))
AX2: Any expression of the form (X )   |X t
AX3: Any expression of the form   X , with X not free in 
AX4: Any expression of the form (X (  )  ((X )  (X))
Proof rules:
Theorems:
modus ponens
valid first order formulas
Computability and Complexity
Gödel’s Completeness Theorem
Theorem
Let  be a set of formulas and  a formula.
Then    if and only if   
9-14
Computability and Complexity
9-15
Resolution
Axioms:
a set of disjunctions of atomic formulas
(a set of clauses)
Proof rules:
• resolution
  (P  ),   (P  )
,  R (  )
C  (X  C), D  (X  D)
C, D R (C  D)
((  ) is called the resolvent of  and )
Computability and Complexity
Satisfiability
Satisfiability
Instance: A conjunctive normal form .
Question: Is  satisfiable?
k-Satisfiability
Instance: A conjunctive normal form  every clause of which
contains exactly k literals.
Question: Is  satisfiable?
9-16
Computability and Complexity
9-17
Theorem
A Satisfiability instance, , is unsatisfiable if and
only if  R 
Example:
(1)
(2)
(3)
(4)
(5)
X  Y , X  Z , Y  Z , X  Z , X  Y
Proof:
X  Z,
Y  Z ,
X  Y , X  Y , X  Z ,
X  X  X , X  Y ,
X  X  X,
