 | |
Il progetto dsy.it è l'unofficial support site dei corsi di laurea del Dipartimento di Scienze dell'Informazione e del Dipartimento di Informatica e Comunicazione della Statale di Milano. E' un servizio degli studenti per gli studenti, curato in modo no-profit da un gruppo di essi. I nostri servizi comprendono aree di discussione per ogni Corso di Laurea, un'area download per lo scambio file, una raccolta di link e un motore di ricerca, il supporto agli studenti lavoratori, il forum hosting per Professori e studenti, i blog, e molto altro...
In questa sezione è indicizzato in textonly il contenuto del nostro forum |
Letterali massimali aiuto !
Clicca QUI per vedere il messaggio nel forum |
| Gatz |
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 |
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ë |
| 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 |
| m@cCo |
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. |
| Drake83 |
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. |
| Eruyomë |
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. |
| m@cCo |
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? |
| Drake83 |
Originally posted by m@cCo
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.
cerca tra gli esercizi di spass quelli senza identità. |
| m@cCo |
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 :D
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ë |
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? |
| m@cCo |
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ò...:D |
| 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. |
| Drake83 |
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: |
| m@cCo |
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? :D
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: |
| Drake83 |
| è allucinante logica :asd: ma mica chiederà tutta la caterba di dimostrazioni che ci sn nelle note vero ? no xkè sn la morte.... |
|
|
|
|
