If we wish to prove a sentence of the form

A [] ( X) t1 = t2where [] indicates that the signature involved is , then it suffices to prove the sentence

A [(X)] t1 = t2where [](X) indicates the signature formed from [] by adding the variables in X as new constants.

Use of this rule is justified by the so called "Theorem of Constants," see
Chapter 8 of
*Theorem Proving and Algebra*.

[Next] [Prev] [Home] [BHome]

12 October 1996