CS 486, Spring ’01

March 8, 2001

5 questions

Quiz 5

 

 

  1. If a denumerable set of formulas S is unsatisfiable, then a finite subset of S is unsatisfiable.

true

false

 

 

 
  1. The block tableau node {Tp1, Tp2, Fp3, Fp1,} is equivalent to the sequent p1, p2, p3 ½¾  p1.

true

false

 

 

 
  1. Which is a correct definition of ~A?  Circle all correct definitions.

i.       AÉ~A

ii.     AÉ^

iii.            AÉ(A&~A)

 

 

 

 

 
  1. What is the correct result of substituting (pÙq) for q in "p.(pÉ(qÉp))?  Circle all correct answers.

i.          "p.(pÉ((pÙq)Ép))

ii.        "r.(rÉ((pÙq)Ér))

iii.       "q.(qÉ((pÙq)Éq))

iv.       "q.(qÉ((qÙq)Éq))

 

 

 

 

 
  1. In Refinement Logic the rule for H ½¾  P Ú Q splits into two separate rules, one with subgoal H ½¾  P and the other with subgoal
    H     ½¾  Q.

true

false