\documentclass[draft,a4paper]{article}
\usepackage{lt}
\usepackage{amsmath}
\usepackage{latexsym}
\usepackage{multicol}
\title{Diskrečiosios matematikos konspektai}
\author{Marius Gedminas}
\date{2003 m. pavasaris\\ (VU informatikos magistrantūros studijų 2 semestras)}

\newcommand{\Def}{\emph}
\newcommand{\true}{\mathbf{t}}
\newcommand{\false}{\mathbf{f}}
\renewcommand{\land}{\mathop{\&}}

\begin{document}
\maketitle

% XXX: ei, disjunktai ar disjungtai?

% ----------------------------------------------------------------------------

\section{Formulės}

Apibrėžimas: \Def{$n$-viečiu predikatu} aibėje $M$ vadiname funkciją $P: M^n
\to \{\true, \false\}$.  Aibė $M$ vadinama \Def{individinių konstantų aibe}.

\Def{Predikatinis kintamasis} yra predikatas (ne koks nors konkrečiai, o
apskritai).

\Def{Formulė} apibrėžiama taip:
\begin{enumerate}
\item $P$ -- formulė, jei $P$ yra predikatinis kintamasis.
\item $\neg F$ -- formulė, jei $F$ -- formulė.
\item $(F \land G)$, $(F \lor G)$, $(F \to G)$ yra formulės, jei $F$ ir $G$
yra formulės.
\item $\forall x F$, $\exists x F$ (skaitoma „visiems $x$“, „egzistuoja $x$“)
yra formulės, jei $F$ yra formulė.
\item $\Box F$, $\Diamond F$ (skaitoma „būtinai $F$“, „galbūt $F$“) yra
formulės, jei $F$ yra formulė.
\end{enumerate}

Punktai 1--4 apibrėžia predikatų logiką, 1--5 --- modalumo logiką.

$\Box F$, $\Diamond F$ galima interpretuoti įvairiai, pvz.,
„visada“/„kartais“, „visur“/„kai kur“.  Semantika nusakoma aksiomomis, pvz.,
$\Box F \to F$, $F \to \Diamond F$.

Ateityje dar bus laiko logika: $\odot F$ („kitas $F$“).
% FIXME: ten ne \odot o tiesiog tuščio tokio dydžio apskritimo reikia.
% \circ yra per mažas, \Bigcirc per didelis.  :(

$\forall$, $\exists$ vadinami \Def{kvantoriais}, $\Box$, $\Diamond$ --
\Def{operatoriais}.

Sąvokos:
% XXX reiktų apibrėžti.
\begin{itemize}
\item kvantorių bei operatorių \Def{veikimo sritis}
\item operatoriaus \Def{įeitis} (angl. occurrence)
\item įeities veikimo sritis
\item \Def{laisvoji} ir \Def{suvaržytoji} individinio kintamojo įeitis
      (suvaržytoji -- jei patenka į atitinkamo kvantoriaus veikimo sritį).
      Kad būtų paprasčiau, tarkime, jog reiš\-ki\-niai a la $\forall x (P(x)
      \land \exists x Q(x))$ nelegalūs.
\end{itemize}

Formulė vadinama \Def{uždaraja}, jei ji neturi laisvų kintamųjų įeičių.

% ----------------------------------------------------------------------------

\section{Semantika}

\Def{Struktūra} (arba \Def{interpretacija}) yra rinkinys
\[S = \langle M; Q_1, \dots, Q_n; x_1, \dots, x_m\rangle\]
kur $M$ -- individinių konstantų aibė, $Q_i$ -- predikatai, $x_j$ -- konkretūs
$M$ elementai.

Formulė $F$ yra \Def{įvykdoma struktūroje $S$}, jei pakeitę formulėje
predikatus į $Q_i$, o laisvus kintamuosius į $x_j$ turime teisingą formulę.

Pvz.: $\forall x \forall y \forall z ((P(x,y) \land P(y,z)) \to P(x,z)))$
yra įvykdoma struktūroje $S = \langle R; x<y \rangle$.

Pvz.: $\forall x \exists y (P(x,y) \land \neg \forall z P(z,z))$ yra įvykdoma
struktūroje $S = \langle N; x < y \rangle$.

Pvz.: $Q(x, x, x)$ yra įvykdoma struktūroje $S = \langle Z; x = y = z; 0
\rangle$ arba $S = \langle R; x^2 + y^2 = z^2; 0 \rangle$.

Pvz.: $\forall x P(x, y) \to \exists z R(y, z, z)$ yra įvykdoma struktūroje $S
= \langle R; x > y, x = y = z; 0 \rangle$.

Formulė $F$ yra \Def{įvykdoma}, jei egzistuoja struktūra, kurioje ji yra
įvykdoma.

(Bendru atveju neįmanoma algoritmiškai nustatyti, ar formulė įvykdoma.)

Formulė $F$ yra \Def{tapačiai teisinga}, jei ji įvykdoma visose struktūrose.

Formulės $F$ ir $G$ yra \Def{ekvivalenčios} ($F \equiv G$), jei su kiekviena
struktūra jos yra kartu teisingos arba kartu klaidingos.

(Beje, ne visose logikose $\neg\neg F \equiv F$).

% ----------------------------------------------------------------------------

\section{Modalumo logikos semantika}

\newcommand{\Strukt}{\ensuremath{\langle M, R, \mathcal{V} \rangle}}

S. Kripke \Def{semantika}: \[ S = \Strukt \] kur $M$ -- galimų pasaulių aibė,
$R$ -- dvivietis predikatas (sąryšis) aibėje $M$ (rodo iš kurių pasaulių į
kuriuos galima patekti), $\mathcal{V}$ -- interpretacijų aibė (priklauso nuo
pasaulio).

Fiksuojame pasaulį $\alpha \in M$.  $\mathcal{V}$ suteikia reikšmes visiem
loginiams kintamiesiems šiame pasaulyje.

\begin{enumerate}

  \item Jei $F$ -- loginis kintamasis, formulė teisinga tada, kai ji teisinga
  pasaulyje $\alpha$.

  \item Jei $F = \neg G$, formulė teisinga tada, kai $G$ klaidinga pasaulyje
  $\alpha$.

  \item Jei $F = G \land H$, formulė teisinga tada, kai ir $G$ ir $H$
  teisingos pasaulyje $\alpha$.

  \item Jei $F = G \lor H$, formulė teisinga tada, kai bent viena iš $G$, $H$
  teisinga pasaulyje $\alpha$.

  \item Jei $F = G \to H$, formulė teisinga tada, kai $G$ teisinga arba $H$
  klaidinga pasaulyje $\alpha$.

  \item Jei $F = \Box G$, formulė teisinga tada, kai $G$ teisinga visuose
  pasauliuose $\alpha'$, kuriems $R(\alpha, \alpha') = \true$.

  \item Jei $F = \Diamond G$, formulė teisinga tada, kai atsiras bent vienas
  pasaulis $\alpha'$, toks, kad $R(\alpha, \alpha') = \true$ ir $G$ teisinga
  pasaulyje $\alpha'$.

\end{enumerate}

Formulė $F$ yra \Def{įvykdoma}, jei egzistuoja tokia struktūra $\Strukt$ ir
pasaulis $\alpha \in M$, kad $F$ įvykdoma pasaulyje $\alpha$.

Formulė $F$ yra \Def{tapačiai teisinga}, jei ji teisinga bet kurios struktūros
kiekviename pasaulyje.

Formulė $F$ yra \Def{tapačiai klaidinga}, jei ji klaidinga bet kurios
struktūros kiekviename pasaulyje.


Pvz.: $F = \Box p$.  $M$ -- pasaulio šalys.  $R(x, y) = \true$ tada ir tik
tada, kai valstybės $x$ ir $y$ turi bendrą sieną.  $p$ -- teiginys „sausis yra
šalčiausias mėnuo“.  Pasaulyje $\alpha = \text{Lietuva}$ $F$ prasmė yra
„visose Lietuvos kaimynėse sausis -- šalčiausias mėnuo“.  Šiame pasaulyje $F$
yra teisinga, o pvz., pasaulyje „Kongas“ ji yra klaidinga.

Pvz.: $F = p \to \Box\Box p$, $M$ -- sveikųjų skaičių aibė, $R(x, y) =
\true$ tada ir tik tada, kai $y = x + 1$, $p$ -- „pasaulis nusakomas neigiamu
skaičiumi“.  Kai $\alpha = -1$, $p = \true$, $\Box\Box p = \false$, o
formulė $F$ klaidinga.  ($\Box\Box p$ prasmė yra daugmaž ar $\alpha + 2
< 0$, ar ne.)


Formulės $F$ \Def{projekcija} $pr(F)$ gaunama išbraukus iš $F$ visas modalumo
logikos operatorių įeitis.

Pvz.: $F = p \to \Box\Diamond(q \lor \Box r)$, tada $pr(F) = p \to (q
\lor r)$.

Jei $pr(F)$ nėra tapačiai teisinga, tai $F$ taip pat nėra tapačiai teisinga
(bet ne at\-vir\-kš\-čiai).

$pr(F)$ ekvivalenti $F$ kai $M = \{\alpha\}$ ir $R(\alpha, \alpha) = \true$.

Pvz.: $M = Z$, $R(x, y) = (y = x+1) \lor (y = x+2)$, $p$ -- „pasaulis --
lyginis skaičius“, $q = \neg p$.  Pasaulyje 2 $\Box(p\lor q) = \true$,
$\Box p = \false$, $\Box q = \false$.


Formulės $F$ transformacija į teiginių logiką žymima $[F]_\tau$ ir
skaičiuojama pagal šias taisykles:
\begin{eqnarray*}
  [\Box F]_\tau &=& \forall v (R(\tau, v) \to [F]_v) \\{}
  [\Diamond F]_\tau &=& \exists v (R(\tau, v) \land [F]_v) \\{}
  [\neg F]_\tau &=& \neg [F]_\tau \\{}
  [F \land G]_\tau &=& [F]_\tau \land [G]_\tau \\{}
  [F \lor G]_\tau &=& [F]_\tau \lor [G]_\tau \\{}
  [F \to G]_\tau &=& [F]_\tau \to [G]_\tau \\{}
  [p]_\tau &=& P(\tau)
\end{eqnarray*}

Pvz.:
\begin{align*}
[\Box\Diamond p]_\tau &=
  \forall v (R(\tau, v) \to \exists u (R(v, u) \land P(u))), \\
[\Box p \to \Diamond (q \lor \Diamond r)]_\tau &=
  \forall v \big(R(\tau, v) \to P(\tau)\big) \to
  \\&\qquad \exists v \big(R(\tau, v) \land
                        \big(Q(v) \lor \exists u (R(v, u) \land Z(u))\big)\big).
\end{align*}

NB norint, kad formulė būtų teisinga ir pačiame pasaulyje, reikia, kad $R$ būtų
refleksyvus, t.y. $R(x, x) = \true$.  Tai galima nusakyti aksioma $\Box p
\to p$.

Jei norime $R$ tranzityvumo, t.y. $\forall x \forall y \forall z ((R(x, y)
\land R(y, z)) \to R(x, z))$, galime tai užrašyti aksioma $\Box p \to
\Box \Box p$.

% ----------------------------------------------------------------------------

\section{Hilberto tipo skaičivimas}

Nagrinėsime modalumo logikas, kuriose perėjimo funkcija $R(x, y)$ tenkina tam
tikrus apribojimus.  Du baziniai apribojimai, tinkantys visiems taikymams:
\begin{itemize}
\item refleksyvumas, t.y. $\forall x R(x, x)$
\item tranzityvumas, t.y. $\forall x \forall y \forall z ((R(x, y) \land R(y,
z)) \to R(x, z))$
\end{itemize}

Kaip patikrinti formulės $F$ tapatų teisingumą?  Vien tik struktūros
apibrėžimo nepakanka -- visų struktūrų neišrašysim, ten jau nebeskaiti aibė.
Vienas (vienintėlis iš žinomų) būdų -- įvairūs formalūs skaičiavimai, kuriose
įrodomos tik ir tik tapačiai teisingos formulės.  Tuomet galime ieškoti
įrodymo kuriame nors skaičiavime.

Yra sugalvoti trys skaičiavimai: Hilberto tipo, sekvenciniai ir rezoliucijų.
Juos galima pritaikyti įvairioms logikoms (klasikinei, predikatų, modalumo,
laiko).

Hilberto tipo skaičiavime naudojama tokia aksiomų sistema ($A, B, C$ --
formulės):
\begin{enumerate}
\item[1.1] $A \to (B \to A)$
\item[1.2] $(A \to (B \to C)) \to ((A \to B) \to (A \to C))$
\item[2.1] $(A \land B) \to A$
\item[2.2] $(A \land B) \to B$
\item[2.3] $(A \to B) \to ((A \to C) \to (A \to (B \land C)))$
\item[3.1] $A \to (A \lor B)$
\item[3.2] $B \to (A \lor B)$
\item[3.3] $(A \to C) \to ((B \to C) \to ((A \lor B) \to C))$
\item[4.1] $(A \to B) \to (\neg B \to \neg A)$
\item[4.2] $A \to \neg\neg A$
\item[4.3] $\neg\neg A \to A$
\item[5.1] $\Box(A \to B) \to (\Box A \to \Box B)$
\item[5.2] $\Box A \to A$ (refleksyvumas)
\item[5.3] $\Box A \to \Box \Box A$ (tranzityvumas).
% dar yra aksiomų su \Diamond, bet jos bus vėliau
\end{enumerate}
Aksiomos 1.1--4.3 aprašo teiginių logiką, 5.1--5.3 prideda modalumo logiką
Kadangi $\Diamond A \equiv \neg \Box \neg A$, o $\Box A \equiv \neg \Diamond
\neg A$, tad aksiomų pakanka.

Hilberto tipo skaičiavime yra dvi taisyklės:
\begin{enumerate}
\item \Def{MP} -- \Def{modus ponens}:
      $\displaystyle\frac{A, A\to B}{B}$
\item \Def{AT}:
      $\displaystyle\frac{A}{\Box A}$
\end{enumerate}
Teiginių logikai pakanka vienos modus ponens taisyklės.  Modalumo logikai
reikia ir antros.

Formulės $F$ \Def{išvedimas} $\vdash F$ -- baigtinė formulių seka $F_1, \dots,
F_n$, kad
\begin{enumerate}
\item $F_n = F$ ir
\item $\forall i$ arba $F_i$ -- aksioma, arba ji gauta pagal kurią nors
taisykle iš kairiau esančių formulių.
\end{enumerate}


Hilberto skaičiavimas -- bazinis, patogus teoriniams samprotavimams, o ne
praktiniam naudojimui.

Pvz.: Įrodykime, kad $\vdash A \to \Diamond A$, kitaip tariant, kad $\vdash A
\to \neg \Box \neg A$.
\begin{enumerate}
\item $\Box \neg A \to \neg A$ (aksioma 5.2)
\item $(\Box \neg A \to \neg A) \to (\neg \neg A \to \neg \Box \neg A)$
      (aksioma 4.1)
\item $\neg \neg A \to \neg \Box \neg A$ arba $\neg\neg A \to \Diamond A$ (MP
      iš 1 ir 2)
\item $A \to \neg \neg A$ (aksioma 4.2)
\item $A \to \Diamond A$ (implikacijos tranzityvumas, kurį reiktų sunkiai
      ir ilgai įrodinėti remiantis aksioma 1.2)
%\item $(A \to (\neg \neg A \to \neg \Box \neg A)) \to
%       ((A \to \neg \neg A) \to (A \to \neg \Box \neg A))$ (aksioma 1.2)
\end{enumerate}

% ----------------------------------------------------------------------------

\section{Sekvencinis skaičiavimas}

\Def{Sekvencija} yra reiškinys $\Gamma \vdash \Delta$, kur $\Gamma, \Delta$ --
(galbūt tuščios) baigtinės formulių aibės (formulių tvarka nesvarbi).

Aksioma:
\[ \Gamma_1, A, \Gamma_2 \vdash \Delta_1, A, \Delta_2 \]

Taisyklės:
\begin{multicols}{2}
\begin{enumerate}
\item $\displaystyle\frac{A, \Gamma \vdash \Delta}
                         {\Gamma \vdash \Delta, \neg A}$
\item $\displaystyle\frac{\Gamma \vdash \Delta, A}
                         {\neg A, \Gamma \vdash \Delta}$
\item $\displaystyle\frac{A, B, \Gamma \vdash \Delta}
                         {A \land B, \Gamma \vdash \Delta}$
\item $\displaystyle\frac{\Gamma \vdash \Delta, A \quad \Gamma \vdash \Delta, B}
                         {\Gamma \vdash \Delta, A \land B}$
\item $\displaystyle\frac{A, \Gamma \vdash \Delta \quad B, \Gamma \vdash \Delta}
                         {A \lor B, \Gamma \vdash \Delta}$
\item $\displaystyle\frac{\Gamma \vdash \Delta, A, B}
                         {\Gamma \vdash \Delta, A \lor B}$
\item $\displaystyle\frac{A, \Gamma \vdash \Delta, B}
                         {\Gamma \vdash \Delta, A \to B}$
\item $\displaystyle\frac{\Gamma \vdash \Delta, A \quad B, \Gamma \vdash \Delta}
                         {A \to B, \Gamma \vdash \Delta}$
\end{enumerate}
\end{multicols}

Išvedimas turi medžio pavidalą: pradedam iš apačios (nuo šaknies) $\Gamma
\vdash \Delta$ ir keliaujam aukštyn.  Sekvencija yra \Def{išvedama}, jei visos
šakos baigiasi aksiomomis.

Bet kokiai tapačiai teisingai formulei $F$ atsiras išvedimas $\vdash F$.

Kiekviena taisyklė panaikina vieną loginę operaciją, tad medžio gylis ribotas.

% FIXME: negražu...
\newcommand{\F}{\displaystyle\frac}
\newcommand{\U}{\underline}
Pvz.: $\vdash (A \land B) \to (A \lor B)$
\[
  \F{\F{\F{A, B \vdash A, B}
          {A \land B \vdash A, B}}
          {A \land B \vdash A \lor B}}
          {\vdash (A \land B) \to (A \lor B)}
\]

Kitas pvz:
\[
  \F{\F{\F{\F{B\to C, \U{A} \vdash \U{A}, C
              \quad \F{\U{B}, A \vdash \U{B}, C
                       \quad B, \U{C}, A \vdash \U{C}}
                      {B, B\to C, A \vdash C}}
             {A\to B, B\to C, A \vdash C}}
          {A\to B, B\to C \vdash A \to C}}
       {A\to B \vdash (B \to C) \to (A \to C)}}
    {\vdash (A\to B) \to ((B \to C) \to (A \to C))}
\]

% 2003-03-05

Dar vienas pvz:
\renewcommand{\F}[2]{\scriptstyle\frac{\scriptstyle #1}{\scriptstyle #2}}
\[
  \F{\F{(B \land C) \to D, \U{A}, B \vdash C \land D, \U{A}
        \quad \F{\dots}
                {B \to C, (B \land C) \to D, A, B \vdash C \land D}}
       {A \to (B\to C), (B \land C) \to D, A, B \vdash C \land D}}
    {A \to (B\to C), (B \land C) \to D, A \land B \vdash C \land D}
\]
kur
\[
  \F{(B \land C) \to D, A, \U{B} \vdash C \land D, \U{B}
     \quad \F{A, B, \U{C}, (B \land C) \to D \vdash \U{C}
              \quad \F{\dots}{A, B, C, (B \land C) \to D \vdash D}}
             {C, (B \land C) \to D, A, B \vdash C \land D}}
    {B \to C, (B \land C) \to D, A, B \vdash C \land D}
\]
kur
\[
  \F{\F{A, \U{B}, C \vdash \U{B}
        \quad A, B, \U{C} \vdash \U{C}}
       {A, B, C \vdash B \land C}
     \quad A, B, C, \U{D} \vdash \U{D}}
    {A, B, C, (B \land C) \to D \vdash D}
\]

Ir dar vienas
\renewcommand{\F}{\displaystyle\frac}
\[
  \F{\F{\F{\F{\U{B}, A \vdash C, D, \U{B}}
             {B \vdash C, D, A \to B}
           \quad \U{C}, B \vdash \U{C}, D}
          {(A \to B) \to C, B \vdash C, D}}
       {(A \to B) \to C, B \vdash C \lor D}}
    {(A \to B) \to C, \neg (C \lor D), B \vdash}
\]

Ilgą laiką nebuvo sekvencinio skaičiavimo pritaikymo modalumo logikai.  Štai
papildomos taisyklės:
\begin{multicols}{2}
\begin{enumerate}
\item[9.] $\displaystyle\frac{F, \Box F, \Gamma \vdash \Delta}
                             {\Box F, \Gamma \vdash \Delta}$
\item[10.] $\displaystyle\frac{\Box \Gamma \vdash F}
                              {\Sigma, \Box \Gamma \vdash \Delta, \Box F}$
\end{enumerate}
\end{multicols}
kur $\Box \Gamma$ -- visos formulės, kurios prasideda operatoriumi $\Box$;
$\Sigma$ -- visos kitos formulės.  Taisykles operatoriui $\Diamond$ galima
išsivesti.

Išvedimas sudėtingesnis, nes galima vienu keliu patekti į aklavietę, teks
grįžti ir bandyti kitaip.

% Gegužės priešpaskutinę savaitę trečiadienį kontrolinis, paskutinę savaitę
% aiškins, kas ir kaip.
% Iš mūsų 25 gaus įskaitas už taškelius.

Pvz.:
\[
  \F{\F{\F{\F{\U{p}, q, \Box(p \land q) \vdash \U{p}}
             {(p \land q), \Box(p \land q) \vdash p}}
          {\Box(p \land q) \vdash p}}
       {\Box(p \land q) \vdash \Box p} \quad
     \F{\F{\F{p, \U{q}, \Box(p \land q) \vdash \U{q}}
             {(p \land q), \Box(p \land q) \vdash q}}
          {\Box(p \land q) \vdash q}}
       {\Box(p \land q) \vdash \Box q}}
    {\Box(p \land q) \vdash \Box p \land \Box q}
\]

Pvz.:
\[
  \F{\F{\F{\F{\F{\F{\F{\F{\F{\Box \neg (A \lor \Box \neg A), \U{A} \vdash \U{A}, \Box \neg A }
                            {\Box \neg (A \lor \Box \neg A), A \vdash (A \lor \Box \neg A) }}
                         {\Box \neg (A \lor \Box \neg A), A, \neg (A \lor \Box \neg A) \vdash}}
                      {\Box \neg (A \lor \Box \neg A), A \vdash}}
                   {\Box \neg (A \lor \Box \neg A) \vdash \neg A}}
                {\Box \neg (A \lor \Box \neg A) \vdash A, \Box \neg A}}
             {\Box \neg (A \lor \Box \neg A) \vdash (A \lor \Box \neg A)}}
          {\neg (A \lor \Box \neg A), \Box \neg (A \lor \Box \neg A) \vdash}}
       {\Box \neg (A \lor \Box \neg A) \vdash}}
    {\vdash \neg \Box \neg (A \lor \Box \neg A)}
\]

NB $\Diamond A \equiv \neg \Box \neg A$.

Pabandykim įrodyti ekvivalentumus:
\begin{align*}
\Box \Box A \equiv \Box A\\
\Box \Diamond A \equiv \Diamond A\\
\Box \Diamond A \equiv \Box A
\end{align*}

% XXX bandymai pagražinti:
% \renewcommand{\F}[2]{{#1 \atop \overline{#2}}}
\[
\F{\Box{A}, \Box \Box A \vdash \U{\Box A}}
  {\Box \Box A \vdash \Box A}
\quad
\F{\U{\Box A} \vdash \U{\Box A}}
  {\Box A \vdash \Box \Box A}
\]

\[
\F{\U{\neg \Box \neg A}, \Box \neg \Box \neg A \vdash \U{\neg \Box \neg A}}
  {\Box \neg \Box \neg A \vdash \neg \Box \neg A}
\quad
\F{\text{neišeina}}
  {\neg \Box \neg A \vdash \Box \neg \Box \neg A}
\]

\[
\F{\text{neišeina}}
  {\Box \neg \Box \neg A \vdash \Box A}
\quad
\F{\F{\F{\F{\U{A}, \Box A, \Box \neg A \vdash \U{A}}
           {A, \neg A, \Box A, \Box \neg A \vdash}}
        {\Box A, \Box \neg A \vdash}}
     {\Box A \vdash \neg \Box \neg A}}
  {\Box A \vdash \Box \neg \Box \neg A}
\]

\section{Kvantorinė modalumo logika}

% Kalba, patogi žinių bazėms aprašyti -- modalumo logikos kalba.
% Kol kas mes išsiaiškinom modalumo logiką teiginiams.  Laikas pereiti prie
% predikatų.

Priminisime sekvencinio skaičiavimo taisykles modalumo logikos operatoriams:
\begin{multicols}{2}
\begin{enumerate}
\item[9.] $\displaystyle\frac{F, \Box F, \Gamma \vdash \Delta}
                             {\Box F, \Gamma \vdash \Delta}$
\item[10.] $\displaystyle\frac{\Box \Gamma \vdash F}
                              {\Sigma, \Box \Gamma \vdash \Delta, \Box F}$
\end{enumerate}
\end{multicols}
kvantorinė modalumo logika papildo jas šiomis:
\begin{enumerate}
\item[11.] $\displaystyle\frac{\Gamma \vdash \Delta, F(z)}
                              {\Gamma \vdash \Delta, \forall x F(x)}$
           \quad kur $z$ yra naujas kintamasis (nesutinkamas niekur kitur).
\item[12.] $\displaystyle\frac{\Gamma \vdash \Delta, F(u), \exists x F(x)}
                              {\Gamma \vdash \Delta, \exists x F(x)}$
           \quad čia $u$ -- bet koks laisvas kintamasis.
           % idėja: parenkam konkrečią reikšmę x = u ir bandom įrodyti, bet
           % jei neišeina, galime bandyti parinkti kitą reikšmę
% o šitie du simetriški (keliant į kitą pusę atsiranda neigimas)
\item[13.] $\displaystyle\frac{F(u), \forall x F(x), \Gamma \vdash \Delta}
                              {\forall x F(x), \Gamma \vdash \Delta}$
           \quad čia $u$ -- bet koks laisvas kintamasis.
\item[14.] $\displaystyle\frac{F(z), \Gamma \vdash \Delta}
                              {\exists x F(x), \Gamma \vdash \Delta}$
           \quad kur $z$ yra naujas kintamasis (nesutinkamas niekur kitur).
\end{enumerate}

% Digression:
%   galima sugalvoti kažkokį teiginį F(n), kurį galima įrodyti kiekvienam
%   n, bet neįmanoma įrodyti bendrai, nėra vieningos schemos.

Pvz.:
\[
\F{\F{\F{\U{A(u)}, \forall x A(x) \vdash \U{A(u)}, \exists x A(x)}
        {A(u), \forall x A(x) \vdash \exists x A(x)}}
     {\forall x A(x) \vdash \exists x A(x)}}
  {\vdash \forall x A(x) \to \exists x A(x)}
\]
o
\[
\F{\F{\F{A(z_1) \vdash A(z_2)}
        {A(z_1) \vdash \forall x A(x)}}
     {\exists x A(x) \vdash \forall x A(x)}}
  {\vdash \exists x A(x) \to \forall x A(x)}
\quad\text{arba}\quad
\F{\F{\F{A(z_1) \vdash A(z_2)}
        {\exists x A(x) \vdash A(z_2)}}
     {\exists x A(x) \vdash \forall x A(x)}}
  {\vdash \exists x A(x) \to \forall x A(x)}
\]
neišvedama.

Pvz.:
\[
\F{\F{\F{\F{\F{\U{A(a, b)}, \forall y A(x, y) \vdash \U{A(a, b)}, \exists x A(x, b)}
              {A(a, b), \forall y A(x, y) \vdash \exists x A(x, b)}}
           {\forall y A(a, y) \vdash \exists x A(x, b)}}
        {\forall y A(a, y) \vdash \forall y \exists x A(x, y)}}
     {\exists x \forall y A(x, y) \vdash \forall y \exists x A(x, y)}}
  {\vdash \exists x \forall y A(x, y) \to \forall y \exists x A(x, y)}
\]

Pvz.:
\[
\F{\F{\F{\F{A(b, a), \forall y \exists x A(x, y)
            \vdash A(b, c), \exists x \forall y A(x, y)}
           {A(b, a), \forall y \exists x A(x, y)
            \vdash \forall y A(b, y), \exists x \forall y A(x, y)}}
        {A(b, a), \forall y \exists x A(x, y)
         \vdash \exists x \forall y A(x, y)}}
     {\exists x A(x, a), \forall y \exists x A(x, y)
      \vdash \exists x \forall y A(x, y)}}
  {\forall y \exists x A(x, y) \vdash \exists x \forall y A(x, y)}
\]
neišvedama.

% Įrodyti, kad neišvedama sunkiau, nei įrodyti, kad išvedama.  Skaičiavimu
% įrodyti neišvedamumo neįmanoma, reikia kažkaip pagrįsti žodžiais.
% Jei formulė tapačiai teisinga, išvedimą anksčiau ar vėliau surasim.
% Jei ne, neįmanoma sugalvoti jokio skaičiavimo, kuris tai parodytų.

Ar $\forall x \Box A(x) \equiv \Box \forall x A(x)$?
\[
\F{\F{\F{\F{\F{\text{neįrodoma}}{A(a), \Box A(a) \vdash A(b)}}
           {\Box A(a) \vdash A(b)}}
        {\Box A(a) \vdash \forall x A(x)}}
     {\Box A(a), \forall x \Box A(x) \vdash \Box \forall x A(x)}}
  {\forall x \Box A(x) \vdash \Box \forall x A(x)}
\quad
\F{\F{\F{\F{\U{A(a)}, \forall x A(x), \Box \forall x A(x) \vdash \U{A(a)}}
           {\forall x A(x), \Box \forall x A(x) \vdash A(a)}}
        {\Box \forall x A(x) \vdash A(a)}}
     {\Box \forall x A(x) \vdash \Box A(a)}}
  {\Box \forall x A(x) \vdash \forall x \Box A(x)}
\]

% 2003-03-19 (nebuvau, nusirašiau nuo Ramūno)

Ar $\Diamond \exists x P(x) \equiv \exists x \Diamond P(x)$?
\[
\F{\F{\F{\text{neįrodoma}}
        {\vdash \neg \exists x P(x)}}
     {\vdash \Box \neg \exists x P(x), \exists x \neg \Box \neg P(x)}}
  {\neg \Box \neg \exists x P(x) \vdash \exists x \neg \Box \neg P(x)}
\quad
\F{\F{\F{\F{\F{\F{\U{P(z)}, \Box \neg \exists x P(x) \vdash \U{P(z)}, \exists x P(x)}
                 {P(z), \Box \neg \exists x P(x) \vdash \exists x P(x)}}
              {P(z), \neg \exists x P(x), \Box \neg \exists x P(x) \vdash}}
           {\Box \neg \exists x P(x) \vdash \neg P(z)}}
        {\Box \neg \exists x P(x) \vdash \Box \neg P(z)}}
     {\neg \Box \neg P(z) \vdash \neg \Box \neg \exists x P(x)}}
  {\exists x \neg \Box \neg P(x) \vdash \neg \Box \neg \exists x P(x)}
\]

% $\forall x \Box A(x) \not\vdash \Box \forall x A(x)$ -- kad įrodytume reikia
% daugiau informacijos, tada galime įsivesti aksiomą $\forall x \Box A(x) \to
% \Box \forall x A(x)$, jei reikia.
% Sekvencinis skaičiavimas blogas tuo, kad taisyklių skaičius auga
% eksponentiškai.

\section{Reoliucijų tipo metodai}

% Tai „paneigimo metodas“?

Kaip patikrinti, ar iš formulių $F_1$, \dots, $F_n$ seka formulė $F$?
Užrašome reiškinio \[F_1 \land \dots \land F_n \land \neg F\] normalinę
konjunkcinę formą $S = \{D_1, \dots, D_k\}$, kur $D_i$ -- disjunktai (literų
disjunkcija; litera yra arba loginis kintamasis, arba jo neiginys).  Taisyklė
\[ \frac{p \lor D', \neg p \lor D''}{D' \lor D''} \]
Jei ją taikydami gauname apačioje tuščią reiškinį (žymima $\bot$), įrodyta.

% XXX kas nors paaiškinkit?

Pvz.: Įmonėje yra trys cechai: A, B ir C, susitarę dėl projektų tvirtinimo
tvarkos.  Jei cechas B nedalyvauja, tai nedalyvauja ir A tvirtinant projektą.
Jei B dalyvauja, tai kartu dalyvauja ir A, ir C.  Klausimas: ar privalo cechas
C dalyvauti tvirtinant projektą, kai tvirtina A?

Kitais žodžiais tariant, ar iš $\neg B \to \neg A$, $B \to (A \land C)$
išplaukia $A \to C$?
\begin{align*}
&(\neg B \to \neg A) \land (B \to (A \land C)) \land \neg (A \to C) \\
&S = \{ B \lor \neg A, \neg B \lor A, \neg B \lor C, A, \neg C \} \\
&\frac{B \lor \neg A, A}{B}
\quad \frac{\neg B \lor C, B}{C}
\quad \frac{C, \neg C}{\bot} \\
\end{align*}
% Įrodyta.

Kitas pvz.: jei Biblija yra teisinga ir ją reikia suprasti pažodžiui, tai
egzistuoja Dievas, be to Adomo ir Ievos išvarymo istorija yra teisinga.  Jei
tiesa, kad Dievas ištaip išvsrė iš rojaus Adomą ir Ievą, tai jis yra
kerštingas ir nemielaširdingas.  Tačiau, jei, kaip teigia Biblija, Dievas yra,
tai jis visagalis ir mielaširdingas.  Vadinasi Biblija yra tik graži pasaka
arba nereikia jos suprasti pažodžiui.

\begin{itemize}
% XXX reduce spacing
\item[b] -- Biblija yra teisinga
\item[p] -- Bibliją reikia suprasti pažodžiui
\item[d] -- egzistuoja Dievas
\item[a] -- Adomo ir Ievos išvarymo istorija yra teisinga
\item[e] -- Dievas yra kerštingas
\item[m] -- Dievas yra mielaširdingas
\item[v] -- Dievas yra visagalis
\end{itemize}

Duota: $(b \land p) \to (d \land a)$, $a \to (e \land \neg m)$, $d \to (v
\land m)$.  Įrodyti: $\neg b \lor \neg p$.
\begin{align*}
%& ((b \land p) \to (d \land a))                                 \land (a \to (e \land \neg m))                   \land (d \to (v \land m))                   \land \neg (\neg b \lor \neg p) \\
%& ((\neg b \lor \neg p) \lor (d \land a))                       \land (\neg a \lor (e \land \neg m))             \land (\neg d \lor (v \land m))             \land b \land p \\
%& (\neg b \lor \neg p \lor d) \land (\neg b \lor \neg p \lor a) \land (\neg a \lor e) \land (\neg a \lor \neg m) \land (\neg d \lor v) \land (\neg d \lor m) \land b \land p
&(b \land p) \to (d \land a)
 = (\neg b \lor \neg p) \lor (d \land a)
 = (\neg b \lor \neg p \lor d) \land (\neg b \lor \neg p \lor a) \\
&a \to (e \land \neg m)
 = \neg a \lor (e \land \neg m)
 = (\neg a \lor e) \land (\neg a \lor \neg m)\\
&d \to (v \land m)
 = \neg d \lor (v \land m)
 = (\neg d \lor v) \land (\neg d \lor m) \\
&\neg (\neg b \lor \neg p)
 = b \land p
\end{align*}
\[
S = \{ \neg b \lor \neg p \lor d, \neg b \lor \neg p \lor a,
       \neg a \lor e, \neg a \lor \neg m,
       \neg d \lor v, \neg d \lor m,
       b, p \}
\]
\begin{align*}
&\frac{\neg b \lor \neg p \lor a, b}{\neg p \lor a} \quad
\frac{\neg p \lor a, p}{a} \quad
\frac{a, \neg a \lor \neg m}{\neg m} \quad
\frac{\neg d \lor m, \neg m}{\neg d} \\&
\frac{\neg d, \neg b \lor \neg p \lor d}{\neg b \lor \neg p} \quad
\frac{\neg b \lor \neg p, p}{\neg b} \quad
\frac{\neg b, b}{\bot}
\end{align*}

\medskip

Kaip elgtis su modalumo logikos operatoriais?  Taisyklės tokios:
\[
\frac{\Box p \lor D', \neg p \lor D''}{D \lor D''} \quad
\frac{\Box p \lor D', \Diamond \neg p \lor D''}{D \lor D''}
\]

% Tai tinka tik atskirais atvejais, kai operatorius taikomas vienam loginiam
% kintamajam.  Bendrą atvejį išnagrinėsime vėliau.

Pvz.:  Jei šį pavasarį nusipirksiu mašiną arba susitaisysiu senąją, tai
važiuosiu į Latviją, o tada būtinai užsuksiu į Biržus.  Jei tikrai užsuksiu į
Biržus, tai aplankysiu tėvus.  Jei užsuksiu pas tėvus, jie galbūt įšnekins
mane kartu praleisti vasarą.  Tokiu atveju pasiliksiu ten iki rudens.  Bet jei
užsibūsiu ten iki rudens, tai Latvijos šią vasarą turbūt nepasieksiu.  Taigi,
galbūt neapsimoka taisyti senosios mašinos.

\begin{itemize}
% XXX reduce spacing
\item[n] -- nusipirksiu mašiną
\item[s] -- susitaisysiu senąją
\item[l] -- važiuosiu į Latviją
\item[b] -- užsuksiu į Biržus
\item[a] -- aplankysiu tėvus
\item[v] -- kartu praleisiu vasarą
\item[r] -- pasiliksiu pas tėvus iki rudens
\end{itemize}

Duota: $(n \lor s) \to (l \land \Box b)$, $\Box b \to a$, $a \to \Diamond v$,
$v \to r$, $r \to \neg l$. Patikrinti, ar $\Diamond \neg s$.

% a \to b === \neg a \lor b
\begin{align*}&
(n \lor s) \to (l \land \Box b)
 = (\neg n \land \neg s) \lor (l \land \Box b)
\\&\phantom{(n \lor s) \to (l \land \Box b)} = (\neg n \lor l) \land (\neg n \lor \Box b) \land (\neg s \lor l) \land (\neg s \lor \Box b) \\&
\Box b \to a = \neg \Box b \lor a = \Diamond \neg b \lor a\\&
a \to \Diamond v = \neg a \lor \Diamond v \\&
v \to r = \neg a \lor r \\&
r \to \neg l = \neg r \lor \neg l \\&
\neg \Diamond \neg s = \Box s
\end{align*}
\[
S = \{ \neg n \lor l, \neg n \lor \Box b, \neg s \lor l, \neg s \lor \Box b,
       \Diamond \neg b \lor a,
       \neg a \lor \Diamond v,
       \neg a \lor r,
       \neg r \lor \neg l,
       \Box s \}
\]
\begin{align*}&
\frac{\Box s, \neg s \lor \Box b}{\Box b} \quad
\frac{\Box s, \neg s \lor l}{l} \quad
\frac{l, \neg r \lor \neg l}{\neg r} \quad
\frac{\neg r, \neg a \lor r}{\neg a} \quad
\frac{\neg a, \Diamond \neg b \lor a}{\Diamond \neg b} \quad
\frac{\Box b, \Diamond \neg b}{\bot}
\end{align*}

% Teiginių logikoj rezoliucijų metodo nereikia -- galima susidaryti teisingumo
% lentelę.  Modalumo logikoj tai jau nebeišeina (jei imsim \Box x kaip atskirą
% kintamąjį, reikės atsižvelgti į aksiomas a la $\Box x \to x$, $(\Box (A \to
% B)) \to (\Box A \to B).

% Ką daryti, jei modalumo operatoriai taikomi poformulėms?  Nebeišeina
% transformuoti reiškinio į normaliąją konjunkcinę formą.  Bet gudrūs žmonės
% sugalvojo NKF atitikmenį.  Bėda, kad tai žymiai sudėtingiau.

Ar $a \equiv b \vdash \Box a \equiv \Box b$?
\[
\F{\F{\F{\text{neišeina}}
        {\Box a \vdash b}}
     {a \to b, b \to a, \Box a \vdash \Box b}}
   {a \to b, b \to a \vdash \Box a \to \Box b}
\]
% Bet kokiu atveju dešinėje valydami \Box nuo b kairėje nieko naudingo negausime
Ne.
% Moralas: modalumo logikos formulės į ekvivalenčią taip paprastai
% nepertvarkysim.  T.y. jei formulės F poformulis A \equiv B, bet jis yra
% kažkokio modalumo operatoriaus galiojimo srityje, tai mes negalime jo
% pakeisti...

% Apie 1990 m. Stenforde kažkoks gudruolis pastebėjo paprastą kelią:

Jei turime formulę F su kažkokiu poformuliu A ir turime $A \equiv B$, tai
nieko, bet jei turime $\Box (A \equiv B)$, tuomet formulėje F galime poformulį
A pakeisti į B.
% \Box (A \equiv B) \vdash F(A) \equiv F(B)

Pvz.: $\Box p \lor \Diamond (q \land r)$.  Pasižymėkime $a := (q \land r)$.
Keiskime $\Box (a \equiv (q \land r) \vdash \Box p \lor \Diamond a$ ir t.t.:
\begin{align*}&
\vdash \Box p \lor \Diamond \underbrace{q \land r}_{a} \\&
\Box (a \equiv (q \land r) \vdash \Box p \lor \underbrace{\Diamond a}_{b} \\&
\Box (a \equiv (q \land r), \Box (b \equiv \Diamond a) \vdash \underbrace{\Box p}_c \lor b \\&
\Box (a \equiv (q \land r), \Box (b \equiv \Diamond a), \Box (c \equiv \Box p)
\vdash \underbrace{c \lor b}_l \\&
\Box (a \equiv (q \land r), \Box (b \equiv \Diamond a), \Box (c \equiv \Box
p), \Box (l \equiv c \lor b) \vdash
\end{align*}

Taisyklės yra šios
\begin{align*}&
 \Box (a \equiv (b \lor c))
   : \Box (a \to (b \lor c)), \Box ((b \lor c) \to a)
   : \Box (\neg a \lor b \lor c), \U{\Box (a \lor \neg c)}, \U{\Box (a \lor \neg b)} \\&
 \Box (a \equiv (b \land c))
   : \Box (a \to (b \land c)), \Box ((b \land c) \to a)
   : \Box (\neg a \lor b), \Box (a \lor c), \U{\Box (\neg b \lor \neg c \lor a)} \\&
 \Box (a \equiv \neg b)
   : \Box (a \to \neg b), \Box (\neg b \to a)
   : \Box (\neg a \lor \neg b), \U{\Box (b \lor a)} \\&
 \Box (a \equiv \Box b)
   : \Box (a \to \Box b), \Box (\Box b \to a)
   : \Box (\neg a \lor \Box b), \U{\Box (\Diamond \neg b \lor a)} \\&
 \Box (a \equiv \Diamond b)
   : \Box (a \to \Diamond b), \Box (\Diamond b \to a)
   : \Box (\neg a \lor \Diamond b), \U{\Box (\Box \neg b \lor a)} \\&
\end{align*}
% XXX: gerai būtų pasitikrinti!!!
Išrašę tai gauname disjunktų aibės atitikmenį modalumo logikai.

Jei formulėje neigimas yra tik prieš loginius kintamuosius, pakanka tik
pabrauktų disjunktų.
% Pvz \neg (\Box p \land \Diamond (q \lor \Box \neg r)) \equiv
%      \Diamond \neg p \lor \Box (\neg q \land \Diamond r)
% tad čia galima.

% Gauname daaaug mažyčių formulų -- rankom nepatogu, kompams paprasta

% 2003-04-02 (nebuvau, nusirašiau nuo Ramūno)

\section{Rezoliucijų metodas modalumo teiginių logikoje}

Formulė $F$ yra išvedama ($\vdash F$), jei atsiras formulių seka $\Box D_1,
\dots, \Box D_s, l \vdash$, kur $D_i$ -- modalumo logikos disjunktai (modalumo
logikos literų konjunkcijos, kur modalumo logikos litera yra $\Box l$,
$\Diamond l$ arba $l$, o $l$ yra įprastinė teiginių logikos litera).

Rezoliucijų metodo taisyklės:
\[ \frac{F, G}{res(F, G)} % -- \text{priklauso nuo $F$ ir $G$ pavidalo.}
\]
\begin{multicols}{2}\noindent
\[ \frac{res(\Box F, \Box G)}{\Box res(F, G)}
\]
\[ \frac{res(\Box F, G)}{res(F, G)}
\]
\[ \frac{res(\Box F, \Diamond G)}{\Diamond res(F, G)}
\]
\[ \frac{res(F \lor G, H)}{F \lor res(G, H)}
\]
\[ \frac{res(l, \neg l)}{\bot}
\]
\end{multicols}
Prastinimas:
\begin{multicols}{3}\noindent
\[ \frac{F \lor \bot}{\bot}
\]
\[ \frac{\Box \bot}{\bot}
\]
\[ \frac{\Diamond \bot}{\bot}
\]
\end{multicols}
% $res$ yra tam tikras operatorius, kuris vėliau dingsta.
% XXX WTH?

% Grr

% BTW \Box \Box F === \Box F
%     \Diamond \Diamond F === \Diamond F
%     \neg \neg F === F

% Toliau eina tik pvz.  XXX: todo

% 2003-04-09

\paragraph{Išvedimo paieška.}  Turime disjunktų aibę $S = \{D_1, \dots D_s\}$.
Galime imti bet kuriuos du disjunktus ir iš jų išvesti naują:
\[ \frac{D_i, D_j}{D'} \]

\paragraph{Tiesinė taktika.}

% Truputį nesupratau.  Perbėgam iš kairės į dešinę.
%   turime {D_1, ..., D_s}
%   D_i, D_j
%   --------
%      D'      D_{f_1}
%      ---------------
%             D''        D_{l}
%             ----------------
%                  D'''
%
% Teiginių logikai to pakanka, visada rasime išvedimą.  Modalumo logikoje
% išeina ne visada.
%

Perbėgame disjunktus iš kairės į dešinę.  Naujai gautus dedame į eilės galą.
Išvedimo medis atrodo labai tiesiškai (kiekviename mazge dešinioji šaka yra
lapas).

\paragraph{Absorbcijos taktika.}  Turime disjunktų aibę
\[ S = \{ D_1, D_2, \dots, D_s \}
\]
Paimame gautus disjunktus $C_1, C_2$  Taktika: susiaurinti išvedamų disjunktų
aibę.  Galime taikyti $\frac{C_1, C_2}{C}$ tik jei
\begin{enumerate}
\item arba vienas iš $C_1, C_2$ priklauso pradinei aibei $S$
\item nei vienas iš $C_1, C_2$ nepriklauso $S$, tada galime taikyti tik jei
      $C_1 = p \lor D'$, $C_2 = \neg p \lor D''$ ir $D' \subset D''$ arba
      $D'' \subset D'$ (čia $A \subset B$ reiškia, kad $A$ yra $B$ dalis, pvz,
      $q \lor \neg r \subset q \lor s \lor \neg r$)
\end{enumerate}

Pvz.:
\[ \F{\F{p \lor \Box q \quad \F{D_1}{\neg q \lor r}}    % XXX align bottoms
        {p \lor r}          \quad              \F{D_2}{\Box \neg r \lor s}}
     {p \lor s} \quad \text{-- šis taikymas netaisyklingas pagal absorbcijos
                               taktiką}
\]
galime perkelti tą netaisyklingą taikymą aukščiau:
\[ \F{\F{\F{D_1}{\neg q \lor r} \quad \F{D_2}{\Box \neg r \lor s}}
        {\neg q \lor s} \text{-- pažeidimas dabar čia}
        \quad p \lor \Box q}
     {p \lor s} 
\]

Kitas pvz:
\[ (*)
   \F{\F{\Box(p \lor q) \quad \F{D_1}{\Diamond \neg q \lor r}}
        {\Box p \lor \Box r}                    \quad \F{D_2}{\Box(\neg r \lor s)}}
     {\Diamond p \lor \Diamond s}
\]
perkeliam aukščiau
\[ 
   \F{\F{\F{D_1}{\Box \neg q \lor r} \quad \F{D_2}{\Box(\neg r \lor s)}}
        {\Diamond \neg q \lor \Diamond s} \quad \Box(p \lor q)}
     {\Diamond p \lor \Diamond s}
\]

\paragraph{Rezoliucijų metodas klasikinėje predikatų logikoje}

Bendra schema: turime $F_1, \dots, F_n$, norime įrodyti $F$. $(F_1 \land \dots
\land F_n) \to F$ yra tapačiai teisinga tada ir tik tada, kai $F_1 \land \dots
\land \neg F$ yra tapačiai klaidinga.
\begin{enumerate}
\item suvedame į normalinę priešdėlinę formą
\item skulemizacija (egzistavimo kvantoriaus eliminavimas),
      bendrumo kvantorius $\forall$ praleidžiame
\item suvedame į normalinę konjunkcinę formą.
\end{enumerate}
Rezultatas -- turime disjunktų aibę $D = \{ D_1 \dots D_s\}$ ir ieškome
išvedimo.

Normalinė priešdėlinė forma yra $Q_1 x_1 Q_2 x_2 \dots Q_n x_n G$, kur $Q_i
\in \{ \forall, \exists \}$, o formulėje $G$ kvantorių nėra.

Leidžiamos transformacijos:
\begin{multicols}{2}\noindent
\[ \forall x A(x) \equiv \forall y A(y) \]
\[ \exists x A(x) \equiv \exists y A(y) \]
\[ \neg \forall x A(x) \equiv \exists x \neg A(x) \]
\[ \neg \exists x A(x) \equiv \forall x \neg A(x) \]
\[ \forall x A(x) \land B \equiv \forall x (A(x) \land B) \]
\[ \exists x A(x) \land B \equiv \exists x (A(x) \land B) \]
\[ \forall x A(x) \lor B \equiv \forall x (A(x) \lor B) \]
\[ \exists x A(x) \lor B \equiv \exists x (A(x) \lor B) \]
\end{multicols}
\nobreak
jei formulėje $B$ nėra kintamojo $x$ (jei jis yra, galima pervadinti).
% \begin{multicols}{2}\noindent
\[ \forall x A(x) \land \forall x B(x) \equiv \forall x (A(x) \land B(x)) \]
\[ \forall x A(x) \lor \forall x B(x) \equiv \forall x \forall y (A(x) \land B(y)) \]
\[ \exists x A(x) \land \exists x B(x) \equiv \exists x \exists y (A(x) \land B(y)) \]
\[ \exists x A(x) \lor \exists x B(x) \equiv \exists x (A(x) \lor B(x)) \]
% \end{multicols}

Pvz.: % rasti norm. pr. form
\begin{align*} &
\exists x \forall y A(x, y) \to \forall y \exists x B(x, y) \\&
\neg \exists x \forall y A(x, y) \lor \forall y \exists x B(x, y) \\&
\forall x \neg \forall y A(x, y) \lor \forall y \exists x B(x, y) \\&
\forall x \exists y \neg A(x, y) \lor \forall y \exists x B(x, y) \\&
\forall x(\exists y \neg A(x, y) \lor \forall y \exists x B(x, y))\\&
\forall x(\exists y \neg A(x, y) \lor \forall y \exists u B(u, y))\\&
\forall x \exists y(\neg A(x, y) \lor \forall v \exists u B(u, v))\\&
\forall x \exists y \forall v(\neg A(x, y) \lor \exists u B(u, v))\\&
\forall x \exists y \forall v \exists u(\neg A(x, y) \lor B(u, v))
% FIXME: ant lentos išėjo \forall x \forall z \exists y (\neg A(x,y) \lor B(y,z))
% Turėtų būti \equiv...
\end{align*}

Skulemizacija -- egzistavimo kvantorių eliminavimas.  Kiekvieną kintamąjį
$\exists x$ keičiame naujai įvestu funkciniu simboliu, kuris priklauso nuo
visų kairiau esančių bendrumo kvantorių.

O bendrumo kvantorius tiesiog praleidžiame.  Pvz.:
\[ \exists x \forall y \exists z \forall u \forall v \exists s F(x, y, z, u,
v, s)
\to
   F(a, y, f(y), u, v, g(y, u, v))
\]

Dabar tereikia suvesti $F$ į normalinę konjunkcinę formą ir gausime disjunktų
aibę.

% XXX imho vis dėlto disjungtas...

\medskip
% Nauja sąvoka

\Def{Keitinys} $\sigma = (t_1/x_1, \dots, t_n/x_n)$ kur $x_i$ -- kintamieji, o
$t_i$ -- termai.

Jei $F(x_1, \dots x_n)$ -- formulė, tai $F\sigma = F(t_1, \dots t_n)$ yra ta
pati formulė, kurioje kintamieji $x_1 \dots x_n$ pakeisti termais $t_1 \dots
t_n$.

Keitinys vadinamas \Def{unifikatoriumi} formulėms $F$ ir $G$, jei $F\sigma =
G\sigma$.

Keitinys $\sigma$ yra bendriausias unifikatorius jei bet koks kitas
unifikatorius $\beta$ yra kompozicija $F\sigma \phi = F\beta$.
% XXX čia sumalta kažkas ne į temą.  Kas yra bendriausias unif?

Pvz. formulių $P(x, f(a), g(z))$ ir $P(f(y), z, g(f(a))$ unifikatorius yra
$\sigma = (f(a)/x, a/y, f(a)/z)$, o bendriausias unifikatorius yra $(f(y)/x,
f(a)/z)$ (į ką keičiamas $y$ nefiksuojama, nes tai nesvarbu).

Ne visas formules galima unifikuoti.

Galima taikyti taisyklę
\[\frac{C_1 \quad C_2}{C}, \quad\text{kur $P(t_1, \dots, t_n) \in C_1$, o
                                          $\neg P(g_1, \dots g_n) \in C_2$,}\]
jei egzistoja unifikatorius $\sigma$, kad $P(t_1, \dots, t_n) \sigma = P(g_1,
\dots g_n) \sigma$.  Tik tuomet keisime visur:
\[\frac{C_1\sigma \quad C_2\sigma}{C\sigma}
\]

% grr

% Gegužės 21 d. kontrolinis, gegužės 28 d. pasirašinėjimai

\end{document}