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.