Kihagyás

Rezolúciós dolog

\[ S = \left\{\neg A \lor B, \neg A \lor C, A \lor C, \neg B \lor C, \neg C\right\} \]
\[\begin{array}{lll} 1. & \neg C & [\in S] \\ 2. & A \lor C & [\in S] \\ 3. & A & \left[\text{res(1,2)}\right] \\ 4. & \neg A \lor C &\left[\in S\right] \\ 5. & C & \left[\text{res}(3,4)\right] \\ 6. & \square & \left[\text{res}(1,5)\right]\\ \end{array} \]

1. Rend

Prenex formula

Legyen \(Q\) tetszőleges kvantor, a \(Q_1x_1, Q_2x_2, \dots, Q_nx_n, B\) formula.

\(Q_1x_1, Q_2x_2, \dots, Q_nx_n,\) prefixum, a formula magja, törzse \(B\), kvantormentes formula.

Skolem normálforma

Skolem formula a \(\forall x_{1}, \forall x_{2} \dots , \forall x_{n} A\) formula, ahol a prefixumban csak univerzális kvantorok szereplenek.

Ez eldönthető formulaosztály.

Elsődrendű klóz

Olyan zárt Skolem formula, aminek a majga az elsődrendű nyelv literáljánák diszjunkciója Pl.: $\forall x\forall y(P(x)\lor\neg Q(x, f(y))) $

Átalakítások

  • Tetszőleges formula átalakítható prenex alakba
  • Tetszőleges prenex formula átalakítható Skolem alakba
  • Tetszőleges Skolem normálforma felírható elsőrendű klózok konjunkciójaként

Prenex formula: DeMorgan szabályok és kvantorkiemelés szabályokkal

Általános De Morgan Szabályok

\[\begin{array}{clcr} &\neg \forall x A & \sim & \exists x \neg A \\ &\neg \exists x A & \sim & \forall x \neg A \\ \end{array} \]

Kvantorkiemelési szabályok

\[\begin{array}{clcll} (1)& \forall x A[x]\land B & \sim &\forall x(A[x]\land B) & \\ & \forall x A[x]\lor B & \sim &\forall x(A[x]\lor B) & \\ (2)&\exist x A[x] \land B & \sim &\exist x(A[x] \land B) & \\ &\exist x A[x] \lor B & \sim & \exist x(A[x] \lor B) & \\ (3)& \forall x A[x]\land \forall x B[x] & \sim & \forall x (A[x] \land B[x]) & \text{De $\lor$-ra nem}\\ (4)& \exist x A[x]\lor \exist x B[x] & \sim & \exist x (A[x] \lor B[x]) & \text{De $\land$-re nem}\\ (5)& Q_1xA[x]\land Q_2xB[x] & \sim & Q_1xQ_2z(A[x]\land B[x/z]) & \\ (6)& Q_1xA[x]\lor Q_2xB[x]& \sim & Q_1xQ_2z(A[x]\lor B[x/z]) & \\ \end{array} \]
\[ The Game \]