reasoning with Horn clauses
(3.3 hours to learn)
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.
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.)
- 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)
→ 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
-No Additional Notes-
- create concept: shift + click on graph
- change concept title: shift + click on existing concept
- link together concepts: shift + click drag from one concept to another
- remove concept from graph: click on concept then press delete/backspace
- add associated content to concept: click the small circle that appears on the node when hovering over it
- other actions: use the icons in the upper right corner to optimize the graph placement, preview the graph, or download a json representation