 | |
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 |
Dubbio ricerca dimostrazione/contromodello
Clicca QUI per vedere il messaggio nel forum |
| - Marte - |
aiuto, ho un dubbio che magari qualcuno sa dissipare riguardo l'applicazione delle regole (and, or, esiste, per ogni) nella ricerca di dimostrazione/contromodello.
per la precisione quando applico la terza regola [esiste] sostituisco una costante nuova alla variabile vincolata.
poi, dopo uno o più passaggi, se applico la quarta regola [per ogni] alla stessa variabile a cui ho precedentemente sostituito con una costante (con la regola dell'esiste) devo per forza sostituirla con la stessa costante o basta un qualsiasi termine ground?
ciao! |
| lordghost |
Per esempio:
ExPx, ExTx, VxRx, VyQy
Le due regole di Esiste creano x/a e x/b
Pa, Tb, *
Dopo il VxRx istanzia per x per i due termini a e b
Pa, Tb, Ra, Rb, *
Infine VyQy istanzia per y anche lui gli stessi termini del precedente PerOgniX
Pa, Tb, Ra, Rb, Qa, Qb
Il fatto che l'esiste crei la nuova costante sulla variabile x non limita a y di usarle poichè ormai a e b esistono nel dominio della struttura.
Già che ci sono espongo un quesito:
VxP(f(x)), -P(f(a)).
Continua a creare nuove costante f(f(f...))) ed in alcuni temi d'esami passati mi hanno dato qualche problema a risolverli, qualcuno sa dirmi qual'è il trucco per capire il funzionamento di questo genere di esercizi? (è un esercizio di dimostrazione). |
| - Marte - |
Il fatto che l'esiste crei la nuova costante sulla variabile x non limita a y di usarle poichè ormai a e b esistono nel dominio della struttura.
Grazie mille, era come pensavo ma il dubbio va assassinato in compagnia.
Già che ci sono espongo un quesito: VxP(f(x)), -P(f(a)). Continua a creare nuove costante f(f(f...))) ed in alcuni temi d'esami passati mi hanno dato qualche problema a risolverli, qualcuno sa dirmi qual'è il trucco per capire il funzionamento di questo genere di esercizi? (è un esercizio di dimostrazione).
Non diventa un esercizio di contromodello perchè non chiude?
concludendo con
D={a, f(a), f²(a), f³(a),...... fⁿ(a)......}
e
I(P)={a} |
| - Marte - |
scusa
D={f(a), f²(a), f³(a),...... fⁿ(a)......}
I(P)={f(a)}
? |
| Deckard |
Originally posted by lordghost
Già che ci sono espongo un quesito:
VxP(f(x)), -P(f(a)).
Continua a creare nuove costante f(f(f...))) ed in alcuni temi d'esami passati mi hanno dato qualche problema a risolverli, qualcuno sa dirmi qual'è il trucco per capire il funzionamento di questo genere di esercizi? (è un esercizio di dimostrazione).
Scusa perché dovrebbe crearti nuove costanti?
VxP(f(x)), ~P(f(a)) lo trasformi in P(f(a)), ~P(f(a)), VxP(f(x)) e hai già chiuso. Il "per ogni" non ti crea nuove costanti. |
| lordghost |
No vabè non prendere alla lettere l'esempio che era solo indicativo, io mi riferivo esattamente al tema d'esame del 25 settembre 2008 1.1 che è indicato come ricerca di dimostrazione.
lo trovi qui a pagina 7 del pdf http://homes.dsi.unimi.it/~logica/d...giu08-feb09.pdf |
| lordghost |
Originally posted by Deckard
Scusa perché dovrebbe crearti nuove costanti?
VxP(f(x)), ~P(f(a)) lo trasformi in P(f(a)), ~P(f(a)), VxP(f(x)) e hai già chiuso. Il "per ogni" non ti crea nuove costanti.
E no! Non hai istanziato f(a), che è anch'esso una costante:
P(f(a)), ~P(f(a)), VxP(f(x)), P(f(f(a) )).
Il che porta il per ogni ad attivarsi ancora sul f(f(a))) creando di nuovo un nuovo P(f(f(f(a)))) che attiva il per ogni.... e così via. Non si esaurisce mai. |
| Deckard |
Originally posted by lordghost
E no! Non hai istanziato f(a), che è anch'esso una costante:
P(f(a)), ~P(f(a)), VxP(f(x)), P(f(f(a) )).
Il che porta il per ogni ad attivarsi ancora sul f(f(a))) creando di nuovo un nuovo P(f(f(f(a)))) che attiva il per ogni.... e così via. Non si esaurisce mai.
Ma non li devi fare tutti!! Li fai tutti nel caso non trovi una contraddizione: se c'è P(f(a)), ~P(f(a)) non c'è bisogno di continuare, ti devi fermare e il ramo è chiuso. |
| lordghost |
| Ok nell'esempio va bene, hai ragione che non devo continuare. Ma nel caso di una dimostrazione? Come nell'esercizio che ho linkato? |
| Deckard |
Originally posted by lordghost
Ok nell'esempio va bene, hai ragione che non devo continuare. Ma nel caso di una dimostrazione? Come nell'esercizio che ho linkato?
L'esempio era una dimostrazione, visto che termina. Non può essere una ricerca di contromodello.
Comunque non avendo svolto l'esercizio che hai linkato non posso dirti granché, ma guardandolo ad occhio non dovrebbero esserci casi che ti creano nuove costanti, visto che l'esiste non c'è, quindi ti basta rieseguire il "per ogni" finché non trovi una contraddizione. |
| - Marte - |
No vabè non prendere alla lettere l'esempio che era solo indicativo, io mi riferivo esattamente al tema d'esame del 25 settembre 2008 1.1 che è indicato come ricerca di dimostrazione. lo trovi qui a pagina 7 del pdf http://homes.dsi.unimi.it/~logica/d...giu08-feb09.pdf
Ho provato a farlo e mi risulta che non chiuda (unsat).
con
D={a, f(a), f²(a), f³(a),...... fⁿ(a)......
b, f(b), f²(b), f³(b),...... fⁿ(b)......}
e
I(R)={(a, f(b)), (f(a),b)} |
| - Marte - |
Non ho capito la differenza tra modello e contromodello a livello pratico...
Nella ricerca di contromodello si nega A, si cerca il ramo che non chiude e se ne descrive D e I.
E nella ricerca di modello? Non si nega e si cerca il ramo che non chiude? :? non so
Qualcuno sa?
grazie |
|
|
|
|
