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:

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-

See also

-No Additional Notes-