Laboratorio del corso di
Logica
Anno accademico 2024/25
Turno B
Avvisi
Il corso inizia martedì 25 febbraio. Verranno presentate le applicazioni usate nelle lezioni di laboratorio.
Orario delle lezioni
Le lezioni si svolgono il
martedì, 13.30-16.30, laboratorio Delta del Dipartimento di Informatica, via Celoria 18.
Per le informazioni sull'organizzazione del corso (suddivisione in turni,
esami, ecc.)
fare riferimento alla pagina del corso di
Logica.
Sono previste 11 lezioni:
25 febbraio;
4, 11, 18, 25 marzo;
8, 15 aprile;
6, 13, 20, 27 maggio.
Eventuali variazioni di orario verranno comunicate nella sezione Avvisi di questa pagina.
Ricevimento
Nel mio ufficio, via Celoria 18
(ufficio 4012, quarto piano)
su appuntamento
(fiorentini@di.unimi.it).
Si raccomando di usare il proprio indirizzo di posta di ateneo
(della forma nome.cognome@studenti.unimi.it) e di indicare
il proprio nome e cognome.
Libro di testo di riferimento
Dave Barker-Plummer, Jon Barwise and John Etchemendy,
Language, Proof and Logic, second edition,
CSLI publications.
Materiale relativo alle lezioni
Esercizi del libro di testo:
Cap. 2-8 (pdf),
Cap. 9-14 (pdf),
Cap. 16 (pdf).
Tabella dei predicati del linguaggio dei blocchi
(pdf).
Regole in Fitch
(pdf).
-
25 febbraio - Laboratorio 1
Introduzione all'uso di Tarski's World.
Documentazione
online (in inglese).
-
4 marzo - Laboratorio 2
- Parte 1.
- Definizione di modelli in Tarski:
3.3, 3.13.
- Traduzione da linguaggio naturale: 3.21, tradurre almeno le prime 5 frasi
(traduzione in italiano).
L'esercizio 3.22 propone dei test per verificare la correttezza delle traduzioni fatte.
- Parte 2.
- Costruzione tavole di verità in Bool, verificare se le proposizioni sono tautologie: 4.2.
- Continuazione esercizio 4.2: 4.3 (annotare risposte su file .txt).
- Parte 3.
- Esercizio 4.9.1
(stabilire enunciati tautologicamente possibili: 1,2,3,5,6,7,8,10): costruire la tabella come file .txt.
- Esercizio 4.9.2 (stabilire enunciati possibili nel mondo dei blocchi: 1,2,3,5,6,7,8,10): costruire la tabella come file .txt.
-
Facoltativo 4.9.3.
-
11 marzo - Laboratorio 3
-
Dimostrare in Fitch le seguenti argomentazioni, non
vanno usate regole Ana Con e Taut Con:
6.5, 6.6, 6.8 (da completare).
-
Nei seguenti esercizi, se il ragionamento è valido costruire una derivazione in Fitch, altrimenti
costruire un controesempio in Tarski.
È possibile usare Ana Con solo per introdurre ⊥
avendo come assunzioni due proposizioni atomiche che nel mondo dei blocchi
si contraddicono l'un l'altra
(ad esempio, è possibile derivare ⊥ dalle assunzioni Cube(a) e Tet(a), in quanto un blocco non può essere contemporaneamente un cubo e un tetraedro):
6.11, 6.12, 6.13, 6.36.
-
Costruire una derivazione in Fitch per i seguenti ragionamenti (sono tutti validi); non
vanno usate regole Ana Con e Taut Con:
6.18, 6.19, 6.20, 6.24, 6.25.
-
18 marzo - Laboratorio 4
- Parte 1
-
Verifica dell'equivalenza tatutologica di due proposizioni
mediante le tavole di verità
(da costruire usando Boole): 7.2, 7.5.
-
Traduzione di proposizioni da linguaggio naturale (scrivere le proposizioni in Tarski):
7.12; tradurre almeno 1,2,3,5,6,7,8 (traduzione in italiano).
Facoltativo: per controllare la soluzione, vedere esercizio 7.13.
- Costruzione di un modello (in Tarski): 7.14.
- Parte 2
-
I seguenti ragionamenti possono essere veri o falsi.
Se veri, costruire una derivazione in Fitch, senze usare Taut Con né Ana Con,
altrimenti costruire un contromodello in Tarski
(in quest'ultimo caso le formule A, B e C vanno istanziate
con opportune formule del linguaggio di Tarski):
8.20, 8.21, 8.22, 8.23, 8.24.
-
Derivazioni in Fitch di ragionamenti validi.
Non usare Taut Con né Ana Con.
Si raccomanda di impostare su carta lo schema della dimostrazione
prima di scriverla in Fitch:
8.26, 8.28.
Nei seguenti esercizi è possibile usare TautCon
per introdurre istanze del principio del terzo escluso:
6.40, 6.41.
-
25 marzo - Laboratorio 5
Esercizi riassuntivi sulla logica proposizionale (derivazioni in Fitch, controesempi).
Nelle derivazioni in Fitch,
usare Taut Con e Ana Con solo se esplicitamente
consentito.
Si raccomanda di impostare su carta lo schema della dimostrazione
prima di scriverla in Fitch.
- Parte 1
Derivazioni in Fitch di ragionamenti validi (nota):
8.33 (esercizio svolto, traduzione formale del ragionamento dell'esercizio 8.5),
8.31 (traduzione formale di 8.3; è possibile usare Taut Con per introdurre
una istanze del principio del terzo escluso),
8.32 (traduzione di 8.4),
8.34 (è possibile usare Ana Con per derivare ⊥ da due proposizioni atomiche),
8.35.
- Parte 2 (esercizi assegnati in uno degli scorsi esami).
Dimostrare in Fitch che le seguente formula è una tautologia tautologia:
¬ A ∨( ¬ B → ¬( A → B ))
(scaricare file prf ).
Suggerimento Mostrare che, assumendo la negazione della tautologia, si arriva a una contraddizione
(si deriva ⊥).
Dimostrar in Fitch e la seguente argomentazione avente una premessa (a sinistra di ⊧) e una conclusione
(a destra di ⊧) è valida:
¬( ¬ ( ¬ A ∨ B ) ∨ B) ∨ B ⊧ A → B
(scaricare file prf ).
- Parte 3
Se il ragionamento è valido,
costruire una derivazione in Fitch,
altrimente fornire un controesempio con Tarski.
È possibile usare Ana Con per derivare
⊥ da due proposizioni atomiche:
8.44, 8.45 (il ragionamento è valido,
usare TautCon
per introdurre una opportuna istanza del principio del terzo escluso),
8.46, 8.47, 8.48, 8.52.
Ulteriori esercizi:
8.49, 8.50, 8.51, 8.53.
-
8 aprile - Laboratorio 6
- Parte 1
- Verifica sintassi formule (Tarski): 9.1.
Ulteriore esercizi: 9.5.
- Parte 2
- Costruzione di modelli: 9.9.
- Validità di enunciati in un modello e traduzione (con uso Play Game) : 9.10.
- Costruzione di modelli o mostrare che non esistono: 9.11.
- Completare modello: 9.14.
- Parte 3
- Esercizi di traduzione (da svolgere usando Tarski):
9.16 (esistenziali), frasi
1-8 (traduzione in italiano).
9.17 (universali), frasi
1-8 (traduzione in italiano).
Come ulteriore esercizio, tradurre le rimanenti frasi.
-
15 aprile - Laboratorio 7
- Parte 1
-
Distinguere se le seguenti argomentazioni sono (a) tautologicamente valide,
(b) logicamente ma non tautologicamente valide, (c) non valide.
Esercizi:
10.2, 10.3, 10.4
-
Le seguenti argomentazioni sono valide. Distinguere se le conclusioni sono (a) conseguenza tautologica delle premesse,
(b) conseguenza al primo ordine delle premesse (FO) ma non conseguenza tautologica, (c) conseguenza nel mondo dei blocchi delle premesse ma non
conseguenza tutologica e neppure conseguenza al primo ordine. In quest'ultimo caso, descrivere in un file di testo un controesempio.
Esercizi:
10.11, 10.14, 10.15, 10.16, 10.17, 10.18, 10.19.
-
Parte 2
-
Determinare se le formule sono (a) tautologie, (b) verità logiche ma non tautologie, (c) non vere.
È possibile usare Fitch con Taut Con e FO Con per controllare le risposte.
Esercizi:
10.1 (1-5).
Ulteriori esercizi:
10.1 (6-10).
-
Parte 3
Verificare la validità delle seguenti argomentazioni.
Se il ragionamento è valido costruire una derivazione in Fitch,
altrimenti costruire un contromodello con Tarski.
Nelle derivazioni in Fitch
è possibile usare TautCon
per giustificare i passaggi che richiedono solo regole proposizionali.
Esercizi 13.2, 13.3, 13.4, 13.5, 13.11, 13.12, 13,13, 13.14, 13.15, 13.16.
Ulteriori esercizi (stesse modalità degli esercizi precedenti): 13.6, 13.7, 13. 8, 13.9.