The HORNE Reasoning System. Revision
Abstract
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)
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1984
- Accession Number
- ADA221796
Entities
People
- Alan M. Frisch
- James F. Allen
- Mark Giuliano
Organizations
- University of Rochester