Catalogue of Artificial Intelligence Techniques

View Maths as: Images | MathML

Rewrite Rules

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 $⟨$

lhs,rhs$⟩$

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.

References:

• 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.