# 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-