Mar 25 Giugno, 11:29:56 - 2019

Autore Topic: Linguaggi del primo ordine, chiarimenti  (Letto 1914 volte)

0 Utenti e 1 Visitatore stanno visualizzando questo topic.

Offline Rattilus

  • Direttore di Dipartimento
  • ***
  • Post: 1242
  • FeedBack: +53/-12
  • Se puoi sognarlo puoi farlo
    • Mostra profilo
Linguaggi del primo ordine, chiarimenti
« il: Ven 30 Novembre, 21:50:56 - 2007 »
Allora lunedì c'è l'esame... e fin quì ci siamo :asd:
Nei compiti passati ho visto che la domanda che capita più spesso, escludendo quelle di traduzione in linguaggio che non ci darà,  è: data una formula verificare che sia soddisfacibile e trovare un modello.
Il tutor ci ha detto di provare subito a cercare un modello perchè se lo troviamo allora è SAT.
Però chiede di verificare che sia SAT e POI trovare un modello.
Quindi va sviluppato il tableaux usando le varie regole e facendo la skolemizzazione fino a che mi trovo che all'infinito posso portare avanti un ramo. A quel punto dico che la formula è SAT.
Se ora costruisco un modello devo però tener conto delle interpretazioni delle costanti e magari delle funzioni mentre se io lo costruivo fin dall'inizio tutte queste complicazioni non c'erano. Voi come fareste?

Volevo poi scrivere le regole principali di sostituzione per vedere se ho capito bene oppure se vanno corrette:

\gamma rule : se ho \forall x all'inizio della formula sostituisco ogni x con delle variabili d1, d2, d2...

\delta rule:  ho \exists x all'inizio della frase:
Caso1: nella formula compaiono già delle variabili d1, d2, d2... sostituisco x con una funzione che ha per argomento QUELLA variabile.
Caso2: nella formula NON compaiono delle variabili d1, d2, d2... sostituisco x con COSTANTI c1, c2, c2...

___________________

Le assegnazioni vanno fatte solo per le variabili libere.
Posso sempre sostituire delle variabili (d) con delle costanti (c)
« Ultima modifica: Ven 30 Novembre, 21:59:37 - 2007 da Rattilus »
Amministratore di Soloingegneria
Se tu hai una mela, e io ho una mela, e ce le scambiamo, allora tu ed io abbiamo sempre una mela per uno. Ma se tu hai un'idea, ed io ho un'idea, e ce le scambiamo, allora abbiamo entrambi due idee.

Offline Alexander

  • Studente di Dottorato
  • ***
  • Post: 239
  • FeedBack: +17/-7
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #1 il: Ven 30 Novembre, 22:42:39 - 2007 »
ciao, le regole di skolemizzazione mi sembrano corrette.. :sisi:
Ho lo stesso tuo dubbio, riguardo l'inclusione o meno delle costanti/funzioni di Skolem nella creazione di un modello..
A prescindere da questo però, da quanto ho capito costruire un tableau del primo ordine ed espanderlo potrebbe servirci solo nel caso in cui risulterebbe CHIUSO.
Solo in quel caso possiamo dire ke la formula sia una contraddizione, altrimenti nn si può dire niente.
Questo perchè nn siamo in grado di dire se ha qualke ramo aperto o no, al contrario di quanto capita nel linguaggio proposizionale...
Io personalmente faccio prima il tableau diretto della formula, giusto per vedere se è una contraddizione...se nn mi chiude provo a trovare un modello a occhio, come faceva il tutor...:asd:
.:: Ad Astra Per Aspera ::.

Offline Artax

  • Global Moderator
  • Direttore di Dipartimento
  • *****
  • Post: 1778
  • FeedBack: +132/-55
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #2 il: Ven 30 Novembre, 22:54:09 - 2007 »
Io provo direttamente un modello a Occhio....
Almeno a quelle immediate..
http://artax87.iobloggo.com/

A computer language is not just a way of getting a computer to perform operations but rather that it is a novel formal medium for expressing ideas about methodology. Thus, programs must be written for people to read, and only incidentally for machines to execute.

Offline Rattilus

  • Direttore di Dipartimento
  • ***
  • Post: 1242
  • FeedBack: +53/-12
  • Se puoi sognarlo puoi farlo
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #3 il: Ven 30 Novembre, 23:02:59 - 2007 »
Citazione
Io personalmente faccio prima il tableau diretto della formula, giusto per vedere se è una contraddizione...
Quindi non tieni conto dei per ogni e degli esiste davanti a tutto e la tratti come se fosse proposizionale? Quindi non applichi skolem?
Amministratore di Soloingegneria
Se tu hai una mela, e io ho una mela, e ce le scambiamo, allora tu ed io abbiamo sempre una mela per uno. Ma se tu hai un'idea, ed io ho un'idea, e ce le scambiamo, allora abbiamo entrambi due idee.

Offline defrenz

  • Direttore di Dipartimento
  • ***
  • Post: 1346
  • FeedBack: +35/-82
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #4 il: Ven 30 Novembre, 23:08:56 - 2007 »
il fatto stesso di trovare un modello dimostra che sia SAT, quindi trovando un modello te lo dimostri :D

le regole sembrano giuste, ma attenzione per la delta, che anche la funzione cambia ogni volta ed in + gli argomenti possono essere anche + di una d ;)

Offline Alexander

  • Studente di Dottorato
  • ***
  • Post: 239
  • FeedBack: +17/-7
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #5 il: Ven 30 Novembre, 23:11:53 - 2007 »
Infatti nn capisco l'utilità del tableau del primo ordine, se la tipologia di esercizi ke ci capiterà si restringe a verificare solo la soddisfacibilità di una formula...  :-\
Tralasciando ke la maggior parte delle formule sono abbastanza banali...
Resta il fatto ke effettivamente nn ci hanno spiegato un metodo rigoroso col quale affrontare un esercizio del genere..
se avessero dedicato + tempo a questi argomenti ( invece di perdere ore sull'induzione ) magari avremmo capito qualcosa..
cmq penso sia meglio costruire un modello a occhio e verificarlo, piuttosto ke espandere alberi e fare skolemizzazioni infinite... ;D
.:: Ad Astra Per Aspera ::.

Offline defrenz

  • Direttore di Dipartimento
  • ***
  • Post: 1346
  • FeedBack: +35/-82
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #6 il: Ven 30 Novembre, 23:13:33 - 2007 »
beh, se ti chiedono "verifica che questa formula è valida(tautologia) o contraddittoria" allora devi per forza usare il tableau :P

Offline Alexander

  • Studente di Dottorato
  • ***
  • Post: 239
  • FeedBack: +17/-7
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #7 il: Ven 30 Novembre, 23:18:30 - 2007 »
certo...sulla validità d'accordo...ma se la traccia ci chiedesse anke di verificare se la formula sia una tautologia o una contraddizione, significherebbe dover fare 2 tableau? ???
( uno diretto e uno della negata )
.:: Ad Astra Per Aspera ::.

Offline Rattilus

  • Direttore di Dipartimento
  • ***
  • Post: 1242
  • FeedBack: +53/-12
  • Se puoi sognarlo puoi farlo
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #8 il: Ven 30 Novembre, 23:20:11 - 2007 »
eh capito... quello chiedono tutti gli esercizi! quindi si fa sto tableaux skolemizzando e vedendo se la negata chiude o no. giusto?
Amministratore di Soloingegneria
Se tu hai una mela, e io ho una mela, e ce le scambiamo, allora tu ed io abbiamo sempre una mela per uno. Ma se tu hai un'idea, ed io ho un'idea, e ce le scambiamo, allora abbiamo entrambi due idee.

Offline Alexander

  • Studente di Dottorato
  • ***
  • Post: 239
  • FeedBack: +17/-7
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #9 il: Ven 30 Novembre, 23:33:56 - 2007 »
beh..se ti chiede di verificare ke la formula sia contraddittoria, o sia una tautologia, in tutti e due i casi devi fare un tableau... ;)
Sappiamo ke il tableau del primo ordine ci dà informazioni solo se risulta chiuso, una volta espanso (e quindi anke dopo aver applicato skolemizzazioni varie).
Quindi:
se ci viene chiesto di verificare se la formula sia una tautologia         ---> controlliamo il tableau della negata
se ci viene chiesto di verificare se la formula sia una contraddizione  ---> controlliamo il tableau diretto

...ma se richiede solo la soddisfacibilità, ce la potremmo cavare benissimo senza tableau, esibendo direttamente un modello qualsiasi (costruito "a occhio") ;D
.:: Ad Astra Per Aspera ::.

Offline anubi

  • Neo-Laureato
  • **
  • Post: 54
  • FeedBack: +4/-2
  • MASTRO... sei sempre il numero 1!!!
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #10 il: Ven 30 Novembre, 23:58:06 - 2007 »
ragazzi quando si deve verificare la soddisfacibilita' di una formula del primo ordine NON SI DEVE fare il tableau!!!

il tableau nn ci dice niente per quanto riguarda la soddisfacibilita' della formula!!!
ci dice solo se la formula e' tautologia o contraddizione, QUANDO CI DICE BENE, altrimenti il tableau al primo ordine nn ci dice assolutamente NIENTE!!!!!!!!

dobbiamo quindi inventarci un dominio, e delle interpretazioni ke rendono vera la formula data... (e caso mai, definire le interpretazioni delle variabili libere, qualora ci fossero)

sono questi i passi per risolvere quel benedetto esercizio sulla logica del primo ordine!!!!!

SPERO SIA STATO CHIARO!!!!!

SALUDOS Anubi

Aoh... E quanno ce vo', ce vo'!!!

Offline Rattilus

  • Direttore di Dipartimento
  • ***
  • Post: 1242
  • FeedBack: +53/-12
  • Se puoi sognarlo puoi farlo
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #11 il: Sab 01 Dicembre, 00:42:35 - 2007 »
Citazione
dobbiamo quindi inventarci un dominio, e delle interpretazioni ke rendono vera la formula data
quindi diciamo che questo dominio se lo costruiamo da subito è decisamente più facile rispetto a quello costruito a "skolemizzazione ultimata" perchè non compaiono interpretazioni di costanti o di funzioni... giusto?
Amministratore di Soloingegneria
Se tu hai una mela, e io ho una mela, e ce le scambiamo, allora tu ed io abbiamo sempre una mela per uno. Ma se tu hai un'idea, ed io ho un'idea, e ce le scambiamo, allora abbiamo entrambi due idee.

Offline defrenz

  • Direttore di Dipartimento
  • ***
  • Post: 1346
  • FeedBack: +35/-82
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #12 il: Sab 01 Dicembre, 00:55:11 - 2007 »
è abbastanza facile inventarsi un modello (struttura (dominio + interpretazione) + assegnazione) che soddisfi un'espressione...

di solito basta far in modo che uno o 2 predicati abbiano un certo valore (vero o falso) e quindi definire la loro interpretazione di conseguenza in modo da rispettare queste nostre condizioni (e ricordarsi i quantificatori che son quelli che danno + problemi) :P

Offline Artax

  • Global Moderator
  • Direttore di Dipartimento
  • *****
  • Post: 1778
  • FeedBack: +132/-55
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #13 il: Sab 01 Dicembre, 01:39:39 - 2007 »
il 90% delle formule so implica... quindi .. è banalmente trovabile un modello
http://artax87.iobloggo.com/

A computer language is not just a way of getting a computer to perform operations but rather that it is a novel formal medium for expressing ideas about methodology. Thus, programs must be written for people to read, and only incidentally for machines to execute.

Offline anubi

  • Neo-Laureato
  • **
  • Post: 54
  • FeedBack: +4/-2
  • MASTRO... sei sempre il numero 1!!!
    • Mostra profilo
Re: Linguaggi del primo ordine, chiarimenti
« Risposta #14 il: Sab 01 Dicembre, 15:25:05 - 2007 »
ESATTO!!!!
Aoh... E quanno ce vo', ce vo'!!!