Calcolo della forma a clausole di una formula ben formata

[Luke35]

Ciao a tutti!

Ho la seguente formula ben formata:
$ ((!=A rArr B) rArr C) rArr ((C ^^ != B) rArr (C rArr A)) $

e devo calcolarne la forma a clausole.

Eliminando l'operatore $rArr$ secondo l'equivalenza fondamentale $A rArr B -= !=A vv B$ ottengo la seguente:

$ (!=(!=A ^^ !=B) ^^ !=C) vv ((!=C vv B) vv (!=C vv A)) $

Ora ,sapendo che una clausola è la disgiunzione finita di letterali, ho sempre proceduto (in altri esercizi) in modo da ottenere l'AND di sottoformule del tipo:

$ (A vv B vv C ) ^^ (D vv E vv F)$

Ottenendo così le clausole: $ c1={A,B,C} c2={D,E,F} $
In questo caso però per poter ottenenere la stessa forma devo togliere fuori l'operatore not posto davanti alle clausole. Per spiegarmi meglio posto di seguito la formula equivalente che ottengo per la forma a clausole:

$ !=( (!=A vv C) ^^ (!=B vv C) ^^ !=(!=C vv B) ^^ !=(!=C vv A) ) $

Ma in questo modo ho degli operatori davanti alle sottoformule e non riesco a capire se il procedimento è giusto o no.

Qualcuno può aiutarmi?

[j18eos]

Prima di [tex]\neq[/tex] cosa ci manca?

[Luke35]

"j18eos":Prima di [tex]\neq[/tex] cosa ci manca?

..oops..avevo diemnticato una parentesi...ora è corretta..