Il corso si propone di analizzare alcuni argomenti di logica matematica legati alla teoria della dimostrazione in logiche non classiche (intuizionismo e sue estensioni) e alla dimostrazione automatica di teoremi in tali logiche. Verranno presentati sistemi deduttivi diretti (deduzione naturale) e indiretti (tableaux) e vari theorem prover. Per arrivare a questi argomenti si partirà dalla logica classica e si riprenderanno in modo più approfondito gli argomenti abbozzati nel corso di Fondamenti dell’informatica (corso obbligatorio della LT) presentando il calcolo della deduzione naturale e introducendo la forma clausale, il principio di risoluzione, la skolemizzazione e l’algoritmo di unificazione.

Si tratterà poi la sintesi logica degli algoritmi e si farà vedere come non sempre le dimostrazioni in logica classica permettono la sintesi diretta. Per questo si comincerà ad introdurre la logica intuizionista con sintassi a tableaux, semantica con modelli di Kripke e relativi teoremi di validità e completezza con cenni a estensioni dell'intuizionismo. Verranno analizzati i rapporti sintattici e semantici fra logica classica e logica intuizionista. Verranno poi presentati i theorem prover proposizionali PITP, PITPINV, IPTP sviluppati in C con le relative valutazioni delle strategie dimostrative, della complessità computazionale e dell’efficienza rispetto alla libreria di benchmark ILTP. Verranno infine valutati possibili sviluppi a livello predicativo.