October 25, 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.
To learn more about what people are doing with automated theorem provers, here are a few popular science articles to get you started.
AI for Math Olypiad Problems
https://www.nytimes.com/2024/07/25/science/ai-math-alphaproof-deepmind.html
Proving Chatbots Correct
https://www.nytimes.com/2024/09/23/technology/ai-chatbots-chatgpt-math.html
Please feel free to reach out to me at klavins@uw.edu if you have any questions about the course.
Restr 22022 B 4 TTh 100-220 ECE 269 Klavins,Eric TITLE: KNOWLEDGE REPRESENTATION AND REASONING --- REPRESENTATION & MANIPULATION OF KNOWLEDGE SYMBOLICALLY USING LOGIC AUTOMATED REASONING. STUDENTS LEARN FIRST ORDER & HIGHER-ORDER LOGICS B BUILDING A SIMPLE SEMI-AUTOMATED INFERENCE SYSTEM FROM SCRATCH IN PYTHON, AS WELL AS EXPLORING EXISTING REASONING SYSTEMS SUCH AS LEAN. ALONG THE WAY, WE WILL DESCRIBE THE POWER & LIMITATIONS OF AUTOMATED RESEARCH SYSTEMS FROM THE POINT OF VIEW OF COMPUTABILITY, COMPUTATIONAL COMPLEXITY, & SET THEORY. AFTER ESTABLISHING A BASIC FOUNDATION, WE WILL INVESTIGATE THE COMBINATION OF SYMBOLIC REASONING SYSTEMS WITH MACHINE LEARNING APPROACHES, A TOPIC THAT HAS SEEN REMARKABLE ADVANCES IN THE PAST SEVERAL YEARS. APPLICATIONS WILL INCLUDE REASONING ABOUT MATHEMATICS SIGNAL PROCESSING, EMBEDDED SYSTEMS MANUFACTURING, & ROBOTICS.