.dsy:it. (http://www.dsy.it/forum/)
- Logica matematica (http://www.dsy.it/forum/forumdisplay.php?forumid=246)
-- Creazione di clausule (http://www.dsy.it/forum/showthread.php?threadid=35557)

Creazione di clausule

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

__________________
Un giorno le macchine riusciranno a risolvere tutti i problemi, ma mai nessuna di esse potrà porne uno

Allora per quanto ricordo(ho dato l'esame a febbraio) per a rivare a ciò a cui arriva spass vengon fatte tutte quelle operazioni che riguardano fnn, fnc, skolemizzazione ecc....Dopo di questo viene fatto tutto con il teorema di Herbrant ...Mi dispiace ma nn ho + i miei libri e appunti sotto mano....riprovo con calma

se vuoi 1 mano concreta io l'es te lo faccio..ma dovrei avere almeno qualche parentesi in + per capire la precedenza degli operatori...

V(b) → ((V(a) ∧ B(b) ∧ B(c)) ∨ (V(b) ∧ B(a) ∧ B(c)) ∨ (V(c) ∧ B(b) ∧ B(a)))


Ecco le parentesi sono cosi

__________________
Un giorno le macchine riusciranno a risolvere tutti i problemi, ma mai nessuna di esse potrà porne uno