56 3 Rules and Inference
pared with programming in forward-chaining mode or programming with a
procedural language.
Forward-chaining engines behave much more like the protein-substrate
binding process introduced at the beginning of this chapter. Modern forward-
chaining rule engines are nearly always based on the Rete algorithm intro-
duced by (Forgy 1982). The Rete algorithm processes the rules and facts with
a network of interrelationships that captures all of the ways that rules can be
fired, either fully or in part. By capturing partially fired rules, it is much eas-
ier to introduce new facts. The Rete network matches the new fact against all
of the partially fired rules to determine whether it can be extended to form a
rule that fires or at least is closer to firing.Summary
- Both forward- and backward-chaining rule engines require a set of rules
and an initial knowledge base of facts. - Forward-chaining rule engines apply rules which cause more facts to be
asserted until no more rules apply. One can then query the knowledge
base. - Backward-chaining rule engines begin with a query and attempt to satisfy
it, proceeding backward from the query to the knowledge base.
3.3 Theorem Provers and Other Reasoners
As the name suggests, atheorem proverattempts to prove theorems. A pro-
gram consists of a theory expressed using axioms and facts. A conjecture is
presented to the system, and the theorem prover attempts to find a proof. A
proofconsists of a sequence of rule invocations which start with the axioms
and end with the conjecture. A proved conjecture is called a theorem. Con-
jectures can be regarded as queries, and the theorem-proving process is a
mechanism for answering the queries. However, this is not quite the same as
the query mechanism supported by rule engines or relational databases. In
the latter systems, the result of a query is the set of ways that it can be satis-
fied, not whether it can be satisfied. Theorem provers are not usually capable
of dealing with queries in the same way as a relational database system.
To illustrate this distinction between theorem provers and rule engines,
consider the case of consistency checking. This is an important problem for