CS 2800: Logik och beräkning Våren 2019

Denna kurs ger en introduktion till formell logik och dess djupa kopplingar till beräkning. Logiken presenteras ur ett beräkningsperspektiv med hjälp av ACL2 Sedantheoremprovningssystemet. Målet med kursen är att introducera grundläggande metoder för att modellera, utforma och resonera om beräkningar, inklusive påståendelogik, rekursion, induktion, ekvationella resonemang, avslutningsanalys, omskrivning och olika bevistekniker. Vi visar hur man använder logik för att formalisera syntaxen och semantiken för ACL2s kärnspråk, ett enkelt LISP-baserat språk med kontrakt. Vi använder sedan ACL2s-språket för att formellt resonera om program, för att modellera system på olika abstraktionsnivåer, för att utforma och specificera gränssnitt mellan system och för att resonera om sådana sammansatta system. Vi undersöker också beslutsprocedurer för fragment av första ordningens logik och hur sådana beslutsprocedurer kan användas för att analysera modeller av system.

Förutsättningarna är en grundläggande förtrogenhet med funktionell programmering (CS 2500) och diskreta strukturer (CS 1800). Om du inte har denna bakgrund måste du få tillstånd av din lärare.

Studenter som deltar i kursen måste kontrollera Piazza dagligen för meddelanden.