代入_谓词演算的基本运算 - 国学百科m.yc-ky.net

代入

谓词演算的基本运算

代入是谓词演算自由变元时需对该变元的所有自由出现进行替换。

定义

在某个形式语言中，一个元素中某个出现（子项）被另一个元素项所代换。

例如，s 为一个项，x 为 s 中的（子）项，于是 s 可写成。如果用另一个项 a 代替 x ，即变为。这时就说是用 a 代入的结果。有时可将这个代入的结果写成或。

如果 s 中的 n 个项被另外 n 个项代替，这样代入的结果可写成。

替换

假定为任一公式，A为非空集。如果对一切，存在唯一的y使得成立，则存在定义域为A的函数f，使得对一切，成立。这就是替换引理。

代入消元法

代入消元法是将方程组中的一个方程的未知数用含有另一个未知数的代数式表示，并代入到另一个方程中去，这就消去了一个未知数,得到一个解。代入消元法简称代入法。

参考资料

谓词逻辑.清华大学主页.2022-11-15

最新修订时间：2025-10-06 22:45

条目作者

概述

定义

替换

代入消元法

参考资料