Rhetorical Knowledge Representation System Reference Manual (for Rhet Version17.9)

摘要

Rhetorical (Rhet) is a programming / knowledge representation system that offersa set of tools for building automated reasoning systems. It's emphasis is on flexibility of representation, allowing the user to decide if the system will basically operate as a theorem prover, a frame-like system, or an associative network. Rhet may be used as the back-end to a user's programming system and handle the knowledge representation chores, or it may be used as a full-blown programming language. Rhet offers two major modes of inference: a horn clause theorem prover (backwards chaining mechanism), and a forward chaining mechanism. Both modes use a common representation of facts, namely horn clauses with universally quantified, potentially type restricted, variables, and use the unification algorithm. Additionally, they both share the following additional specialized reasoning capabilities: (1) variables may be typed with a fairly general type theory, that allows a limited calculus of types including intersection and subtraction; (2) full reasoning about equality between ground terms; (3) reasoning within a context space, with access to axioms and terms in parent contexts; and (4) escapes into Lisp for use as necessary.