CS 2800: Logic and Computation Spring 2019

Ten kurs stanowi wprowadzenie do logiki formalnej i jej głębokich powiązań z informatyką. Logika jest przedstawiona z perspektywy obliczeniowej przy użyciu systemu ACL2 Sedantheorem proving. Celem kursu jest wprowadzenie podstawowych, fundamentalnych metod modelowania, projektowania i rozumowania o obliczeniach, w tym logiki propozycjonalnej, rekurencji, indukcji, rozumowania równościowego, analizy terminacji, przepisywania i różnych technik dowodowych. Pokazujemy, jak używać logiki do formalizowania składni i semantyki podstawowego języka ACL2s, prostego języka opartego na LISP-ie z kontraktami. Następnie używamy językaACL2s do formalnego rozumowania o programach, modelowania systemów na różnych poziomach abstrakcji, projektowania i specyfikowania interfejsów między systemami oraz rozumowania o takich złożonych systemach. Badamy również procedury decyzyjne dla fragmentów logiki pierwszego rzędu i jak takie procedury decyzyjne mogą być wykorzystane do analizy modeli systemów.

Wymagania wstępne to podstawowa znajomość programowania funkcyjnego (CS 2500) i struktur dyskretnych (CS 1800). Jeśli nie masz tego tła, potrzebujesz zgody swojegoinstruktora.

Studenci biorący udział w zajęciach są zobowiązani do sprawdzenia Piazza dla ogłoszeń codziennie.