Creazione di clausule
Clicca QUI per vedere il messaggio nel forum |
| bluone |
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 |
| pusio |
| 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 ;) |
| pusio |
| se vuoi 1 mano concreta io l'es te lo faccio..ma dovrei avere almeno qualche parentesi in + per capire la precedenza degli operatori... |
| bluone |
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 |
|
|
|
