Clausulas y resolventes

Clausulas y resolventes

1.

(A↔B)

(A→B)(B→A)

(¬AB)(¬BA)

[(¬A,B),(¬B,A)]

 R1(c1,c2)=(¬A,A)

R2(R1,c2)=(¬B,A)

R3(R2,R1)=(¬B,A)

 por lo tanto se dice que es satisfactible.

2.

{(A,¬B),(A,C),(¬B,C),(A,B),(¬C,B),(¬A,¬C)}

numero de resolventes

R1(c1,c4)=(A) R2(c1,c5)=(A,¬C) R3(c1,c6)=(¬B,¬,C) R4(c2,c5)=(A,B) R5(c2,c6)=(C,¬C) 

R6(c3,c4)=(C,A)  R7(c3,c5)=(¬B,B) R8(c3,c6)=(¬B,¬A) R9(c4,c6)=(B,¬C) R10(c5,c3)=(¬C,C)

R11(c6,c2)=(¬A,A.)