The HORNE Reasoning System. Revision
James F. Allen, Mark Giuliano, Alan M. Frisch · 1984
HORNE is a programming system that offers a set of tools for building automated reasoning systems. It offers three major modes of inference; (1) a horn clause theorem prover (backwards chaining mechanism); (2) a forward chaining mechanism; and (3) a mechanism for restricting the range of variables with arbitrary predicates. All three modes use a common representation of facts, namely horn clauses with universally quantified variables, and use the unification algorithm. Also they all share the following additional specialized reasoning capabilities: (1) variables may be typed with a fairly general type theory that allows intersecting types; (2) full reasoning about equality between ground terms, and limited equality reasoning for quantified terms; and (3) escapes into LISP for use as necessary. This paper contains an introduction to each of these facilities, and the HORNE User's Manual.