CS 2800: Logica e Calcolo Primavera 2019

Questo corso fornisce un’introduzione alla logica formale e alle sue profonde connessioni con il calcolo. La logica è presentata da una prospettiva computazionale utilizzando il sistema di proving ACL2 Sedantheorem. L’obiettivo del corso è di introdurre metodi fondamentali per modellare, progettare e ragionare sulla computazione, inclusa la logica proposizionale, la ricorsione, l’induzione, il ragionamento equazionale, l’analisi della terminazione, la riscrittura e varie tecniche di dimostrazione. Mostriamo come usare la logica per formalizzare la sintassi e la semantica del linguaggio ACL2s, un semplice linguaggio basato su LISP con contratti. Usiamo poi il linguaggio ACL2s per ragionare formalmente sui programmi, per modellare sistemi a vari livelli di astrazione, per progettare e specificare interfacce tra sistemi e per ragionare su tali sistemi composti. Esaminiamo anche le procedure decisionali per frammenti di logica del primo ordine e come tali procedure decisionali possono essere usate per analizzare modelli di sistemi.

I prerequisiti sono una familiarità di base con la programmazione funzionale (CS 2500) e le strutture discrete (CS 1800). Se non avete questo background, avete bisogno del permesso del vostro istruttore.

Gli studenti che seguono il corso sono tenuti a controllare Piazza per gli annunci ogni giorno.