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; (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.
Document Details
- Document Type
- Technical Report
- Publication Date
- Sep 01, 1984
- Accession Number
- ADA150983
Entities
People
- A. M. Frisch
- J. F. Allen
- M. Giuliano
Organizations
- University of Rochester