LOGI : INTRODUZIONE ALL'USO

Generalità

Il software didattico LOGI è stato progettato come "supplemento" al course-ware Language, Proof and Logic (LPL) utilizzato nel corso di Logica Matematica. In LPL vari esercizi devono essere risolti "a mano", dal momento che prevedono segnature e interpretazioni diverse dalla quella del mondo dei blocchi utilizzata in LPL dalla applicazione "Tarski's World", che d'ora in poi indicheremo con TW. LOGI ha lo scopo di consentire la (auto)valutazione automatica di tali esercizi. Inoltre fornisce le valutazioni boolene delle formule proposizionali e, più in generale, della forma vero-funzionale delle formule del primo ordine.

LOGI è sviluppato in SWI Prolog. Nella sezione Installazione trovate le istruzioni per installare SWI Prolog e l'applicazione LOGI.

Installazione

• Scaricare dal sito logi.zip e scompattare e aprire la cartella logiBasic, che contiene lib, logi_implm e il file fol.pl, come illustrato in figura.

  

• Dal logiBasic lanciate fol.pl. Se l'applicazione è installata correttamente si aprono i "fogli" di lavoro:

  

Uso del sistema - uno sguardo generale.

• Nella prima fase si inseriscono le formule o ragionamenti e le interpretazioni (circostanze) richieste per lo svolgimento dell’esercizio; formule e ragionamenti vanno scritti sul foglio FORMULE e le interpretazioni sul foglio INTERPRETAZIONI. In fase di scrittura, il menù EDIT mette a disposizione le operazioni di cut and paste. I simboli logici possono essere inseriti tramite il menù OPERATORI o tramite i corrispondenti "acceleratori." Quanto scritto sui fogli deve essere controllato e registrato tramite il menù FOGLI.

  Con CONTROLLA FORMULE del menù FOGLI il sistema controlla la correttezza sintattica delle formule, ricostruisce la segnatura utilizzata. La segnatura ricostruita può essere visualizzata tramite la voce Mostra la segnatura ricostruita del menù HELP.

  Il comando REGISTRA INTERPRETAZIONE del menù FOGLI è possibile solo dopo aver salvato le formule, dal momento che le interpretazioni devono riguardare la segnatura usata nelle formule. Il sistema controlla che l'interpretazione sia inserita correttamente e riguardi la segnatura delle formule. Siccome è possibile associare più interpretazioni ad uno stesso foglio FORMULE, il sistema chiede di dare un nome alla interpretazione in esame, che viene "registrata" con quel nome.

  Tramite l voce Mostra la bozza d'interpretazione del menù HELP è possibile visualizzare una bozza di interpretazione generata automaticamente dal sistema. Tale bozza può essere usata come "brogliaccio" da cui partire nella stesura di una interpretazione, tramite la voce USA BOZZA d'interpretazione del menù FOGLI.

  Altri comandi del menù FOGLI consentono di scegliere una delle interpretazioni registrate, di eliminarne una, alcune o tutte dal registro, ed altre operazioni che verranno presentate nel seguito.

• Nella seconda fase si valuta/autovaluta la correttezza delle risposte date all'esercizio. Allo scopo, il menù VALUTAZIONE consente la valutazione automatica della verità delle formule del foglio FORMULE nella interpretazione del primo ordine riportata sul foglio INTERPRETAZIONE; ciò consente di valutare se una interpretione sia modello di un insieme di assiomi o sia un contro-esempio della validità di una formula o un ragionamento in FOL.

  La voce VERITA' del menù VALUTAZIONE consente di visualizzare mediante colori la verità (in verde) o falsità (in rosso) delle formule riportate sul foglio FORMULE nella interpretazione riportata sul foglio INTERPREAZIONE. Se il foglio contiene un ragionamento, viene valutato il ragionamento e la parola chiave "CONSEGUENZA" viene colorata in rosso se il ragionamento non vale (cioè le premesse sono vere e la conseguenza falsa) e in verde altrimenti.

  La verità di una formula in una interpretazione può essere spiegata in uno o più modi. Con la voce di menù SPIEGAZIONI è possibile vedere tutte le spiegazioni possibili. Ciò è utile in esercizi in cui si chieda di giustificare le risposte.

  Nel caso di formule proposizionali si possono valutare proprietà riguardanti l'insieme delle interpretazioni proposizionali; con la voce di menù TAUTOLOGIE si può verificare se una formula proposizionale sia una tautologia e con la voce CONSEGUENZA TAUTOLOGICA si può verificare se una formula proposizionale sia conseguenza tautologica di un insieme di premesse. Il sistema non si limita a fornire le risposte ma consente anche di vedere come queste siano state ottenute, in modo da fornire una giustificazione detagliata delle risposte date.

• Il menù HELP non consente solo di vedere la segnatura ricostruita e la bozza di interpretazione. Esso consente anche di accedere a spiegazioni relative all'uso dei fogli FORMULE e INTERPRETAZIONI, a spiegazioni relative ai menù e ad esempi di esercizi svolti.
• Il menù VERBOSE consente di disattivare (OFF) o attivare (ON) la modalità "verbose"; se attiva vengono mostrate varie spiegazioni/avvisi che, una volta acquisita familiarità con il sistema, diventano inutilmente pesanti. L'applicazione viene installata in modalità "verbose".

Per acquisire un minimo di manualità con l'editor incorporato, si proceda come segue. Su uno dei fogli FORMULE o INTERPRETAZIONE si scriva un testo arbitrario e si usino Copy, Cut, Paste; si tratta di funzioni simili in tutti gli editor, per cui non le esaminiamo qui. Vediamo invece le funzioni peculiari dell'editor integrato, che riguardano:

• I commenti. Si scriva un commento, ad es. % Oggi è bel tempo. I commenti iniziano con % e sono mono-linea. Si noti che, una volta andati a capo, il commento viene evidenziato in corsivo blu.

  

• I simboli logici. Il menù OPERATORI contiene una voce per ogni simbolo logico e per la diseguaglianza (neq). Ad esempio, selezionando la voce and e "clickando" su di essa, viene inserito sul foglio il simbolo logico ∧.

  ==>

• Accanto ad ogni simbolo logico è riportato il corrispondente "acceleratore", cioè una combinazione di tasti di controllo che inserisce il simbolo da tastiera; ad esempio, in "And \C-a", \C-a indica che tenendo premuto il tasto Ctrl e premendo a si ottiene l'inserimento di ∧. Per esercizio ⊥ si inseriscano tutti i simboli logici presenti sul menù.

Seguono alcuni esercizi guidati.

Esercizio 1. Interpretazioni in FOL

Si chiede di

1. Scrivere su un foglio le due proposizioni atomiche Tet(a) e RightOf(rm(a),b).
2. Creare un'interpretazione della segnatura del foglio appena scritto, che rappresenti il mondo di Tarski mostrato in Figura:

   

3. Valutare la verità delle formule del foglio nella interpretazione creata ed esaminare le spiegazioni fornite dal sistema.
4. Modificando solo l'interpretazione delle costanti a e b, scrivere
   • un'interpretazione che renda Tet(a)=false e RightOf(rm(a),b)=false,
   • una che renda Tet(a)=true e RightOf(rm(a),b)=false
   • e una che renda Tet(a)=true e RightOf(rm(a),b)=true.
   Per ciascuna delle tre interpretazioni, si disegni un mondo corrispondete usando il tool "Tarski's World" di LPL.

1. Scrivere le formule

Scrivere sul foglio FORMULE le due formule atomiche richieste, Tet(a) e RightOf(rm(a),b). Ogni formula deve essere preceduta da un'etichetta, usata dal sistema per indicarla nei vari messaggi. E' meglio controllare sempre quanto scritto con la voce CONTROLLA FORMULE del menù FOGLI oppure con il corrispondente acceleratore \C-f (f per "formule"). Se vi sono errori, vengono segnalati e la verifica non ha successo. Se non vi sono errori, la verifica ha successo si ha il messaggio "Fatto".

>> >>

2. Creare l'interpretazione richiesta

La prima cosa da fare per creare un'interpretazione è stabilire l'universo del discorso. Visto che non possiamo "inserire fisicamente" nel computer gli oggetti del dominio, li "inseriamo" mediante dei nomi interni con cui indicare in modo biunivoco gli oggetti reali. Stabilito l'universo, su di esso interpreteremo i simboli di costante, funzione e predicato della segnatura.

• Universo. Sulla scacchiera abbiamo due cubi, uno grande e uno piccolo, ed un tetraedro. Poniamo:
  u := {'il cubo grande', 'il cubo piccolo', 'il tetraedro'}
  dove u è la sorta "universo del discorso" e fra graffe abbiamo messo i tre nomi interni che d'ora in poi useremo per i tre blocchi fisicamente sulla scacchiera, come mostrato in figura

  

• Interpretazione dei simboli di costante. Interpretiamo a come nome del cubo piccolo e b del tetraedro. Formalmente poniamo:
  a := 'il cubo piccolo'
  b := 'il tetraedro'
• Interpretazione dei simboli di funzione. Seguendo il libro di testo, interpretiamo rm/1 come la funzione che associa ad ogni blocco il blocco che si trova più a destra sulla sua stessa riga. Il blocco più a destra sulla riga del cubo grande è il cubo grande medesimo. Il blocco più a destra sulla riga del tetraedro è il cubo piccolo, che è anche il più ad destra sulla sua stessa riga. Quindi l'interpretazione di rm/1 è:
  rm/1 := {('il cubo grande')->'il cubo grande', ('il tetraedro')->'il cubo piccolo', ('il cubo piccolo')->'il cubo piccolo'}
• Interpretazione dei simboli di predicato. Le interpretazioni di Tet/1 e RightOf/2 corrispondenti alla nostra scacchiera sono:
  Tet/1 := {('il tetraedro')}
  RightOf/2 := {('il cubo piccolo', 'il tetraedro'), ('il tetraedro', 'il cubo grande')}
  La prima indica che l'unica (x) che verifica Tet(x) è ('il tetraedro'). La seconda indica che le coppie (x,y) che verificano RightOf(x,y) sono ('il cubo piccolo', 'il tetraedro') e ('il tetraedro', 'il cubo grande').

Per immettere un'interpretazione si usa il foglio INTERPRETAZIONE. Per acquisire familiarità con la sintassi delle interpretazioni, le prime volte conviene partire dalla "bozza d'interpretazione" che può essere caricata sul foglio INTERPRETAZIONE con la voce USA BOZZA d'interpretazione del menù FOGLI. Il sistema chiede di dare un nome ad ogni interpretazione, dal momento che per un stesso foglio di formule si possono avere più interpretazioni. Scegliendo, ad es., il nome i1 si ottiene il salvataggio della bozza con nome i1, come illustrato in figura:

>> >>

Modificando la bozza (con le usuali operazioni di editing), si può introdurre l'interpretazione desiderata, che nel nostro esempio è:

>> >>

3. Valutare la verità delle formule nell'interpretazione creata

Tramite la voce VERITA' del menù VALUTAZIONE si chiede al sistema di valutare la verità delle formule sul foglio FORMULE nella interpretazione mostrata sul foglio INTERPRETAZIONE i1. Si ottiene:

>>

Con la voce SPIEGAZIONI del menù VALUTAZIONE si ottiene la visualizzazione delle spiegazioni della verità/falsità di una formula, selezionando una delle formule del foglio. Le spiegazioni vengono elencate su nuovi fogli di spiegazione temporanei. Il sistema inizia con la "Spiegazione 0":

>> >>

Per esercizio si esaminino le spiegazioni della verità della formula f2.

4. Modificare l'interpretazione di a, b in modo da ottenere le altre combinazioni di valori di verità e disegnare i mondi corrispondenti

Costruiamo le interpretazioni richieste modificando 'interpretazione delle costanti in i1.

• Interpretazione che rende Tet(a) falsa e RightOf(rm(a),b) falsa.
  Modifichiamo le interpretazioni delle costanti ponendo a := 'il cubo grande', b := 'il cubo grande'. Per evitare di ricoprire la interpretazione precedente, registriamo la nuova interpretazione cambiando il nome i1, proposto in automatico dal sistema, in i2:

  >>
  >> >> >>
  

  Per verificare la correttezza di quanto fatto, usiamo valuta la verità:

  >>

  Le due formule sono colorate di rosso, dunque sono false in i2, come richiesto. Disegnamo ora il mondo corrispondente a i2:

  

  Si osservi che abbiamo registrato due interpretazioni, i1, quella di partenza, che falsifica e i2, quella in cui abbiamo modificato l'interpretazione di b. Possiamo scegliere una delle due tramite la voce Scegli interpretazione del menù FOGLI; ad esempio, possiamo tornare a i1:

  >> >>

• Gl altri due casi sono lasciati come esercizi non guidati.

Dire quali delle seguenti formule sono "verità logiche in in TW" (TW: Tarski's World del libro di testo) ma non valide in FOL, quali sono valide FOL ma non tautologie, quali tautologie.

1. (¬∃x Tet(x) ∧ (Cube(a) → ∃x Tet(x))) → ¬Cube(a)
2. ∀x ∀y (x ≠ y → LeftOf(x,y) ∨ LeftOf(y,x) )
3. ∀x ∀y (¬SameCol(x,y) ↔ LeftOf(x,y) ∨ LeftOf(y,x) )
4. ∀x ¬(Tet(x) ∨ Cube(x)) → ¬∃x (Tet(x) ∨ Cube(x))

Soluzione Guidata

Analizziamo le formule una per una, diamo una risposta e la verifichiamo.

Risposta per la formula 1

Per verificare la risposta, scriviamo la formula e controlliamo che la formula sia sintatticamente corretta:

Per esercizio si esamini la segnatura ricostruita e si carichi la bozza di interpretazione. Si provi poi ad usare la voce TAUTOLOGIE del menù VALUTAZIONE, scegliendo f1 come formula da valutare, e si noti la risposta ottenuta.

Per mostrare che f1 è una tautologia passiamo alla forma vero-funzionale. Possiamo procedere in due modi.

• Modo 1.

  Costruiamo la forma vero-funzionale ponendo P = '∃x Tet(x)' e Q = 'Cube(a)', seguendo quanto detto nella risposta.

  

  Chiediamo ora di usare la bozza d'interpretazione. Il sistema riconosce che si tratta di una segnatura proposizionale e genera come bozza una interpretazione proposizionale. Modificandola, introduciamo le interpretazioni considerate nella risposta nei casi a), b), c) e controlliamo quanto detto.

  La spiegazione data nella risposta per il caso a) è: Se Q è falsa, il conseguente ¬Q è vero, per cui l'implicazione è vera. Per verificarla, poniamo Q :=false indipendentemente da P, che lasceremo non interpretato. Salviamo tale interpretazione con il nome caso_a; il sistema avvisa che P/0 non è interpretato, ma accetta l'interpretazione, come mostrato in figura.

  
  >> >> >>

  Ora controlliamo la correttezza della spiegazione data per il caso a), usando la voce SPIEGAZIONI del menù VALUTAZIONE:

  >> >>

  La Spiegazione 0 corrisponde a quella data nella risposta per il caso a): la forma vero-funzionale è vera in questa interpretazione parziale perché la conclusione è vera essendo falsa Q.

  Gli altri casi si verificano in modo analogo. Omettendo i vari passaggi, abbiamo:

  

  che conferma la risposta per in caso b), e:

  

  che conferma la risposta per in caso c).

  Possiamo ottenere una conferma delle risposte date anche chiedendo al sistema di valutare in automatico la forma vero-funzionale e di stabilire se si tratti di una tautologia, usando la voce TAUTOLOGIE del menù VALUTAZIONE. Otteniamo:

  >> >>
  >> >> ... ... ... ... >>

  NOTA. Mentre valutando le spiegazioni caso per caso possiamo limitarci alle spiegazioni rilevanti, chiedendo la valutazione automatica vengono esaminate tutte le combinazioni booleane e la valutazione segue le tavole di verità.

• Modo 2.

  Siccome il sistema accetta come simboli proposizionali arbitrarie sequenze di caratteri racchiuse fra apici, un modo immediato per passare alla forma vero-funzionale è il seguente: anziché sostituire con nuovi simboli proposizionali le sottoformule quantificate e le sottoformule atomiche esterne allo scopo dei quantificatori, possiamo racchiuderle fra apici. Procediamo in questo modo, salviamo e carichiamo la bozza d'interpretazione:

  
  

  Come si vede, usando gli apici 'Cube(a)' e '∃x Tet(x)' diventano simboli proposizionali (gli apici dicono al sistema di non analizzare ciò che racchiudono e di cinsiderarlo come un simbolo).

  Modificando la bozza, si ottiene il caso a) che si presenta come segue:

  >>

  Omettiamo gli altri casi, lasciati per esercizio.

Risposta per la formula 2

Per controllare la risposta, disegnamo il contro-esempio (due blocchi diversi sulla stessa colonna) usando Tarski's World e verifichiamo che in tale mondo la formula 2 è falsa.

L'uso di Tarski's World è molto intuitivo ma non spiega in dettaglio il modo con il quale il sistema è giunto a valutare la formula come falsa. Possiamo farlo usando LOGI e scrivendo la interpretazione corrispondente al mondo disegnato in Fig.e2.10. Abbiamo:

>> salvataggio ... >> >> ...

Risposta per la formula 3

Non possiamo dimostrare (a) in LOGI; per dimostrarlo formalmente dobbiamo ricorrere a Fitch e usare ANACON; lasciamo questa parte come esercizio non guidato. Per mostrare che la risposta (b) è corretta, scriviamo la formula e il contro-esempio in FOL.

Ora verifichiamo che si tratti di un contro-esempio, usando Valuta la verità ed Elenca le spiegazioni: l2.logi:

>>

Risposta per la formula 4

In LOGI non possiamo verificare (a); dobbiamo usare Fitch (lasciato come esercizio non guidato). Per verificare (b) possiamo procedere in uno dei modi mostrati per la formula 1; lasciamo ciò come esercizio non guidato.

Ricordiamo che una formula è conseguenza logica di un insieme di premesse in un dato contesto sse è vera in tutte le circostaze del contesto in cui sono vere le premesse. Per trovare un contro-esempio nel contesto, non basta trovare una interpretazione che renda vere le premesse e falsa la conseguenza, bisogna anche che questa interpretazione rappresenti una circostanza possibile nel contesto.

La frase "You may assume that Folly can only be one person's pet at any given time" stabilisce il contesto in cui valutare il ragionamento, ovvero l'insieme delle circostanze possibili nel contesto considerato, che chiameremo (PETS). In (PETS) non sono possibili circostanze in cui, in un dato istante, un animale appartiene a due persone distinte. Inoltre, anche se ciò non è esplicitamente detto nel testo dell'esercizio, è chiaro che in (PETS) Max e Claire sono due persone distinte, Folly è un animaletto, 2:05 pm e 2 pm sono due istanti temporali distinti.

Esaminiamo l'esercizio a 3 livelli diversi: nel contesto (PETS), nella logica del primo ordine (FOL) e nella logica proposizionale (TAUT). Per rendere l'analisi più rigorosa, ci sganciamo dal lingauggio naturale e traduciamo le frasi in 1,2,3 in formule. Usando il linguaggio introdotto dal libro di testo per i pets, traduciamo "a was b's pet at t pm" con "Owned(b,a,t)". Otteniamo:

1. Owned(Claire, Folly, 2pm) ∨ Owned(Claire, Folly, 2:05pm)
2. Owned(Max, Folly, 2pm)
3. Owned(Claire, Folly, 2:05pm)

Riformuliamo in LOGI le tre domande, sotto forma di conseguenza logica, e le esaminiamo, nell'ordine.

Domanda 1. Does (3) follow from (1) and (2)?

Il ragionamento corrispondente a questa domanda è:

Rispondendo SI il sistema genera la interpretazione Bool0.gen e valuta in essa il ragionamento, colorando le tre formule in rosso, dal momento che sono false in Bool0.gen, e la parola chiave CONSEGUENZA in verde, dal momento che le premesse sono false in Bool0.gen e quindi il ragionamento è corretto (da premesse false segue qualsiasi cosa). Poi il sistema chiede se si vuol proseguire con altre interpretazioni.

... ...

Passiamo ora a (FOL). Per recuperare le formule originali che avevamo salvato nel file pets_fol, lo riapriamo:

Infine consideriamo il contesto (PETS). L'interpretazione intp_corrispondente_a_Boole5 non rappresenta una circostanza possibile nel contesto, in quanto nell'istante t1 abbiamo che pet appartiene contemporaneamente a due persone distinte, persona1 e persona2. Comunque si vadano a interpretare Claire, Max come due persone distinte e Folly come un animaletto come previsto nel conteto(PETS), non è possibile rendere conemporaneamente veri Owned(Max, Folly, pm_2) e Owned(Claire, Folly, pm_2) senza violare l'assunzione che un animaletto NON possa appartenere contemporante a due persone diverse. Siccome l'unico modo per ottenere un controesempio è rendere veri Owned(Max, Folly, pm_2) e Owned(Claire, Folly, pm_2) e Owned(Claire, Folly, pm_2_05) falso, non è possibile trovare contro-esempi in (PETS). Dunque in (PETS) f3 segue logicamente da f1 e f2.

Domanda 2.Does (2) follow from (1) and (3)?

Per avere un contro-esempio in (PETS) cerchiamo una circostanza possibile in (PETS) in cui Owned(Max, Folly, pm_2) è falso (per cui la conseguenza f2 è falsa) e Owned(Claire, Folly, pm_2_05) è vero (per cui le premesse (1) e (3) sono vere). Siccome vogliamo una interpretazione che rappresenti una circostanza del contesto, prendiamo come nomi interni claire e max per indicare proprio le due persone di nome Claire e Max, folly per indicare il gatto di Claire che si chiama Folly e '2:00' e '2:05' per indicare i due istanti temporali considerati; supponiamo che nell'intervallo di tempo considerato Claire non venda o acquisti gatti, per cui folly le appartiene sia alle '2:00', sia alle '2:05'. Ovviamente folly non appartiene a Max. Tale interpretazione è l'interpretazione cex_domanda2 riportata in figura:

Valutiamo il contro-esempio con il comando valuta la verità del menù VALUTAZIONE. Otteniamo che si tratta di un contro-esempio in (FOL):

Domanda 3. Does (1) follow from (2) and (3)?

La directory di lavoro

Nell'esercizio precedente abbiamo salvato due files. I files vengono salvati e cercati nella directory di lavoro. L'installazione assume come directory di lavoro di default la directory in cui viene lanciata l'applicazione.

Si può vedere qual'è la directory di lavoro attualmente in uso con Vedi directory di lavoro attuale del menù EDIT:

.. scrivo il nome Esempi e click so OK

Ora la directory di lavoro è Esempi e LOGI crea o apre files in essa.