ユニフィケーション
Prolog では、大文字で始まるシンボルは変数名、小文字で始まるシンボルは関数名を表し、カンマは論理積として使われる。数学の慣習では小文字だけを使い、アルファベットの最後の方(たとえば x,y,z)は変数名、f,g,h といった文字は関数記号、a,b,c といった文字は定数を意味し、定数は引数を持たない関数とみなされる。論理積は & または ∧ {\displaystyle \land } で表される。
置換は、変数から項へのマッピングの有限集合 { x 1 ↦ t 1 , ... , x k ↦ t k } {\displaystyle \{x_{1}\mapsto t_{1},\dots ,x_{k}\mapsto t_{k}\}} と定義され、1つの変数を2つの異なる項にマッピングすると曖昧さが生じるため、個々のマッピングは一意的でなければならない。項 u への置換の「適用」を u { x 1 ↦ t 1 , ... , x k ↦ t k } {\displaystyle u\{x_{1}\mapsto t_{1},\dots ,x_{k}\mapsto t_{k}\}} と記述し、項 u {\displaystyle u} に出現する各変数 x i {\displaystyle x_{i}} を項 t i {\displaystyle t_{i}} で置き換えることを意味する。このとき、 1 ≤ i ≤ k {\displaystyle 1\leq i\leq k} である。例えば、 f ( x , a , g ( z ) , y ) { x ↦ h ( a , y ) , z ↦ b } = f ( h ( a , y ) , a , g ( b ) , y ) {\displaystyle f(x,a,g(z),y)\{x\mapsto h(a,y),z\mapsto b\}=f(h(a,y),a,g(b),y)} となる。