The course presents propositional logic, predicate logic, and modal logic, and algorithms for proof and refutation for these logics. Classical results, including soundness, completeness, undecidability of some theories, and compactness, are obtained by systematically studying the algorithms. Algorithms for satisfiability and model checking are studied in depth. Examples and problems illustrate the use of logic in reasoning about programs and systems.
Students will be assessed by a series of exercises, problem sets, projects, and presentations.
Exercises will be shared in class. They may be peer critiqued. They will not be formally graded. Students should prepare exercises in advance and deposit them in the class "dropbox". Participation in the presentation and critique of exercises will be part of class participation, which will be 20% of the grade.
Problem sets are to be handed in. They will be graded by the instructors. These grades will be recorded. Problem sets will account for 20% of the grade.
Projects will be larger in scope and significantly more open ended than problem sets. Each student will do one project. The project grade is 40% of the grade
Presentations: students will be asked to prepare presentations on lecture topics and on their projects. Presentations will typically be 25 to 50 minute lecture segments. Presentations will account for 20% of the grade. Presentations will be evaluated for clarity, organization, technical content, and overall effectiveness.