Logica e Macchine

L'esperienza mostra come sia scarsamente affidabile il ragionamento umano nel dedurre conclusioni certe da premesse date. L'informatica suggerisce, d'altra parte, l'uso di macchine come uno degli strumenti più affidabili per trattare compiti di tipo ripetitivo nei quali è facile commettere errori logici. Tuttavia le macchine non conoscono il linguaggio e le modalità di ragionamento dell'uomo. Come correlare queste due realtà? L'idea naturale à "trasferire manualmente" alla macchina le premesse e dotarla di "meccanismi automatici" di deduzione. Attraverso l'esame di alcuni casi molto semplici, si cercherà di coinvolgere lo studente nei due aspetti: da una parte la traduzione delle premesse e della conclusione in un formato comprensibile ad una macchina e, dall'altro, nell'utilizzo di strumenti di dimostrazione automatica. Il laboratorio si propone inoltre di complementare gli aspetti più filosofico/matematici dei rapporti tra linguaggio e sua formalizzazione matematica con l'approccio informatico che vede nella logica matematica un caso particolare e privilegiato di manipolazione simbolica.