Universal Quantifier Elimination
If we wish to prove a sentence of the form 
    A [] ( X) t1 = t2
where [] indicates that the signature involved is , then it suffices to prove the sentence 
    A [(X)] t1 = t2
where [](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