HORNE is a programming system that offers a set of tools for building automated reasoning systems. It offers three major modes of inference: a horn clause theorem prover (backwards chaining mechanism); a forward chaining mechanism; and 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. (jhd)