CS 2800 Logic and Computation Spring 2019

このコースでは、形式論理とその計算への深い関わりについて紹介します。 論理学は、ACL2セダント定理証明システムを用いて、計算の観点から提示されます。 このコースでは、命題論理、再帰、帰納、等式推論、終端分析、書き換え、様々な証明技術など、計算のモデル化、設計、推論に必要な基礎的な方法を紹介することを目的としています。 本論文では、LISPベースの単純な言語であるACL2sの構文と意味論を論理学で形式化する方法を示す。 さらに、ACL2s言語を使って、プログラムの正式な推論、様々な抽象度でのシステムのモデル化、システム間のインターフェースの設計と指定、およびそのような構成されたシステムの推論を行う。 また、一階論理の断片に対する決定手順を検討し、その決定手順をシステムのモデルを分析するためにどのように使用できるかを検討します。

前提条件として、関数型プログラミング（CS 2500）と離散構造（CS 1800）に精通していること。

この授業を受ける学生は、毎日Piazzaのお知らせを確認することが必要です。