Catalogue of Artificial Intelligence Techniques
Aliases: Condition-action Pairs, Demodulants
Keywords: matching, rule of inference, substitution
Categories: Automatic Programming , Inference and Reasoning , Theorem Proving
Author(s): Lincoln Wallen
Rewrite rules are sets of ordered pairs of expressions
usually depicted as (lhs rhs). There is usually a similarity relation between the `lhs' and the `rhs' such as equality, inequality or double implication. Rewrite rules, as the pairs are called, together with the rewriting rule of inference allow one expression to be `rewritten' into another. A subexpression of the initial expression is matched with the `lhs' of the rewrite rule yielding a substitution. The resulting expression is the expression obtained by replacing the distinguished subexpression with the `rhs' of the rewrite rule after applying the substitution. The matching process may be full Unification or, more usually, a restricted form of Pattern Matching where only the variables in the rewrite rule may be instantiated. Examples of the use of rewrite rules are the restricted Paramodulation inferences called demodulation performed in theorem provers, or programming with abstract data types introduced by a series of equations. Some powerful theoretical results have been obtained for rewriting systems.
- Huet, G. and Oppen, D.C., Equations and Rewrite Rules: A Survey, Formal Language Theory: Perceptives and Open Problems (Book, R.V.
, ed.), Academic Press, 1980.