bluone

Desperados

User info:

Registered: Jan 2007
Posts: 14 (0.00 al dì)
Location:
Corso: TICOM
Anno: 1
Time Online: 8:43:32 [...]
Status: Offline

Post actions:

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

pusio

User info:

Registered: Apr 2005
Posts: 73 (0.01 al dì)
Location: milano
Corso: Ticom
Anno: primo
Time Online: 1 Day, 15:45:38 [...]
Status: Offline

Post actions:

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

User info:

Registered: Apr 2005
Posts: 73 (0.01 al dì)
Location: milano
Corso: Ticom
Anno: primo
Time Online: 1 Day, 15:45:38 [...]
Status: Offline

Post actions:

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

Desperados

User info:

Registered: Jan 2007
Posts: 14 (0.00 al dì)
Location:
Corso: TICOM
Anno: 1
Time Online: 8:43:32 [...]
Status: Offline

Post actions:

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