CS 2800: Logic and Computation Spring 2019

Dieser Kurs bietet eine Einführung in die formale Logik und deren tiefe Verbindungen zum Rechnen. Die Logik wird aus einer rechnerischen Perspektive unter Verwendung des ACL2 Sedantheorembeweissystems vorgestellt. Ziel des Kurses ist es, grundlegende Methoden für die Modellierung, den Entwurf und die Argumentation von Berechnungen vorzustellen, einschließlich Aussagenlogik, Rekursion, Induktion, Gleichheitsschluss, Terminierungsanalyse, Umschreiben und verschiedene Beweistechniken. Wir zeigen, wie man Logik verwendet, um die Syntax und Semantik der ACL2s-Kernsprache zu formalisieren, einer einfachen LISP-basierten Sprache mit Verträgen. Anschließend verwenden wir dieACL2s-Sprache, um formal über Programme nachzudenken, um Systeme auf verschiedenen Abstraktionsebenen zu modellieren, um Schnittstellen zwischen Systemen zu entwerfen und zu spezifizieren und um über solche zusammengesetzten Systeme nachzudenken. Wir untersuchen auch Entscheidungsprozeduren für Fragmente der Logik erster Ordnung und wie solche Entscheidungsprozeduren verwendet werden können, um Modelle von Systemen zu analysieren.

Die Voraussetzungen sind eine grundlegende Vertrautheit mit funktionaler Programmierung (CS 2500) und diskreten Strukturen (CS 1800). Wenn Sie nicht über diese Kenntnisse verfügen, benötigen Sie die Erlaubnis Ihres Dozenten.

Die Studenten, die den Kurs belegen, müssen täglich auf Piazza nach Ankündigungen suchen.