.dsy:it. - Letterali massimali aiuto !

.dsy:it. (http://www.dsy.it/forum/)
- Logica matematica (http://www.dsy.it/forum/forumdisplay.php?forumid=246)
-- Letterali massimali aiuto ! (http://www.dsy.it/forum/showthread.php?threadid=28728)

Posted by Gatz on 31-12-2006 17:53:

Letterali massimali aiuto !

Ciao a tutti !

Sembra proprip che io non riesca a digerire l'algoritmo per trovare i letterali massimali di una clausola...

se prendiamo ad esempio l'esercizioa pag 41 della dispensa

ordine di precedenza: f > g > P > a > b
ordinamento: LPO

clausola:

f(a)=g(a) => f(a)=f(b)

trasformando i letterali i multiinsiemi diventa:

{f(a),f(a),g(a),g(a)} per il letterale negativo
{f(a),f(b)} per il letterale positivo

cancelliamo i termini uguali dai due multiinsiemi e abiamo:

{g(a),g(a)}
{f(b)}

visto l'ordine di precedenza mi viene da controllare questo:

f(b) >LPO g(a) (ok per LPO2)
f(b)>a (ok per LPO2)

quindi secondo il mio ragionamento si dovrebbe avere:

f(a)=g(a) => f(a)=f(b)*

e invece la dispensa conclude con:

f(a)=g(a)* => f(a)=f(b)

dove sbaglio ????

grazie a tutte le persone che mi risponderanno !

ciao

Posted by m@cCo on 12-01-2007 11:56:

In effetti questa faccenda dei multiiinsiemi e dei massimali sfugge anche a me.
E poi non riesco a capire da dove tira fuori le uguaglianze...

Posted by Eruyomë on 23-01-2007 10:57:

Quando elimini i termini in comune togli dal primo due f(a) e uno solo dal secondo, dovresti togliere uno ed uno e così trovi f(a) > f(b) per LPO3

__________________
Io sono la fata verde. Sono la rovina e il rimpianto, la vergogna e il disonore. Io sono la morte, io sono l'assenzio...

Posted by m@cCo on 24-01-2007 08:47:

Originally posted by Eruyomë
Quando elimini i termini in comune togli dal primo due f(a) e uno solo dal secondo, dovresti togliere uno ed uno e così trovi f(a) > f(b) per LPO3

Ma perché devo eliminare i termini uguali? Il confronto non andrebbe fatto secondo l'ordinamento > definito per i multiinsiemi, cioè trovando n multiinsiemi M0, ..., Mn t.c. M = M0 >1 ... >1 Mn = N?

E poi ripeto, dove tira fuori le uguaglianze nelle clausole?

Una clausola della forma f(a)=g(a) -> f(a)=g(b) non l'ho mai vista sinceramente.

Posted by Drake83 on 24-01-2007 09:33:

Originally posted by m@cCo

Una clausola della forma f(a)=g(a) -> f(a)=g(b) non l'ho mai vista sinceramente.

parli di quest'anno? se è così nn le ha fatte semplicemente perchè subito pirma di farle si è fatto male e nnha spiegato superposition e compagnia bella;quindi ha spiegato risoluzioni di clausole senza uguaglianza.

__________________
"io non sono come gli altri Robin Hood, io non ballo coi lupi"
"ogni mattina come narciso si specchia nel ruscello retrovisore", "ci sono mille modi per chiamare dio...dio,allha,adta,arauffa,crisma..afjasf...tanto non ti risponde"

Corrado Guzzanti è il mio Dio.
Roberto Saviano eroe nazionale.

Posted by Eruyomë on 24-01-2007 10:18:

Originally posted by m@cCo
[B]Ma perché devo eliminare i termini uguali? Il confronto non andrebbe fatto secondo l'ordinamento > definito per i multiinsiemi, cioè trovando n multiinsiemi M0, ..., Mn t.c. M = M0 >1 ... >1 Mn = N?

Guarda io quella roba lì non l'ho mica capita ma poco più in alto c'è un'altra definizione molto più chiara e cioè:
M > N se
M = M' U (x)
N = M' U (y1....yn)
e x > di tutti gli y

Nel nostro caso quel M' è proprio f(a) allora puoi non considerarlo ai fini del confronto. Ti rimane quindi l'altro f(a) che interpreti come x e che risulta maggiore dei vari y1...yn che sono i termini rimasti del secondo multinsieme.

Credo sia giusto così, nel caso accetto consigli.

__________________
Io sono la fata verde. Sono la rovina e il rimpianto, la vergogna e il disonore. Io sono la morte, io sono l'assenzio...

Posted by m@cCo on 24-01-2007 10:48:

Originally posted by Drake83
parli di quest'anno? se è così nn le ha fatte semplicemente perchè subito pirma di farle si è fatto male e nnha spiegato superposition e compagnia bella;quindi ha spiegato risoluzioni di clausole senza uguaglianza.

Peccato che gli esempi sulla dispensa siano proprio in questa forma :asd:

A questo punto mi chiedo come possiamo trovare un letterale massimale se è necessario che le clausole siano della forma t1 = s1....tn = sn -> u1 = v1...un = sn.

@eruyome: mi son perso :asd:

Allora, consideriamo M quello più grande, ovvero M = {f(a), f(a), g(a), g(a)} e N = {f(a), f(b)}. In questo caso, se ho capito il tuo ragionamento, possiamo vedere M come M' U {x}, con M' = {f(a)} e x = {f(a)}. Ma gli altri due g(a) dove li metti?

E nel caso considerassimo M = {f(a), f(b)} e N = {f(a), f(a), g(a), g(a)}?
Allora abbiamo M' = {f(a)}, {x} = {f(b)} e quindi M = M' U {x}. Ma allora {y1, ..., yn} = {f(a), g(a), g(a)} e N = M' U {y1, ..., yn}.
Tuttavia in questo caso non vale x > y1, ..., x > yn e quindi i due letterali non sono confrontabili. Dove sbaglio?

Posted by Drake83 on 24-01-2007 11:10:

Originally posted by m@cCo
Peccato che gli esempi sulla dispensa siano proprio in questa forma
A questo punto mi chiedo come possiamo trovare un letterale massimale se è necessario che le clausole siano della forma t1 = s1....tn = sn -> u1 = v1...un = sn.

cerca tra gli esercizi di spass quelli senza identità.

Posted by m@cCo on 24-01-2007 11:31:

Originally posted by Drake83
cerca tra gli esercizi di spass quelli senza identità.

Ci sono arrivato, al posto del termine destro dell'uguaglianza si usa la costante true

Resta il dubbio per l'esempio...

In teoria io posso sostituire un qualsiasi sottoinsieme X di M (anche M stesso) con un nuovo sottoinsieme Y tale che per ogni y in Y valga x > y per qualche x in X. Quindi N = (M - X) U Y.

Riprendendo l'esempio:

M = {f(a), f(a), g(a), g(a)}
N = {f(a), f(b)}

X = {f(a), g(a), g(a)}
Y = {f(b)}

N = (M - X) U Y = ({f(a), f(a), g(a), g(a)} - {(f(a), g(a), g(a)}) U {f(b)}

Ora, se ho ben capito, basta che valga x > y, per ogni y in Y, per QUALCHE x. Ovvero basta che esista un x in X che soddisfa la condizione.
In questo caso abbiamo che f(a) > f(b) e quindi M > N.

Questo è quanto sono riuscito ad estrapolare, vi ci trovate?

Posted by Eruyomë on 24-01-2007 12:30:

Ma voi avete capito per caso il teorema di Herbrand? Io sono un po' perplito a riguardo...inoltre il simpaticastro a lezione non ha mai fatto neanche un esempio e, personalmente...non c'ho capito na' mazza!!

Oppure altra domanda: ma perché devo usare sto herbrand quando devo risolvere un problema di conseguenza logica del I ordine, non posso buttare dentro tutto a SPASS e vedere che mi dice?

__________________
Io sono la fata verde. Sono la rovina e il rimpianto, la vergogna e il disonore. Io sono la morte, io sono l'assenzio...

Posted by m@cCo on 24-01-2007 19:34:

Originally posted by Eruyomë
Ma voi avete capito per caso il teorema di Herbrand? Io sono un po' perplito a riguardo...inoltre il simpaticastro a lezione non ha mai fatto neanche un esempio e, personalmente...non c'ho capito na' mazza!!

Oppure altra domanda: ma perché devo usare sto herbrand quando devo risolvere un problema di conseguenza logica del I ordine, non posso buttare dentro tutto a SPASS e vedere che mi dice?

Io sinceramente il teorma di Herbrandt ( ma non ci sono pure delle algebre di sto tizio? O forse mi confondo con Heyting o quel che sia :asd:

) l'ho sentito nominare durante le lezioni solo riguardo all'infinità delle istanziazioni possibili per i termini di un linguaggio. Da qui a saperlo però...

Posted by Eruyomë on 27-01-2007 12:38:

Stavo studiando sulle slide di ranise ma:

lezione 3 lucido 90:
"se un'istanza chiusa di fi è soddisfacibile allora fi è soddisfacibile ed il metodo termina"

lezione 3 lucido 91 (quello dopo...ma subito dopo!)
"il metodo termina se la formula di input è insoddisfacibile"

Cioè...ehm...allora..cechiamo di capirci....mi prende in giro.....è evidente che c'è qualcosa che non va........ma come diavolo funziona sta roba inutile e offensiva!!

Scusate ma non ce la faccio più a far ste robe; forse un lucido si riferisce alla forumula originale e l'altro alla formula refutata? E' l'unica spiegazione che mi do...ma non c'è scritto da nessuna parte.

Ciao.

__________________
Io sono la fata verde. Sono la rovina e il rimpianto, la vergogna e il disonore. Io sono la morte, io sono l'assenzio...

Posted by Drake83 on 27-01-2007 12:59:

Originally posted by Eruyomë
Stavo studiando sulle slide di ranise ma:

lezione 3 lucido 90:
"se un'istanza chiusa di fi è soddisfacibile allora fi è soddisfacibile ed il metodo termina"

lezione 3 lucido 91 (quello dopo...ma subito dopo!)
"il metodo termina se la formula di input è insoddisfacibile"

Cioè...ehm...allora..cechiamo di capirci....mi prende in giro.....è evidente che c'è qualcosa che non va........ma come diavolo funziona sta roba inutile e offensiva!!

Scusate ma non ce la faccio più a far ste robe; forse un lucido si riferisce alla forumula originale e l'altro alla formula refutata? E' l'unica spiegazione che mi do...ma non c'è scritto da nessuna parte.

Ciao.

effettivamente.... :asd:

Posted by m@cCo on 28-01-2007 19:47:

Originally posted by Eruyomë
Stavo studiando sulle slide di ranise ma:

lezione 3 lucido 90:
"se un'istanza chiusa di fi è soddisfacibile allora fi è soddisfacibile ed il metodo termina"

lezione 3 lucido 91 (quello dopo...ma subito dopo!)
"il metodo termina se la formula di input è insoddisfacibile"

Cioè...ehm...allora..cechiamo di capirci....mi prende in giro.....è evidente che c'è qualcosa che non va........ma come diavolo funziona sta roba inutile e offensiva!!

Scusate ma non ce la faccio più a far ste robe; forse un lucido si riferisce alla forumula originale e l'altro alla formula refutata? E' l'unica spiegazione che mi do...ma non c'è scritto da nessuna parte.

Ciao.

Logica: ovvero come complicarsi la vita cercando di renderla più semplice :asd:

Comunque ho appena guardato le videolezioni sul famigerato Herbrand ed ecco quanto ho capito.

Dato che la logica del I ordine è indecidibile non potrò mai sapere se una teoria è consistente. Si cerca allora di ragionare dualmente, ovvero cercando di dimostrare l'incosistenza della teoria.
E, dato che se una teoria PHI |= phi allora PHI U {¬phi} è inconsistente, devo trovare il modo di verificare questa inconsistenza.

Ora, tentare di dimostrare l'inconsistenza di una teoria significa trovare almeno un modello in cui tale teoria non è vera, ovvero almeno una struttura in cui la teoria non è vera.
E che c'azzecca Herbrand qui dentro?

Ecco, il signor Herbrand (che a quanto pare è pure morto a 25 anni, che culo), ha detto una cosa molto semplice: guardate che invece di sbattervi a tentare di generare tutte le strutture che soddisfano gli assiomi della vostra teoria, basta che generate le mie, che sono più semplici da trattare e sono anche di meno, tiè.

Per i dettagli vi rimando alle note ed alle slide, dato che devo ancora "interiorizzare" il tutto :asd:

In pratica alla fin fine si può ridurre l'insoddisfacibilità (ovvero l'inconsistenza) di una teoria ad un "semplice" problema di soddisfacibilità booleana, trattando le formule in un certo modo e istanziandole per tutti i termini dell'universo di Herbrand. Ovviamente essendo la formula che vogliamo essere soddisfatta della forma:

VX1,..., Xn phi

Se generiamo tutte le sue istanziazioni per una data struttura (in questo caso quella di Herbrand) e ricaviamo che sono tutte vere, allora anche la formula di partenza sarà per forza di cose vera.

Mah! :asd:

Posted by Drake83 on 29-01-2007 15:14:

è allucinante logica :asd: ma mica chiederà tutta la caterba di dimostrazioni che ci sn nelle note vero ? no xkè sn la morte....

All times are GMT. The time now is 04:54.

Show all 15 posts from this thread on one page