Soddisfacibiltà formula
Avendo la seguente formula:
$not(A(x)->B(x))^^AAyB(y)$
devo vedere se è soddisfacibile,il problema è che non sò come trattare i quantificatori $AA$ e $EE$,qualcuno mi potrebbe dire quali regole devo utilizzare?
$not(A(x)->B(x))^^AAyB(y)$
devo vedere se è soddisfacibile,il problema è che non sò come trattare i quantificatori $AA$ e $EE$,qualcuno mi potrebbe dire quali regole devo utilizzare?
Risposte
"Uhm". Metto con riserva di verificare fesserie, ma per essere soddisfacibile $forall y B(y)$ deve esserlo, pertanto $B(x)$ deve essere soddisfatto ogni volta che la formula è soddisfacibile.
E' possibile che possa togliere i quantificatori se non compaiono variabili libere nel loro dominio?
Se fosse vero dalla mia formula scompare il $AAy$,e diverebbe così:
$not(A(x)->B(x))^^B(y)$
ora per essere risolubile deve risultare $A(x)=1$,$B(x)=0$ e $B(y)=1$.
Però ancora non ho capito bene come trattare i quantificatori,e questo è un problema quando mi trovo ad affrontare formule più lunghe e complesse...
Se fosse vero dalla mia formula scompare il $AAy$,e diverebbe così:
$not(A(x)->B(x))^^B(y)$
ora per essere risolubile deve risultare $A(x)=1$,$B(x)=0$ e $B(y)=1$.
Però ancora non ho capito bene come trattare i quantificatori,e questo è un problema quando mi trovo ad affrontare formule più lunghe e complesse...
Accedi a tutti gli appunti
Tutor AI: studia meglio e in meno tempo