reasoning with Horn clauses
(3.3 hours to learn)
Summary
Horn clauses are a restricted kind of formula in propositional or first-order logic which are computationally tractable, yet highly expressive. They form the core of programs in Prolog, a popular logic programming language. One can reason efficiently with Horn clauses using a combination of forward and backward chaining.
Context
This concept has the prerequisites:
- propositional satisfiability (Horn clauses can be used for inference in propositional logic.)
- first-order logic (Horn clauses are an important tool for inference in first-order logic.)
- first-order unification (Unification is a part of reasoning algorithms for first-order Horn clauses.)
Goals
- Define what a Horn clause is
- Know the forward chaining algorithm, and be able to simulate it on simple examples
- Know the backward chaining algorithm, and be able to simulate it on simple examples
- Why can naive backward chaining get stuck in infinite loops, and how can that be dealt with?
Core resources (read/watch one of the following)
-Paid-
→ Artificial Intelligence: a Modern Approach
A textbook giving a broad overview of all of AI.
- Section 7.5, "Reasoning patterns in propositional logic," subsection "Forward and backward chaining," pages 217-220
- Section 9.3, "Forward chaining," pages 280-287
- Section 9.4, "Backward chaining," pages 287-295
→ Knowledge Representation and Reasoning
An introductory textbook on knowledge representation.
Location:
Chapter 5, "Reasoning with Horn clauses," pages 85-95
See also
-No Additional Notes-