with Changing Equations
|Yishai A. Feldman
|Dept. of Computer Science
||Mitsubishi Electric Research Labs
|Tel Aviv University
|69978 Tel Aviv, Israel
||Cambridge, MA 02139, U.S.A.
Appeared in: J. Automated Reasoning, 7, 1991, 403-433
Pattern-directed invocation is a commonly used artificial-intelligence
reasoning technique in which a procedure, called a demon, is automatically
invoked whenever a term matching its pattern appears in a ground data base. For
completeness, if the data base includes equations, a demon needs to be invoked not only
when a term in the data base exactly matches its pattern, but also when some variant of a
term in the data base matches. An incremental algorithm has been developed for invoking
demons in this situation without generating all possible variants of terms in the data
base. The algorithm is shown to be complete for a class of demons, called transparent
demons, that obey a natural restriction between the pattern and the body of the demon.
Completeness is maintained when new demons, terms, or equations are added to the data base
in any order. Equations can also be retracted via a truth maintenance system. The
algorithm has been implemented as part of a reasoning system called BREAD.