baza de Herbrand

În logica matematică , pentru fiecare limbaj de design , cu un set de termeni din " Herbrand univers , baza Herbrand definește recursiv mulțimea tuturor formulelor atomice care pot fi combinate pentru a forma predicat de termenii Herbrand univers. O Herbrand de bază a unui limbaj de ordinul I $L$ ${\ displaystyle L}$ $L$ poate fi construit din universul Herbrand lui $L$ ${\ displaystyle L}$ $L$ , Aplicarea fiecăruia dintre elementele sale unele predicatul $L$ ${\ displaystyle L}$ $L$ . Prin urmare, este mulțimea tuturor atomilor la sol , care pot fi construite folosind simboluri din $L$ ${\ displaystyle L}$ $L$ . Este numit după Jacques Herbrand . În baza de Herbrand lui, fiecare element este numit un atom.

O interpretare $H(S)$ ${\ H displaystyle (S)}$ ${\ H displaystyle (S)}$ este completă pentru toate clauzele $S.$ ${\ displaystyle S}$ $S.$ atunci când o valoare de adevăr este atribuit fiecărui atom din bază.

Baza Herband este un set numărabilă, elementele care pot fi comandate. De exemplu, ele pot fi aranjate într-o secvență ordonată $\{P1,P2,\ldots ,Pn\}$ ${\ Displaystyle \ {P1, P2, \ ldots, Pn \}}$ ${\ Displaystyle \ {P1, P2, \ ldots, Pn \}}$ .

Termeni Herbrand și atomi

Având în vedere o limbă $L(po)$ ${\ L displaystyle (po)}$ ${\ L displaystyle (po)}$ , Un termen Herbrand este un termen de bază (sol termen, adică un termen care nu conține variabile)

Exemple: $f(a)$ ${\ displaystyle f (a)}$ $face)$ , $g(a,b)$ ${\ Displaystyle g (a, b)}$ ${\ Displaystyle g (a, b)}$ , $g(f(a),b)$ ${\ Displaystyle g (f (a), b)}$ ${\ Displaystyle g (f (a), b)}$ , $g(f(a),g(b,c))$ ${\ Displaystyle g (f (a), g (b, c))}$ ${\ Displaystyle g (f (a), g (b, c))}$ , $g(f(a),g(f(b),c))$ ${\ Displaystyle g (f (a), g (f (b), c))}$ ${\ Displaystyle g (f (a), g (f (b), c))}$ , ...

Atom A Herbrand este un atom bazic (atom sol, adică un atom care nu conține variabile)

Exemple: $P(f(a))$ ${\ Displaystyle P (f (a))}$ ${\ Displaystyle P (f (a))}$ , $P(g(a,b))$ ${\ P displaystyle (g (a, b))}$ ${\ P displaystyle (g (a, b))}$ , $Q(g(f(a),b)$ ${\ Q displaystyle (g (f (a), b)}$ ${\ Q displaystyle (g (f (a), b)}$ , $g(f(a),g(b,c)))$ ${\ Displaystyle g (f (a), g (b, c)))}$ ${\ Displaystyle g (f (a), g (b, c)))}$ , ...

Herbrand univers și baza

Herbrand Universul este multimea tuturor termenilor Herbrand. Exemplu: $U(H)=\{a,b,c,f(a),g(a,b),g(f(a),b),g(f(a),g(b,c)),g(f(a),g(f(b),c)),\dots \}$ ${\ Displaystyle U (H) = \ {a, b, c, f (a), g (a, b), g (f (a), b), g (f (a), g (b, c )), g (f (a), g (f (b), c)), \ dots \}}$ ${\ Displaystyle U (H) = \ {a, b, c, f (a), g (a, b), g (f (a), b), g (f (a), g (b, c )), g (f (a), g (f (b), c)), \ dots \}}$

Baza Herbrand este multimea tuturor atomilor Herbrand. Exemplu: $B(H)=\{P(a),P(b),P(c),P(f(a)),P(g(a,b)),Q(g(f(a),b),g(f(a),g(b,c))),\dots \}.$ ${\ Displaystyle B (H) = \ {P (a), P (b), P (c), P (f (a)), P (g (a, b)), Q (g (f (a ), b), g (f (a), g (b, c))), \ dots \}.}$ ${\ Displaystyle B (H) = \ {P (a), P (b), P (c), P (f (a)), P (g (a, b)), Q (g (f (a ), b), g (f (a), g (b, c))), \ dots \}.}$

sisteme de Herbrand

Având în vedere o declarație universală, de forma $\forall x_{1}\forall x_{2}\dots \forall x_{n}\varphi$ ${\ Displaystyle \ forall X_ {1} \ forall X_ {} \ dots \ forall X_ {n} \ varphi 2}$ ${\ Displaystyle \ forall X_ {1} \ forall X_ {} \ dots \ forall X_ {n} \ varphi 2}$ ( $\varphi$ ${\ displaystyle \ varphi}$ $\ varphi$ nu conține cuantificatorii), sistemul Herbrand este setul (chiar infinit) formulelor închise generate de substituție $\varphi [x_{1}/t_{1},x_{2}/t_{2},\dots ,x_{n}/t_{n}]$ ${\ Displaystyle \ varphi [X_ {1} / {1} T_, X_ {2} / T_ {2}, \ dots, X_ {n} / T_ {n}]}$ ${\ Displaystyle \ varphi [X_ {1} / {1} T_, X_ {2} / T_ {2}, \ dots, X_ {n} / T_ {n}]}$ cu toate combinațiile posibile $<t_{1},t_{2},\ldots ,t_{n}>$ ${\ Displaystyle <T_ {1}, {2} T_, \ ldots, T_ {n}>}$ ${\ Displaystyle <T_ {1}, {2} T_, \ ldots, T_ {n}>}$ din $t(i)$ ${\ T displaystyle (i)}$ ${\ T displaystyle (i)}$ aparținând $U(H)$ ${\ Displaystyle U (H)}$ ${\ Displaystyle U (H)}$ . Exemple:

H(\forall xP(x)\in Q(x)))=\{P(f(a))\in Q(f(a)),P(g(a,b))\in Q(g(a,b)),\ldots \}

{\ Displaystyle H (\ forall xP (x) \ în Q (x))) = \ {P (f (a)) \ în Q (f (a)), P (g (a, b)) \ în Q (g (a, b)), \ ldots \}}

{\ Displaystyle H (\ forall xP (x) \ în Q (x))) = \ {P (f (a)) \ în Q (f (a)), P (g (a, b)) \ în Q (g (a, b)), \ ldots \}}

H(\forall x\forall yR(x,y))=\{R(f(a),f(a)),R(g(a,b),f(a)),R(f(a),g(a,b)),\ldots \}.

{\ Displaystyle H (\ forall x \ forall Yr (x, y)) = \ {R (f (a), f (a)), R (g (a, b), f (a)), R ( f (a), g (a, b)), \ ldots \}.}

{\ Displaystyle H (\ forall x \ forall Yr (x, y)) = \ {R (f (a), f (a)), R (g (a, b), f (a)), R ( f (a), g (a, b)), \ ldots \}.}

Sistemul Herbrand al unei teorii

Având în vedere o teorie $\Sigma$ ${\ displaystyle \ Sigma}$ $\ Sigma$ de propoziții universale, sistemul Herbrand al teoriei $\Sigma$ ${\ displaystyle \ Sigma}$ $\ Sigma$ este uniunea $H(\Sigma )$ ${\ H displaystyle (\ Sigma)}$ ${\ H displaystyle (\ Sigma)}$ a tuturor sistemelor Herbrand generate de rostirile $\Sigma$ ${\ displaystyle \ Sigma}$ $\ Sigma$ .

Exemplu:

\Sigma =\{\varphi ,\psi ,X\}

{\ Displaystyle \ Sigma = \ {\ varphi, \ psi, X \}}

{\ Displaystyle \ Sigma = \ {\ varphi, \ psi, X \}}

H\left(\Sigma \right)=H(\varphi )\bigcup H(\psi )\bigcup H(X).

{\ Displaystyle H \ left (\ Sigma \ dreapta) = H (\ varphi) \ bigcup H (\ psi) \ bigcup H (X).}

{\ Displaystyle H \ left (\ Sigma \ dreapta) = H (\ varphi) \ bigcup H (\ psi) \ bigcup H (X).}

Teorema lui Herbrand

O declarație universală $\forall x_{1}\cdots \forall x_{n}\ \varphi$ ${\ Displaystyle \ forall X_ {1} \ cdots \ forall X_ {n} \ \ varphi}$ ${\ Displaystyle \ forall X_ {1} \ cdots \ forall X_ {n} \ \ varphi}$ este și numai în cazul în care se cauta una în cazul în care există un subset finit de $H(\varphi )$ ${\ Displaystyle H (\ varphi)}$ ${\ Displaystyle H (\ varphi)}$ contradictoriu în sensul logicii propozițiilor.

Teorema lui Herbrand este importantă deoarece reduce satisfiabilitate / valabilitate (acestea sunt concepte duale, de fapt $\varphi$ ${\ displaystyle \ varphi}$ $\ varphi$ este satisfiable dacă și numai dacă $\neg \varphi$ ${\ displaystyle \ neg \ varphi}$ ${\ displaystyle \ neg \ varphi}$ Nu este logic validă) a primei logica predicatelor de ordinul a logicii propoziționale, deoarece pentru fiecare formulă este o formulă universală equisoddisfacibile ( Skolem formă normală ). Acesta prevede , de asemenea , o metodă de semi-decizie (și nu de decizie, ca " Entscheidungsproblem este indecidabila) pentru a testa satisfiable / validitatea unei formule logicii predicatelor de ordinul întâi.

Corolar (Horn forma clauza)

Este $\tau$ ${\ displaystyle \ tau}$ $\ tau$ un set de clauze Horn, următoarele afirmații sunt echivalente:

$\tau$ ${\ displaystyle \ tau}$ $\ tau$ este satisfiable.
$\tau$ ${\ displaystyle \ tau}$ $\ tau$ are un model Herbrand.

Trebuie remarcat faptul că se afirmă că $\tau$ ${\ displaystyle \ tau}$ $\ tau$ are un model Herbrand, nu $H(\tau )$ ${\ Displaystyle H (\ tau)}$ ${\ Displaystyle H (\ tau)}$ . Ea nu se aplică în general: numai dacă $\tau$ ${\ displaystyle \ tau}$ $\ tau$ este un set de clauze Horn. În această formă (finită), este aproape o procedură reală.

Portalul de matematică : accesați intrările Wikipedia care se ocupă de matematică