Logic and Mechanized Reasoning Course ID 15311 Description Symbolic logic is fundamental to computer science, providing a foundation for the theory of programming languages, database theory, AI, knowledge representation, automated reasoning, interactive theorem proving, and formal verification. Formal methods based on logic complement statistical methods and machine learning by providing rules of inference and means of representation with precise semantics. These methods are central to hardware and software verification, and have also been used to solve open problems in mathematics. This course will introduce students to logic on three levels: theory, implementation, and application. It will focus specifically on applications to automated reasoning and interactive theorem proving. We will present the underlying mathematical theory, and students will develop the mathematical skills that are needed to design and reason about logical systems in a rigorous way. We will also show students how to represent logical objects in a functional programming language, Lean, and how to implement fundamental logical algorithms. We will show students how to use contemporary automated reasoning tools, including SAT solvers, SMT solvers, and first-order theorem provers to solve challenging problems. Finally, we will show students how to use Lean as an interactive theorem prover. Key Topics Mathematical foundations, propositional logic, first-order logic, fundamental algorithms, SAT solvers, SMT solvers, and first-order theorem provers. Required Background Knowledge None except pre requisite courses 15-151 and 15-150 Course Goals The course is intended to be an introduction to classical propositional logic, first-order logic, and higher-order logic, with a focus on applications to computer science, specifically to formal verification and automated reasoning. Learning Resources The course will provide an online interactive textbook and the relevant software. Assessment Structure Regular homework assignments, two midterm exams, and a final exam.
