Gatz

.amico.

User info:

Registered: Oct 2005
Posts: 37 (0.01 al dì)
Location:
Corso:
Anno:
Time Online: 13:00:37 [...]
Status: Offline

Post actions:

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

m@cCo

Steek Huzzee

User info:

Registered: Sep 2003
Posts: 936 (0.12 al dì)
Location: Trecate - Novara - Piedmont - Italy
Corso: Computer Science (magistrale)
Anno: II
Time Online: 9 Days, 0:20:33 [...]
Status: Offline

Post actions:

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...

Eruyomë

Duca di Elchingen

User info:

Registered: Feb 2003
Posts: 147 (0.02 al dì)
Location:
Corso: Informatica
Anno: II^ Magistrale
Time Online: 3 Days, 1:27:46 [...]
Status: Offline

Post actions:

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...

m@cCo

Steek Huzzee

User info:

Registered: Sep 2003
Posts: 936 (0.12 al dì)
Location: Trecate - Novara - Piedmont - Italy
Corso: Computer Science (magistrale)
Anno: II
Time Online: 9 Days, 0:20:33 [...]
Status: Offline

Post actions:

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

Drake83

Fan di Splinter

User info:

Registered: Nov 2003
Posts: 1631 (0.21 al dì)
Location: Garbagnate milanese
Corso: Tutto finito
Anno:
Time Online: 108 Days, 5:46:38 [...]
Status: Offline

Post actions:

Originally posted by m@cCo

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

__________________
"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.

Eruyomë

Duca di Elchingen

User info:

Registered: Feb 2003
Posts: 147 (0.02 al dì)
Location:
Corso: Informatica
Anno: II^ Magistrale
Time Online: 3 Days, 1:27:46 [...]
Status: Offline

Post actions:

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?

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

m@cCo

Steek Huzzee

User info:

Registered: Sep 2003
Posts: 936 (0.12 al dì)
Location: Trecate - Novara - Piedmont - Italy
Corso: Computer Science (magistrale)
Anno: II
Time Online: 9 Days, 0:20:33 [...]
Status: Offline

Post actions:

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
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

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?

Drake83

Fan di Splinter

User info:

Registered: Nov 2003
Posts: 1631 (0.21 al dì)
Location: Garbagnate milanese
Corso: Tutto finito
Anno:
Time Online: 108 Days, 5:46:38 [...]
Status: Offline

Post actions:

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.

__________________
"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.

m@cCo

Steek Huzzee

User info:

Registered: Sep 2003
Posts: 936 (0.12 al dì)
Location: Trecate - Novara - Piedmont - Italy
Corso: Computer Science (magistrale)
Anno: II
Time Online: 9 Days, 0:20:33 [...]
Status: Offline

Post actions:

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?

Eruyomë

Duca di Elchingen

User info:

Registered: Feb 2003
Posts: 147 (0.02 al dì)
Location:
Corso: Informatica
Anno: II^ Magistrale
Time Online: 3 Days, 1:27:46 [...]
Status: Offline

Post actions:

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...

m@cCo

Steek Huzzee

User info:

Registered: Sep 2003
Posts: 936 (0.12 al dì)
Location: Trecate - Novara - Piedmont - Italy
Corso: Computer Science (magistrale)
Anno: II
Time Online: 9 Days, 0:20:33 [...]
Status: Offline

Post actions:

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 ) 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ò...

Eruyomë

Duca di Elchingen

User info:

Registered: Feb 2003
Posts: 147 (0.02 al dì)
Location:
Corso: Informatica
Anno: II^ Magistrale
Time Online: 3 Days, 1:27:46 [...]
Status: Offline

Post actions:

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...

Drake83

Fan di Splinter

User info:

Registered: Nov 2003
Posts: 1631 (0.21 al dì)
Location: Garbagnate milanese
Corso: Tutto finito
Anno:
Time Online: 108 Days, 5:46:38 [...]
Status: Offline

Post actions:

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....

__________________
"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.

m@cCo

Steek Huzzee

User info:

Registered: Sep 2003
Posts: 936 (0.12 al dì)
Location: Trecate - Novara - Piedmont - Italy
Corso: Computer Science (magistrale)
Anno: II
Time Online: 9 Days, 0:20:33 [...]
Status: Offline

Post actions:

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

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

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!

Drake83

Fan di Splinter

User info:

Registered: Nov 2003
Posts: 1631 (0.21 al dì)
Location: Garbagnate milanese
Corso: Tutto finito
Anno:
Time Online: 108 Days, 5:46:38 [...]
Status: Offline

Post actions:

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

__________________
"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.