Tableaux y resolucion

    tableaux y resolución

Resolver por tableaux

C,  A => (C => B  )  I=  A => B

                                     C

                           A => (C => B  )
                               A => B
                          -A v (C => B  )

                                   ^
                   -A                       C => B  
                     ^                           ^
                A  v  -B                C             B
                      ^                     +         A  v  -B
               A         -B                              ^
                +          _                        A         -B
                                                      _             +



Resolver por  resolución

A <==> B

(A => B)  v  (B => A)
(-A v B) v (-B v A)

(-A,B)   (-B,A)

P1 = (-A,B)
P2=  (-B,A)

R1 (c1,c2 )= (B,-B)
R2 (c2,c1 )= (A,-A)
R3 (R1,c1 ) = (-A,B )
R4 (R2,c2 ) = (-B,A )

Ya no esta en a condición dado que no se cumple.