代入

在某個形式語言中，一個元素中某個出現（子項）被另一個子項所代換。

例如，s 為一個項，x 為 s 中的（子）項，於是 s 可寫成 。如果用另一個項目a 代替 x ，即 變為 。這時就說 使用 a 代入 的結果。有時可將這個代入的結果寫成 或 。

如果s中的n個項被另外 n 個項代替，這樣代入的結果可寫成 。

假定 為任一公式，A為非空集。如果對一切 ，存在唯一的y使得 成立，則存在定義域為A的函數f，使得對一切， 成立。這就是替換引理。

代入消元法是將方程組中的一個方程的未知數用含有另一個未知數的代數式表示，並代入到另一個方程中去，這就消去了一個未知數，得到一個解。代入消元法簡稱代入法。