CS 2800: Jaro 2019

Tento kurz je úvodem do formální logiky a jejího hlubokého propojení s výpočetní technikou. Logika je prezentována zpočítačové perspektivy s využitím systému ACL2 Sedantheorem proving. Cílem kurzu je představitzákladní, fundamentální metody pro modelování, navrhování a zdůvodňování výpočtů, včetně výrokové logiky, rekurze, indukce, rovnostního zdůvodňování, terminační analýzy, přepisování a různých důkazových technik. Ukážeme si, jak pomocí logiky formalizovat syntaxi a sémantiku jádra jazyka ACL2s, jednoduchého jazyka založeného na LISPu s kontrakty. JazykACL2s pak používáme k formálnímu zdůvodňování programů, k modelování systémů na různých úrovních abstrakce, k návrhu a specifikaci rozhraní mezi systémy a k zdůvodňování takových složených systémů. Zkoumáme také rozhodovací procedury pro fragmenty logiky prvního řádu a jak lze takové rozhodovací procedury použít k analýze modelů systémů.

Předpokladem je základní znalost funkcionálního programování (CS 2500) a diskrétních struktur (CS 1800). If youdo not have this background, you need consent of yourinstructor.

Studenti navštěvující tento předmět jsou povinni denně kontrolovat oznámení na Piazza.