Logic and Mechanized Reasoning

Course Overview

Symbolic logic is fundamental to computer science, providing a foundation for the theory of programming languages, the theory of databases, AI, knowledge representation, automated reasoning, 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 is an introduction to symbolic logic on three levels: theory, implementation, and application. 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. Finally, we will show students how to use contemporary automated reasoning tools, including SAT solvers, SMT solvers, and first-order theorem prover, to solve challenging problems, and 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.

Prerequisite knowledge: None except prerequisite courses 15-151 and 15-150.

Logistics

Instructors:

Marijn Heule Jeremy Avigad

Teaching assistant:

Wojciech Nawrocki

Lectures: Tuesdays and Thursdays from 11:50am to 1:10pm in Porter 125D

Textbook: https://avigad.github.io/lamr/ (work in progress)

Repository: https://github.com/avigad/lamr

Grading: Grades are based on homework assignments (40%) and on the three exams (60% = 20% × 3).

Late policy: Homework assignments that are submitted late will be penalized by subtracting 5 points per day (10%).

Learning Resources: The course will provide an online interactive textbook and the relevant software.

Academic Integrity: Students are expected to complete each homework assignment on their own, and should be able to explain all of the work that they hand in. Copying material from other students or online sources is not allowed. If you have questions about whether something might be an issue, contact the course staff before discussing further. Please refer to the Carnegie Mellon Code for information about university policies regarding academic conduct.

Take care of yourself: Do your best to maintain a healthy lifestyle this semester by eating well, exercising, avoiding drugs and alcohol, getting enough sleep and taking some time to relax. This will help you achieve your goals and cope with stress. All of us benefit from support during times of struggle. You are not alone. There are many helpful resources available on campus and an important part of the college experience is learning how to ask for help. Asking for support sooner rather than later is often helpful. If you or anyone you know experiences any academic stress, difficult life events, or feelings like anxiety or depression, we strongly encourage you to seek support. Counseling and Psychological Services (CaPS) is here to help: call 412-268-2922 and visit their website. Consider reaching out to a friend, faculty or family member you trust for help getting connected to the support that can help.