\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}
