Automated Reasoning: Theory and Application Course

Program Overview

COM SCI XLC 264A: Automated Reasoning: Theory and Applications introduces students to the theory and practice of automated reasoning using propositional and first-order logic. The course covers topics such as syntax and semantics of formal logic, algorithms for logical reasoning, and applications in various fields. Students will gain hands-on experience through laboratory sessions and explore the impact of syntactic and semantic restrictions on knowledge bases.

Program Outline

Outline:

Automated Reasoning: Theory and Applications

-Course Overview:

Introduction to theory and practice of automated reasoning using propositional and first-order logic. Topics include syntax and semantics of formal logic; algorithms for logical reasoning, including satisfiability and entailment; syntactic and semantic restrictions on knowledge bases; effect of these restrictions on expressiveness, compactness, and computational tractability; applications of automated reasoning to diagnosis, planning, design, formal verification, and reliability analysis.

-Course Structure and Schedule:

Lecture: four hours; laboratory, four hours; outside study, four hours.

-Modules:

• Syntax and semantics of formal logic
• Algorithms for logical reasoning
• Satisfiability and entailment
• Syntactic and semantic restrictions on knowledge bases
• Effect of these restrictions on expressiveness, compactness, and computational tractability
• Applications of automated reasoning to diagnosis, planning, design, formal verification, and reliability analysis