.dsy:it. - Creazione di clausule

.dsy:it.
//www.dsy.it

Creazione di clausule

Posted by bluone on 26-06-2008 10:39

Ciao a tutti, ho un grosso problema. Ho la conjecture di cui sotto e devo trasformarla in una serie di clausule; ho provato in tutti i modi ma non riesco ad arrivare alla soluzione di SPASS

V(b)_→_V(a)_∧_B(b)_∧_B(c)_∨_V(b)_∧_B(a)_∧_B(c)_∨_V(c)_∧_B(b)_∧_B(a)

Per SPASS da questa conjecture dovrebbero scaturire le seguenti clausule

|| V(b) -> V(c) B(c)*.
|| V(b) -> B(b)* B(c).
|| V(b) -> B(a)* B(c).
|| V(b) -> B(a)* B(b).
|| V(b) -> B(a)* V(a)

Se qualcuno per caso sa come fare ad arrivarci e mi può postare i passaggi gli sarei molto grato.

Grazie