2-7谓词演算推理理论
消去和添加量词规则：
US(全称指定规则)：                (x)G(x)G(c)ES(存在指定规则)：                (x)G(x)G(c)UG(全称推广规则)：                G(y)(x)G(x)EG(存在推广规则)：                G(c)(x)G(x)                                               
US全称指定规则，书写形式：                (x)G(x)G(c)        成立条件是：c为任意个体常量。

ES(存在指定规则) ，书写形式：                (x)G(x)G(c)                        成立条件是：c是使G(x)为真特定个体常量。c不在前提中或者居先推导公式中出现或自由出现，换句话说，此c是在该推导之前从未使用过。