补充资料：代换法则

代换法则
substitution rule

　　代换法则[s一山stituti叨n此:，10及eT阴oB阴np姗加]，亦称代换规则 逻辑一数学演算中的推导法则(derjvation rLde)之一代换法则有各种不同形式.例如，在命题演算(proposit，0，1:LI ealculus)中，代换法则是用一个公式代换命题变兀在命题公式中的所有的出现.在谓词演算戈Pfe山cate calculus)中，它是:a)用一个公式代换谓词公式中的谓词变元(predieatev::riable)(这里需要遵守一系列关于个体变元出现的限制以避免变元碰撞(二1llable collision)，即出现在公式中的自由变元通过代换变为约束变元);b)项的代换法则是用一个项代换渭同公式中相应类型的个体变元的自由出现(这里也必须避兔变兀碰撞).
　　

说明：补充资料仅用于学习参考，请勿用于其它任何用途。