Math 470 Spring Õ05

HW #4 Solutions

 

 

Section 1.8

5. a) CNF:  (¯A v C v D) ^ (¯B v C v D)

   Clausal Form: {{¯A, C, D} , {¯B, C, D}}

    b) CNF: ( ¯A v ¯B v C)

  Clausal Form: { { ¯A, ¯B, C}}

   c) CNF: ( ¯A v ¯B) ^ (¯B )  ^ (¯C) ^  (¯A v ¯C)

Clausal Form: {{ ¯A, ¯B}, {¯B}, {¯C}, {¯A, ¯C}}

 

6. a)  satisfiable :  A false, B  true

    b) not satisfiable: The 1st clause says A must be false.  The 2nd  clause then makes B false.  But the 3rd  clause requires B to be true.

    c) not satisfiable, since it contains the empty clause.

    d) not satisfiable, since it contains the empty clause.

 

7. a) {A, ¯A} and {B, ¯B}.

    b) {A, C, D}

 

8.  a) The given clauses and {A}, {¯B}, {B}, the empty clause.

     b) The given clauses only.

 

9.

1.  {B, C}

2. {¯B}

3.  {C} res 1,2

4.  {B, ¯C}

5.  {¯C} res 2, 3

6. { }   res 3, 5

 

10.  a) CNF: (¯A v ¯B v C) ^ (A v B) ^ (A v ¯C) ^ (¯A v B) ^ (A v ¯B) ^ (¯A v ¯C) ^ (A v C)

Clauses: {{¯A, ¯B, C}, {A, B}, {A, ¯C}, {¯A, B}, {A, ¯B}, {¯A, ¯C} , {A, C}}

Resolution refutation:

1. {A, ¯C}

2.  {¯A, ¯C}

3. {¯C}  res 1, 2

4. { ¯A, ¯B, C}

5.  {A, ¯B}

6.  {¯B, C} res  4, 5

7.  {A, B}

8. {¯A, B}

9. {B}   res 7,8

10. {C} res 6, 9

11. { }  res 3, 10

 

b)  CNF: ((A->B) -> ¯B) ^ B —  (¯(A->B) v ¯B)  ^  B — ((A ^ ¯B) v ¯B)) ^ B  — (Av ¯B) ^ (¯B v ¯B) ^ B — (A v ¯B) ^ ¯B ^  B

Clausal:  { {A, ¯B}, {¯B}, {B}}

Resolution refutation:

1. {¯B}

2. {B}

3. {} res 1, 2

 

11. a)  F(¯ (p v q) -> (¯p ^ ¯q))

                    T ¯(p v q)

                     F (¯p ^ ¯q)

                     F (p v q)

                      Fp

                     F q

                   /       \

               F ¯p     F ¯q

                Tp        Tq

                  X         X

      b) ¯a  —  ¯(p v q)  ^ ¯(¯p ^ ¯q) — ¯p ^ ¯q ^ (¯¯p v ¯¯q) — ¯p ^ ¯q ^ ( p v q)

    Clauses:  { {¯p}, {¯q}, {p, q} }

Resolution proof of a:

  1. {p, q}
  2. {¯q}
  3. {p} res 1, 2
  4. {¯p}
  5. { }  res 3, 4.

 

12. a) F(¯r v(p^q) -> ((r-> p ) ^ (r ->q)))

                T (¯r v( p ^ q))

                 F (r -> p) ^ (r -> q)

                  /               \

                T ¯r           T (p ^ q)

              /       \                /            \

        F(r->p)  F(r->q)    F(r ->p)   F(r->q)

           Tr         Tr            Tr            Tr

            Fp        Fq           Fp            Fq

             X         X           Tp            Tp

                                       Tq            Tq

                                         X             X

b) ¯b — (¯r v(p ^q) ^ ¯((r->p) ^ (r-> q)) —  (¯r v p) ^ (¯r v q) ^ (¯(r->p) v ¯(r ->q)) — (¯r vp ) ^ (¯r v q) ^ ((r ^ ¯p) v ( r ^ ¯q)) — (¯r v p) ^ (¯r v q)  ^ (r v r ) ^ ( r v ¯p) ^ (r v ¯q) ^ (¯p v ¯q)

Clausal:  {{¯r, p}, {¯r, q}, {r}, {r, ¯p}, {r, ¯q}, {¯p, ¯q}}

Resolution proof of b:

1.      {¯r, p}

2.       {r}

3.        {p}  res 1, 2

4.        {¯r, q}

5.         {q }   res 2, 4

6.      {¯p, ¯q}

7.      {¯p}  res 5, 6

8.      {}   res 3, 7