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
Instructor:
Marijn Heule- Location: Gates Hillman Complex 9107
- Email: marijn@cmu.edu
- Office Hours: TBD
Teaching assistants:
TBDLectures: Tuesdays and Thursdays from 11:00am to 12:20pm in GHC 4307
Textbook: https://avigad.github.io/lamr/
Repository: https://github.com/avigad/lamr
Assignments: The homework are available on Gradescope and due on Wednesday (midnight).
Grading: Grades are based on homework assignments (40%, 10 x 30 points) and on the three exams (60%, 3 x 150 points).
Late policy: Homework assignments can be submitted one day late with a penalty of subtracting 3 points (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.