ECE: EE 546: Special Topics Course: Knowledge Representation and Reasoning – WIN 25

November 5, 2024

EE 546: Special Topics Course: Knowledge Representation and Reasoning

• Quarter: Winter 2025
• Instructor: Professor Eric Klavins
• Time: Tuesdays and Thursdays from 1:00 pm to 2:20 pm
• Credits: 4

Description: In this course we will study the representation and manipulation of knowledge symbolically using logic and automated reasoning. Students will learn propositional logic, first-order logic, type theory, and various application-specific logical frameworks and the proof systems associated with them. These frameworks will be examined in depth using the Lean Theorem Prover, and students can expect to learn in detail how to construct a computer-checkable formal proof. Along the way, we will describe the power and limitations of automated reasoning systems from the point of view of computability, computational complexity, and proof theory. The course will include a review of recent literature, such as results combining formal logic with machine learning. The applications of knowledge representation and reasoning are diverse, and we will introduce applications in pure and applied mathematics, trustworthy AI, hardware verification, and robotics among other areas. Students should have solid programming skills and will ideally have taken at least one course involving mathematical proof. The course will culminate in a project combining ideas developed in the course with a domain of interest to the student.

Please feel free to reach out to me at klavins@uw.edu if you have any questions about the course.