Pattern-Directed Invocation with Equations


Pattern-Directed Invocation
with Changing Equations

Yishai A. Feldman and Charles Rich
Dept. of Computer Science Mitsubishi Electric Research Labs
Tel Aviv University 201 Broadway
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.