Un caz special al formulei

Un caz special de formule

Dacă înlocuim formule în loc de variabile în formula , respectiv, atunci obținem o formulă , care se numește un caz special al formulei : $A(x_1,\dots,x_n)$ $x_1,\dots,x_n$ $B_1,\dots,B_n$ $B$ $A$

B = A(\dots,x_i,\dots)\{B_i//x_i\}^n_{i=1}

Fiecare formulă este înlocuită pentru toate aparițiile variabilei . $B_{i}$ $x_{i}$

Mulțimea substituțiilor se numește unificator . $\{B_i//x_i\}^n_{i=1}$

Un caz special al unui set de formule

Un set de formule se numește un caz special al unui set de formule dacă fiecare formulă este un caz special al unei formule cu același set de substituții. $B_1,\dots,B_n$ $A_1,\dots,A_n$ $B_{i}$ $A_{i}$

Un caz special comun de formule

O formulă se numește un caz special comun de formule și dacă este un caz special al unei formule și în același timp un caz special al unei formule cu același set de substituții, adică $C$ $A$ $B$ $C$ $A$ $B$

C = A(\dots,x_i,\dots)\{X_i//x_i\}^n_{i=1} \land C = B(\dots,x_i,\dots)\{X_i//x_i\}^ n_{i=1}

Formulele care au un caz special comun se numesc unificatori , iar o mulțime de substituții care produce un caz special comun de formule unificabile se numește unificator general . $\{X_i//x_i\}^n_{i=1}$

Un caz special comun al unui set de formule

Un set de formule se numește un caz special comun de seturi de formule și dacă fiecare formulă este un caz special de formule și cu același set de substituții. $C_1,\dots,C_n$ $A_1,\dots,A_n$ $B_1,\dots,B_n$ $C_{i}$ $A_{i}$ $B_{i}$

Sarcina unificării

Sarcina unificării este de a determina dacă două formule sunt un caz special al aceleiași, în special, una al celeilalte.

Problema este de nerezolvată din punct de vedere algoritmic în cazul general dacă se folosesc termeni de ordine superioară (adică semne de funcții).

Vezi și

Caz special (logica)