CS 2800: Logică și calculatoare Primăvara 2019

Acest curs oferă o introducere în logica formală și legăturile sale profunde cu informatica. Logica este prezentată dintr-o perspectivă computațională folosind sistemul de demonstrare a teoremelor ACL2 Sedantheorem. Scopul cursului este de a introducemetode fundamentale, fundamentale pentru modelarea, proiectarea și raționamentul despre calcul, inclusiv logica propozițională, recursivitatea, inducția, raționamentul ecuațional, analiza terminării, rescrierea și diverse tehnici de demonstrație. Vom arăta cum să folosim logica pentru a formaliza sintaxa și semantica limbajului de bază ACL2s, un limbaj simplu bazat pe LISP cu contracte. Utilizăm apoi limbajul ACL2s pentru a raționa formal despre programe, pentru a modela sisteme la diferite niveluri de abstractizare, pentru a proiecta și specifica interfețe între sisteme și pentru a raționa despre astfel de sisteme compuse. De asemenea, examinăm procedurile de decizie pentru fragmente de logică de ordinul întâi și modul în care astfel de proceduri de decizie pot fi folosite pentru a analiza modele de sisteme.

Precondițiile sunt o familiaritate de bază cu programarea funcțională (CS 2500) și cu structurile discrete (CS 1800). Dacă nu aveți aceste cunoștințe, aveți nevoie de permisiunea instructorului.

Studenții care urmează acest curs sunt obligați să verifice zilnic anunțurile din Piazza.