\input stf \def\NieparzystyHead{\line{\hfill\HeaderFont On a Certain Deduction System with Metainduction}} \def\ParzystyHead{\line{\HeaderFont Anna Zalewska\hfill}} \startpageno=85 \pageno=\startpageno \lineskiplimit0pt \pu\pu\pu \lasta Anna Zalewska\\ %%\lasta University in Bialystok\\ \t A CRITERION OF DECIDABILITY \\ \smallskip \lastt OF SOME ALGORITHMIC FORMULAS\\ \def\rrr #1\\{\pu\pu\centerline{\bf #1}\pu} \def\rrrr #1\\{\pu\centerline{\bf #1}} \def\rrrrbezpu #1\\{\centerline{\bf #1}} \def\<{\langle} \def\>{\rangle} \def\name#1{\bigskip\line{#1\hfill}} \def\zero{\hbox{\bf 0}} \def\one{\hbox{\bf 1}} \font\gothic=eufm10 \font\mgothic=eufm7 \font\mmgothic=eufm5 \font\pisane=eusm10 \font\mpisane=eusm7 \font\msam=msam10 \font\eurb=eurb10 \def\true{\hbox{\bf true}} \def\false{\hbox{\bf false}} \def\IF{\hbox{\rm IF}} \def\Begin{\hbox{\bf begin~}} \def\End{\hbox{\bf ~end}} \def\If{\hbox{\bf if~}} \def\Then{\hbox{\bf ~then~}} \def\Else{\hbox{\bf ~else~}} \def\Fi{\hbox{\bf ~f{}i}} \def\While{\hbox{\bf while~}} \def\Do{\hbox{\bf ~do~}} \def\Od{\hbox{\bf ~od}} \def\gotM{\hbox{\gothic M}} \def\gotB{\hbox{\gothic B}} \def\mgotM{\hbox{\mgothic M}} \def\mmgotM{\hbox{\mmgothic M}} \def\pisA{\hbox{\pisane A}} \def\pisC{\hbox{\pisane C}} \def\pisE{\hbox{\pisane E}} \def\pisI{\hbox{\pisane I}} \def\pisP{\hbox{\pisane P}} \def\mpisP{\hbox{\mpisane P}} \let\Stopien=\circ \def\stopien{^\Stopien} \let\limp=\Rightarrow \let\bigpi=\prod \let\Over=\slash \def\kwadrat{\hbox{\msam\char3}} \def\Q{\hbox{\eurb Q}} \def\Lemma #1 {\noindent {\bf Lemma #1~~}} \def\Proof.{\noindent {\bf Proof.}~~} \def\Definition #1 {\noindent {\bf Definition #1}~~} \def\Theorem #1 #2\\ #3\par{\noindent {\bf Theorem #1}~~#2\hfill\break #3\par} \def\Corollary #1\\ #2\par{\noindent {\bf Corollary #1}\hfill\break #2\par} \def\CBDO{\par\line{\hfill\msam\char3}} \def\CBDOg{\par\vskip-\baselineskip\line{\hfill\msam\char3}} \def\cbdo{\hbox{\msam\char3}} \font\Large=cmr12 \def\prefcirc{{\it pref}\kern2pt$^\circ$} \def\prefpcirc{{\it pref'}\kern2pt$^\circ$} \def\LargeQ{\hbox{\Large Q}} \def\jedna #1.#2||#3*{ \line{% \hbox to .2\hsize{#1\hfill}\hbox to.8\hsize{$\displaystyle{#2\over#3}$\hfill}\hss}% \medskip } \def\jednadol #1.#2||#3*#4*#5*{ \line{% \hbox to .2\hsize{#1\hfill}\hskip#5\hbox to.8\hsize{$\displaystyle{#2\over\vbox{\hbox{$#3$}\hbox{$#4$}}}$\hss}\hss}% \medskip } \def\jednaprzesunieta #1.#2||#3*#4*{ \line{% \hbox to .2\hsize{#1\hfill}\hskip#4\hbox to.8\hsize{$\displaystyle{#2\over#3}$\hss}\hss}% \medskip } \def\dwie #1.#2||#3* #4* #5.#6||#7*{ \medskip \line{% \hbox to .1\hsize{#1\hfill}\hbox to.35\hsize{$\displaystyle{#2\over#3}$\hfill}% \hfill #4\hfill \hbox to .1\hsize{#5\hfill}\hbox to.35\hsize{$\displaystyle{#6\over#7}$\hfill}}% \medskip } \vskip-\baselineskip \Abstract. In the paper a certain criterion of decidability for proof system of propositional algorithmic logic is presented. The criterion allows to prove validity of the algorithmic formulas in automatic way suitable for computer realization. Two examples of computer experiments are included. \\ \rbezpu 1. Introduction\\ It was Leibniz [3] who first claimed {\it It is unworthy of excellent [persons] to lose hours like slaves in the labor of calculation which could be safely relegated to anyone else if machines were used}. Now modern computer techniques give us possibility for realization of automated reasoning. In order to prove validity of formulas (in a given logic) in automatic way we should have at our disposal a proof system which is sound, complete and decidable. The property of decidability of the proof system is very important from automated proving point of view. It is necessery to have a procedure that in finite number of steps gives us the answer to the question about validity of a given formula. But it is not enough: the procedure should be suitable for computer realization. In [4] the proof system for propositional algorithmic logic was described. Soundness and completness of the system were described there, too. The propositional algorithmic logic is decidable (see [1]) but the procedure proposed by Chlebus is not appropriate from computer realization point of view. In the paper a certain criterion of decidability for the proof system is presented. The criterion gives us a procedure that checks validity of the algorithmic formulas in automatic way suitable for implementation. \looseness=1 In Chapter~2 the basic notions connected with the proof system are reminded. In Chapter~3 we present the basic rules of our proof system. In Chapter~4 a criterion of decidability of some algorithmic formulas is described. In appendix two examples of computer experiments are included. \pu \rbezpu 2. Basic notions\\ Let us remind that the alphabet of the language of propositional algorithmic logic \pu \centerline{$A_{PAL} = V_0 \cup V_p \cup L_c \cup L_{con} \cup I_q \cup P_c \cup A_s$} \pu \noindent where $V_0$ and $V_p$ are respectively an enumerable set of propositional variables, and an enumerable set of program variables, $L_c$ is the set of {\it logical constants} $(\{\true,\false\})$, $L_{con}$ denotes the set of {\it logical connectives} $(\{\lnot,\lor,\land,\limp\})$ and $I_q$ denotes the set of {\it iteration quantifiers} $(\{\bigcup,\bigcap\})$, $P_c$ is the set of {\it program connectives} $(\{\Begin - ; - \End, \If - \Then - \Else - \Fi, \While - \Do - \Od\})$ and $A_s$ is the set of {\it auxiliary signs} $(\{(,)\})$. The set of all {\it programs} is the least extension of the set~$V_p$ and program constant~$Id$ such that if $\gamma$ is a classical propositional formula and $M,M'$ are programs then the expressions $\Begin M; M' \End$, $\If \gamma \Then M \Else M' \Fi$, $\While \gamma \Do M \Od$ are programs. The set of all {\it formulas} is the least extension of the set of classical propositional formulas such that if $M$ is a~program and $\alpha$ and $\beta$ are formulas then $(\alpha \lor \beta)$, $(\alpha \land \beta)$, $(\alpha \limp \beta)$, $\lnot\alpha$ $M\alpha$, $\bigcup M\alpha$, $\bigcap M\alpha$ are formulas too. Let $pref\stopien$ stand for {\it prefix} i.e. finite sequence, perhaps empty, of the form $\mp K_1\mp K_2\dots\mp K_l$ \noindent where $K_i\in V_p$ and $\mp K_i$ is $\lnot K_i$ when ``$\mp$"=``$\lnot$" or $K_i$ when ``$\mp$"=``$\varepsilon$", and ``$\Stopien$"=``$+$" if the number of programs with negation occurring in prefix is even, otherwise ``$\Stopien$"=``$+$". {\it An~absolute value} of~$\mp K_i$ is defined in the following way \medskip $\vert\mp K_i\vert=\cases{ \lnot(\mp K_i)&if ``$\mp$"=``$\lnot$"\cr (\mp K_i)&if ``$\mp$"=``$\varepsilon$"\cr }$ \medskip Let $pref\stopien$ (${pref'}\stopien$) will be of the form $\mp K_1\mp K_2\dots\mp K_l$ ($\mp L_1\mp L_2\dots\mp L_l$). The absolute value of the prefix $pref\stopien$ is {\it equal} to the absolute value of the prefix~${pref'}\stopien$ if for all indexes $i=1,\dots,n$ $\vert\mp K_i\vert=\vert\mp L_i\vert$ (we will denote the equality writing $\vert pref\vert=\vert pref'\vert$). We~will write $pref_k^-$ ($pref_k^+$) in order to mark the fact that the first $k$ elements of the prefix~$pref\stopien$ set up the subprefix in which the number of programs with negation occurring in it is even (uneven). Let $\Pi$ be a finite sequence of formulas. A prefix $pref$ is said to be {\it removable in the sequence}~$\Pi$ if the following conditions hold \pu \itemitem{(*)}$\exists_{\beta \in \Pi} (\beta=pref\stopien \beta')$ and \pu \itemitem{(**)}$\forall_{k \in \{1,\dots, l\}} \exists_{\beta\in\Pi}(\beta={pref'}^-\beta' \land \vert pref' \vert = \vert pref_k\vert)$ \pu \noindent where $l$ denotes the length of the prefix~$pref$ and $\beta'$~is an~arbitrary formula. \r 3. Basic rules\\ Here we remind only basic rules (and the others notions) of the proof system (it is called PS) that are needed in order to understand the next chapter (for better understanding see [4,5]). %%\medskip According to notational conventions, used in the literature, by $\Delta$, $\Delta'$, $\Gamma$, $\Gamma'$, $\Pi$, $\Pi'$, $\Sigma$ and $\Sigma'$ (possible with indices) we denote sequents, i.e. finite sequence (maybe empty) of formulas. By $\{\Gamma,\alpha,\Delta\}$ we shall mean a~sequence in which we have first~$\Gamma$, next~$\alpha$ and lastly~$\Delta$. %% \medskip In the PS system conclusion and premises of the rules will be presented as ordered pair of the form \pu \itemitem{(*)}$~~~~~~~~~~~~~~~~~~~~~~~~~~\langle\Pi,\pisA\rangle$ \pu \noindent where $\Pi$ denotes main sequent, \noindent \hphantom{where }$\pisA$ stands for set (maybe empty) of sequents. \pu \noindent Each of the rules of the PS system describes relation between its conclusion (written over a~line) and its premise or premises (written under the line). Then schemes of the decomposition rules are in the following form \pu \dwie ~.\langle \Pi,\pisA\rangle ||\langle \Pi',\pisA'\rangle * or* ~.\langle \Pi,\pisA\rangle ||\langle \Pi',\pisA'\rangle ~;~\langle \Pi'',\pisA''\rangle * \pu \noindent In all the below schemes $\Gamma$~denotes a~set of indecomposable formulas and $\Delta$~is an~arbitrary set of formulas; $\alpha$,~$\beta$~are arbitrary formulas; $\gamma$~denotes an~open formula; $M$,~$M'$, $M''$~denote arbitrary programs; $p\in V_0$; $\Stopien\in \{-,+\}$; $\mp \in \{\lnot,\varepsilon\}$; $\kwadrat\in \{\land,\lor\}$; $\Q\in \{\bigcup,\bigcap\}$. \medskip \medskip \medskip The basic decomposition rules of PS system are presented below. \medskip \medskip (1) \jedna ~.\<\{\Gamma,pref \stopien\true,\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\lnot \false,\Delta\},\pisA\>* (2) \jedna ~.\<\{\Gamma,pref \stopien\lnot\true,\Delta\},\pisA\>||\<\{\Gamma,pref \stopien \false,\Delta\},\pisA\>* (3) \jedna ~.\<\{\Gamma,pref \stopien\lnot\lnot\alpha,\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\alpha,\Delta\},\pisA\>* \medskip (4) \jedna~.\<\{\Gamma,pref \stopien\mp (\alpha\limp\beta),\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\mp (\lnot\alpha\lor\beta),\Delta\},\pisA\>* (5) \jedna ~.\<\{\Gamma,pref \stopien\mp (\alpha \cbdo \beta),\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\mp \alpha,\Delta\},\pisA\>; \<\{\Gamma,pref \stopien\mp \beta,\Delta\},\pisA\>* \noindent where $(\Stopien,\mp,\kwadrat) \in \{(-,\varepsilon,\lor),(+,\varepsilon,\land),(+,\lnot,\lor),(-,\lnot,\land)\}$ \medskip (6) \jedna ~.\<\{\Gamma,pref \stopien\mp (\alpha \cbdo \beta),\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\mp \alpha,pref \stopien\mp \beta,\Delta\},\pisA\>* \noindent where $(\Stopien,\mp,\kwadrat) \in \{(+,\varepsilon,\lor),(-,\varepsilon,\land),(-,\lnot,\lor),(+,\lnot,\land)\}$ \medskip (7) \jedna ~.\<\{\Gamma,pref \stopien\mp Id\alpha,\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\mp \alpha,\Delta\},\pisA\>* \noindent where $\alpha\notin \{\false,p\}$ \medskip (8) \jedna ~.\<\{\Gamma,pref \stopien\mp \alpha,\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\mp Id\alpha,\Delta\},\pisA\>* \noindent where $\alpha\in \{\false,p\}$ and $Id$ is not an element of the prefix~$pref\stopien$ \medskip (9) \jedna ~.\<\{\Gamma,pref\stopien\mp \Begin M';M'' \End\alpha,\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\mp M'(M''\alpha),\Delta\},\pisA\>* (10) \jedna ~.\<\{\Gamma,pref\stopien\mp \If \gamma \Then M' \Else M''\Fi\alpha,\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\mp ((\gamma\land M'\alpha)\lor(\lnot\gamma\land M''\alpha)),\Delta\},\pisA\>* (11) \jedna ~.\<\{\Gamma,pref\stopien\mp \While \gamma \Do M \Od\alpha,\Delta\},\pisA\>||\<\{\Gamma,pref \stopien\mp \bigcup\If \gamma \Then M \Fi(\lnot\gamma\land\alpha),\Delta\},\pisA\>* (12) \jedna ~.\<\{\Gamma,pref \stopien\mp QM\alpha,\Delta),\pisA\> || \<\{\Gamma,pref \stopien\mp \alpha,\Delta,pref \stopien\mp MQM\alpha\},\pisA\>* % \medskip % \pu \noindent The main sequent~$\Pi$ of the ordered pair $\langle\Pi,\pisA\rangle$ is said to be \item{$\bullet$}{\it indecomposable} iff no $PS$ rule can be applied to it, \item{$\bullet$}{\it fundamental} iff the formulas $pref^-\alpha$ and $pref'^+\alpha$ satisfying the conditions (I-II) belong to the sequent~$\Pi$ or the formula $pref^-\false$ satisfying the conditions (II) belongs to the sequent~$\Pi$ where \itemitem{(I)}$\vert pref\vert=\vert pref'\vert$, \itemitem{(II)}$pref$ is not empty and removable in the sequent~$\Pi$, \item{$\bullet$}$\pisA$-{\it provable} iff there exists a~sequent $\Sigma\in\pisA$ such that \smallskip \centerline{$\forall_{\alpha\in\Sigma}\exists_{\beta\in\Pi} (\beta$ is equal to $\alpha)$} \smallskip \item{}(we will say sometimes that $\Pi$ is $\pisA$\--{\it provable with respect to the sequent~$\Sigma$}), \item{$\bullet$}$\pisA^*$-{\it provable} iff there exists a~sequent $\Sigma\in\pisA$ for which $\Sigma^-\ne\emptyset$ (where $\Sigma^-=\{\beta\in\Sigma\vert\beta=\lnot\beta'\}$) and there exists a~sequence~$L$ of program variables $L_1\dots L_m$ such that \smallskip \centerline{$\forall_{\alpha\in\Sigma}\exists_{\beta\in\Pi}(\beta$ is equal to $\alpha_L)$} \smallskip \item{}where $\alpha_L=\pm L_1\dots L_m\alpha'$ if $\alpha=\pm\alpha'$ and ``$\pm$"$\in \{\lnot,\varepsilon\}$ \item{$\bullet$}{\it terminal} iff $\Pi$ is indecomposable but $\Pi$ is neither fundamental nor $\pisA$\--provable nor $\pisA^*$\--provable. \medskip \medskip \noindent A {\it proof} of the sequent~$\Pi$ is a~diagram (diagram is a decomposition tree obtaining by application of decomosition rules to input formula; precise definition of diagram can be found in [5]) of the sequent such that all paths of the diagram are finite and each its leaf is labelled by the ordered pair $\langle\Pi,\pisA\rangle$ where $\Pi$~is fundamental or $\pisA$\--provable or $\pisA^*$\--provable. \medskip \r 4. A criterion of decidability \\ In PS system its decidability is reduced to solution the problem \medskip {\it does exist a procedure that allows to check how many times the scheme (12) should be applied to a given formula of the main sequent of the ordered pair (during building the decomposition tree) in order to state that another application of the scheme is useless because it does not lead us to a leaf of the tree}. \medskip The solution above problem is especially useful during the building a counterexample of a given sequent i.e. during checking for a given ordered pair $<\Pi, {\cal A}>$ whether another application of the scheme (12) to a given formula $\Pi$ of the main sequent do not lead us to state that the sequent is fundamental or ${\cal A}^{*}$-provable. %%\medskip The second case of described above problem is enough simple. In order to check whether the sequent $\{\Gamma, ${\prefcirc }$\mp \LargeQ M\alpha, \Delta {\bf \}}$, where $(\circ ,\mp ,{\LargeQ} ) \in \{(+,\epsilon ,\bigcup),(-,\epsilon ,\bigcap), (-,\neg ,\bigcup),(+,\neg ,\bigcap )\}$ is ${\cal A}^{*}$-provable with respect to the sequent $\{\Gamma',${\prefpcirc }$\mp \LargeQ M\alpha ,\Delta' {\bf \}} \in {\cal A}$ and the sequence of programs $L_{1}, \ldots, L_{n}$ it is enough to check whether the length of the prefix {\prefcirc} is greater then sum of the number $n$ and the length of the prefix {\prefpcirc}. If it is true then next application of the scheme (12) is needless. %%% \medskip %In order to state from which moment next application of the scheme (12) %to a given formula will be useless. The first case of described above problem is more difficult task. However there exists a procedure given by Chlebus ([1]) that allows us to decide the problem. The weak point, from practical point of view, Chlebus's method is it that it requires remembering in computer memory the whole of the decomposition tree %(zwi/azane jest to z potrzeb/a sprawdzania %na danym poziomie diagramu formu/ly %czy nie wyst/api/l wierzcho/lek %tak samo ju/z etykietowany wcze/sniej, tzn. na /scie/zce prowadz/acej %z wierzcho/lka drzewa do wierzcho/lka na tym danym poziomie) what is not convenient during implementation. %% \medskip Presented below strategy allows us in many cases to eliminate symbols $\bigcup, \bigcap$ from formulas to which the scheme (12) can be applied. \smallskip \vfill {\bf STRATEGY:} %%\smallskip Let $\Pi$ be a sequent containing the set of formulas $S=\{\delta_{1}, \ldots, \delta_{n}\}$ such that their prefixes are not empty and the scheme (12) can be applied to the formulas. The formulas are in the form \vfill %%\smallskip \centerline {{\prefcirc }$\mp \LargeQ M\delta$} \vfill %\smallskip \noindent where $(\circ , \mp , {\LargeQ}) \in$ $\{(+, \epsilon , \bigcup),$ $(-, \epsilon , \bigcap),$ $(-, \neg , \bigcup),$ $(+, \neg , \bigcap )\}$. \smallskip \item{1.~}Separate from $\Pi$ the set ${\cal P}$ such that its elements are classes of formulas from the sequent ${\Pi}$ and for each class ${K_{i}}\in {\cal P}$ two following conditions are satisfied: %% \pu \leftskip10mm \item{--~}at least one formula from the set S belongs to ${K_{i}}$ \leftskip5mm \item{--~}prefixes of formulas belonging to ${K_{i}}$ (from which program constants ${\it Id}$ are removed) can be presented as the following sequence \leftskip3mm %\smallskip \vfill ~~~~~~~~~~$\mid{\it pref1}\mid~\subseteq~\mid{\it pref2}\mid~ \subseteq~\ldots~\subseteq~\mid{\it prefm}\mid$, %\smallskip \vfill \leftskip3mm \noindent ~~~~~~~~where m is the number of formulas in the class ${K_{i}}$ \leftskip5mm \item{--~}for each two classes ${K_{i}},{K_{j}}\in {\cal P}$ neither ${K_{i}}~\subseteq~{K_{j}}$ nor ${K_{j}}~\subseteq~{K_{i}}$. %%%\pu \leftskip0mm \item{2.~}Remove from the set ${\cal P}$ these classes that satisfy the condition: there exists the formula with the shortest prefix to which the scheme (12) can be applied such that the prefix is not removable in the class. %%% \medskip \item{3.~}For each class $K_{i}$ such that \leftskip5mm %\smallskip \item{--~}exactly one formula from the set $S$ belongs to $K_i$ %\smallskip \leftskip0pt \item{}check (by after-mentioned procedure PROC1($K_{i}$)) whether application of the scheme (12) to $K_i$ does not lead us to leaves of the decomposition tree. \eject %%%\medskip \item{4.~}For each class $K_{i}$ such that \leftskip5mm %\smallskip \item{--~}at least two formulas from the set $S$ belong to $K_i$ and \item{--~}each application of the scheme (12) to $K_i$ leads to fixed increment of prefix elements of a~given formula %\smallskip \leftskip0pt \item{}check (by after-mentioned procedure PROC2($K_{i}$)) whether application of the scheme (12) to $K_i$ does not lead us to leaves of the decomposition tree. %%%\medskip \item{5.~}For each class $K_{i}$ such that \leftskip5mm %\smallskip \item{--~}$K_i$ does not satisfy conditions of the point 3 or 4 %\smallskip \leftskip0mm \item{}use Chlebus's method. \medskip \medskip Below we give two mentioned before procedures. \medskip {\bf PROC1($K_{i}$)} \par {\bf begin} \par ~let~$\alpha$={\prefcirc }$\mp \LargeQ M\delta \in K_{i} \cap S$, \par ~~~~~$\beta$ -- formula with the greatest length of prefix in $K_{i}$ \par ~~~~~~~~~~~such that $\beta \neq \alpha$, \par ~~~~~$d_{1}$ -- length of the prefix of the formula $\alpha$, \par ~~~~~$d_{2}$ -- length of the prefix of the formula $\beta~$ decreased \par ~~~~~~~~~~~~by 1, \par ~if $d_{2} \geq d_{1}$ then \par ~$\alpha:=${\prefcirc }$\mp \delta ~\cup~${\prefcirc }$\mp M\delta ~\cup~ \ldots ~\cup~ ${\prefcirc }$\mp M^{(d_{2}-d_{1})+1}\delta ~\cup~\delta'$ \par \smallskip ~~~~~~~~~where $\delta'$ = {\prefcirc }$\mp M^{(d_{2}-d_{1})+2}\LargeQ M\delta$; \par \smallskip ~build the decomposition tree for $K_{i}$; \par {\bf end} \medskip Let $\varphi(\alpha)$, where $\alpha=${\prefcirc }$\mp \LargeQ M\delta$ i $(\circ , \mp , {\LargeQ}) \in$ $\{(+, \epsilon , \bigcup),$ $(-, \epsilon , \bigcap),$ $(-, \neg , \bigcup),$ $(+, \neg , \bigcap )\}$, be a partial function defining the fixed increment of prefix elements of a given formula during the application of the scheme (12): \medskip \medskip \medskip \newbox\ala \setbox\ala=\vtop{\parindent=0pt \hsize68mm $M = \hbox{\bf if}~ \gamma~ \hbox{\bf then}~ N~ \hbox{\bf else}~ N'~ \hbox{\bf fi}$~~and~~$\varphi(N)$, \par $\varphi(N')$ are defined and $\varphi(N)=\varphi(N')$,\par} \newbox\alaB \setbox\alaB=\vtop{\parindent=0pt \hsize68mm $M=\hbox{\bf begin}~N; N' \hbox{\bf end}$ ~and~ $\varphi(N), \varphi(N')$ \par are defined,\par} \newbox\alaC \setbox\alaC=\vtop{\parindent=0pt \hsize68mm $M = \hbox{\bf while}~ \gamma~ \hbox{\bf do}~ N~ \hbox{\bf od}$~~and~~$\varphi(N)$ is\par defined,\par} %$\cases{M_{\hM}(s) & if \box\ala\cr %\noalign{\vskip5mm} % M'_{\hM}(s) & if $(\neg \gamma)_{\hM}(s)={\bf 1}$,\cr % }$ \noindent $\varphi(\alpha)=$ $\cases{0 & when $M={\it Id}$,\cr \noalign{\vskip2mm} 1 & when $M \in V_{p}$,\cr \noalign{\vskip2mm} \varphi(N)+\varphi(N') & when \box\alaB\cr \noalign{\vskip2mm} \varphi(N) & when \box\ala\cr % ~~gdy~ $M = {\bf if} \gamma {\bf then}~ N_{1}~ {\bf else}~ N_{2}~ {\bf fi}$ % $\varphi(N_{1})=\varphi(N_{2})$ oraz $N_{1}, N_{2}$ s/a zdefiniowane,\cr \noalign{\vskip2mm} \varphi(N) & when \box\alaC\cr \noalign{\vskip2mm} ndef & otherwise,\cr }$ %%\pu \eject {\bf PROC2($K_{i}$)} {\bf begin} ~~let~$\alpha_{1}, \ldots, \alpha_{n} \in K_{I} \cap S$, \leftskip16mm \item{$\beta$ --} formula with the greatest length of prefix in $K_{i}$ such that $\beta \neq \alpha_{i}$ for $i \in \{1, \ldots, n\}$, \leftskip19mm \item{$d_{i}$~=~}$\varphi(\alpha_{i})$, \leftskip16mm \item{$d$ --}length of the prefix of the formula $\beta$ decreased by 1; \leftskip0mm \smallskip ~~if $d \geq d_{i}$ then to each formula $\alpha_{i}$ apply the scheme (12) $(d-d_{i})+1$ ~~times; \smallskip ~~let $\alpha_{i}'$={\prefpcirc }$\mp \LargeQ M\delta$ be a formula obtained from $\alpha_{i}$ after application ~~of the scheme (12); \smallskip ~~$\alpha_{i}':=${\prefpcirc }$\mp \delta ~\cup~${\prefpcirc }$\mp M\delta ~\cup~ \ldots$ \line{\hfill $\ldots ~\cup~ ${\prefpcirc }$\mp M^{(d_{1} \cdot \ldots \cdot d_{i-1} \cdot d_{i+1} \cdot \ldots \cdot d_{n})+1}\delta~\cup~\delta'$} \smallskip ~~~~~~~~where $\delta'$ = {\prefcirc }$\mp M^{(d_{1} \cdot \ldots \cdot d_{i-1} \cdot d_{i+1} \cdot \ldots \cdot d_{n})+2}\LargeQ M\delta$; \smallskip ~~build the decomposition tree for $K_{i}$; {\bf end} \medskip \medskip \medskip \noindent {\bf MOTIVATION:} \smallskip \item{1.~} We do not consider formulas with empty prefixes because they can not (if they have not done it up to now) extend the sequent by formulas that could satisfy the definition of fundamental sequent. \item{2.~}From the set ${\cal P}$ we remove classes for which there exist formulas with removable prefixes because next applications of the scheme (12) do not extend the classes by formulas that satisfy the condition (ii) of the definition of fundamental sequent. \item{3.~}If there exists exactly one element from the set S in the class $K_{i}$, then we apply the scheme (12) as long as a formula with enough long prefix will be generated (enough long prefix is not comparable with any prefix of another formula from the sequent). \item{4.~}If there exist at least two formulas from the set $S$ in the class $K_{i}$ and each application of the scheme (12) to them leads us to fixed increment of prefix elements of a given formula then \itemitem{--} first apply the scheme (12) to each element from the set $S$ so many times in order to generate a formula that is not comparable with any formula from the class $K_{i}$ \itemitem{--} next apply the scheme (12) to each element from the set $S$ so many times in order to be sure that these formulas can not generate (during application of the scheme (12)) formulas that satisfy conditions of the definition of fundamental sequent; proof is by showing semantical equivalence of the formula $\alpha_{i}'$={\prefpcirc }$\mp \LargeQ M\delta$ and the formula \smallskip \itemitem{}{\prefpcirc }$\mp \delta ~\cup~${\prefpcirc }$\mp M\delta ~\cup~ \ldots ~\cup~ ${\prefpcirc }$\mp M^{(d_{1} \cdot \ldots \cdot d_{i-1} \cdot d_{i+1} \cdot \ldots \cdot d_{n})+1}\delta$. \r 4. Final remark \\ In appendix we give two experimental work concerning automated theorem proving with system IPAL (see [5]) that bases on the proof system for algorithmic logic ([4,5]). Experiments are presented in form of computer printings. The computer printings in comparision with these generated by the computer system IPAL have changed a little in order to obtain better readability. The experiments are the following: \medskip {\bf uyes.prn}~--~the example showing described before criterion of decidability in the case when input formula is tautology, \par \medskip {\bf uno.prn}~--~~the example showing described before criterion of decidability in the case when input formula is not tautology. \par \medskip \medskip \r References\\ \item{[1]}Chlebus, B.: {\it On the decidability of propositional algorithmic logic}, ``Zeitschr. f. math. Logik und Grundlagen d.~Math.'', Bd~28, pp. 247-261, 1982 \item{[2]}Leibniz, G.W.: {\it De Principio Individui}, 1663 \item{[3]}Mirkowska, G., Salwicki, A.: {\it Algorithmic Logic}, D.~Reidel Publishing Company, Dordrecht, 1987 \item{[4]}Zalewska, A.: {\it On a certain deduction system with matainduction}, ``Studies in Logic, Grammar and Rhetoric'', XII//XIII, pp 95-121, 1993//94 \item{[5]}Zalewska, A.: {\it Interactive Prover for Programs Properties Expressed in Algorithmic Logic}, Doctoral Dissertation, Warsaw University, 1996 \vfill \eject \font\ttex=cmtex10 scaled\magstephalf \font\tt=cmtt10 scaled\magstephalf \tt \newdimen\dl \dl=5mm \newdimen\wys \wys=\baselineskip \newdimen\gr \gr=.5pt \def\alfa{{\ttex\char2}} \def\beta{{\ttex\char3}} \def\ffi{\char28} \def\neg{{\ttex\char5}} \def\cap{{\ttex\char18}} \def\bl{\char123} \def\br{\char125} \def\ff{~~~~} \let\\=\pu \parindent0pt \def\v #1.#2.#3.{\vbox to0pt{ \vskip#2\wys \vskip.3\wys \line{\hskip#1\dl\vrule width \gr height #3\wys depth0pt\hss} \vss}} \def\h #1.#2.#3.{\vbox to0pt{ \vskip#2\wys \vskip.3\wys \line{\hskip#1\dl\vrule width #3\dl height \gr depth0pt\hss} \vss}} \newdimen\dlugosc \newdimen\wysokosc \def\vv #1.#2.#3.{\vbox to0pt{ \vskip#2\wys \vskip.3\wys \wysokosc=#3\wys \advance\wysokosc by -.3\wys \vskip.3\wys \line{\hskip#1\dl\vrule width \gr height \wysokosc depth0pt\hss} \vss}} \def\hh #1.#2.#3.{\vbox to0pt{ \vskip#2\wys \vskip.3\wys \dlugosc=#3\dl \advance\dlugosc by -.2\dl \line{\hskip#1\dl\vrule width \dlugosc height \gr depth0pt \vbox to0pt{\vss $\scriptstyle{\lor}$\vskip-.6mm}\hss} \vss}} \def\hhh #1.#2.#3.{\vbox to0pt{ \vskip#2\wys \vskip.3\wys \dlugosc=#3\dl \advance\dlugosc by -.2\dl \line{\hskip#1\dl\vrule width \dlugosc height 0pt depth0pt \vbox to0pt{\vss $\scriptstyle{\lor}$\vskip-.6mm}\hss} \vss}} \def\t #1.#2.#3...{\vbox to0pt{ \vskip#2\wys \line{\hskip#1\dl\hskip1mm \vphantom{(/S}#3\hss} \vss}} \pu\pu\pu \centerline{\bf APPENDIX} \pu\pu\pu uyes.prn \centerline{I P A L - BEGIN OF DOCUMENTATION} INPUT: \ff K(K(U begin K;K end {\alfa})) v {\neg}K(K(K(K(K({\cap} begin K;K;K;K;K \ff end {\alfa}))))) The formula tree: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.1,5. \h 1.1.1. \h 1.2.1. \t 2.1.KKU begin K;K end ({\alfa})... \t 2.2.{\neg}KKKKK{\cap} begin K;K;K;K;K end ({\alfa})... } \\\\\\ The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.3. \vv 2.1,5.1,5. \vv 2.3,5.1,5. \hh 1.1,5.1. \hh 1.3,5.1. \h 2.2.1. \h 2.3.1. \h 2.4.1. \h 2.5.1. \t 3.2.KKId{\alfa}... \t 3.3.KKKKU begin K;K end ({\alfa})... \t 3.4.{\neg}KKKKKId{\alfa}... \t 3.5.{\neg}KKKKKKKKKK{\cap} begin K;K;K;K;K end ({\alfa})... } \\\\\\\\\\\\ The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ \neg KKKKKKKKKK{\cap} begin K;K;K;K;K end (\alfa), KKKKU begin K;K \ff ~~end (\alfa), {\neg}KKKKKId\alfa, KKId\alfa\br\ Not\_fund Let us consider the following pair : \ff <\bl\ KKKKU begin K;K end (\alfa), {\neg}KKKKKKKKKK{\cap} begin K;K;K;K;K \ff ~~~end (\alfa), KKId\alfa, {\neg}KKKKKId\alfa\br, \bl{\ffi}\br> The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.6,5. \vv 2.1,5.1,5. \vv 2.3,5.1,5. \hh 1.1,5.1. \hh 1.3,5.1. \h 2.2.1. \h 2.3.1. \h 2.4.1. \h 2.5.1. \h 1.6.1. \h 1.7.1. \t 3.2.KKKKId{\alfa}... \t 3.3.KKKKKKU begin K;K end ({\alfa})... \t 3.4.{\neg}KKKKKKKKKKId{\alfa}... \t 3.5.{\neg}KKKKKKKKKKKKKKK{\cap} begin K;K;K;K;K end ({\alfa})... \t 2.6.KKId{\alfa}... \t 2.7.{\neg}KKKKKId{\alfa}... } %%\\\\\\\\\\\\\\\\ \vfill\eject The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ \neg KKKKKKKKKKKKKKK\cap\ begin K;K;K;K;K end (\alfa), KKKKKKU begin \ff ~~K;K end (\alfa), \neg KKKKKKKKKKId\alfa, KKKKId\alfa, KKId\alfa, \neg KKKKKId\alfa\br \ff ~~Not\_fund Let us consider the following pair: \ff <\bl\ KKKKKKU begin K;K end (\alfa), \neg KKKKKKKKKKKKKKK\cap\ begin \ff ~~~K;K;K;K;K end (\alfa), KKId\alfa, KKKKId\alfa, \neg KKKKKId\alfa, \ff ~~~\neg KKKKKKKKKKId\alfa\br, \bl\ffi\br> The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.10,5. \vv 2.1,5.1,0. \vv 2.5,5.1,5. \vv 3.2,5.1,0. \vv 4.3,5.1,5. \hh 1.1,5.1. \h 2.2.1. \hh 2.2,5.1. \h 3.3.1. \hh 3.3,5.1. \h 4.4.1. \h 4.5.1. \hh 1. 5,5.1. \h 2. 6.1. \h 2. 7.1. \h 1. 8.1. \h 1. 9.1. \h 1.10.1. \h 1.11.1. \t 3.2.KKKKKKId\alfa... \t 4.3.KKKKKKKKId\alfa... \t 5.4.KKKKKKKKKKId\alfa... \t 5.5.KKKKKKKKKKKKU begin K;K end (\alfa)... \t 3.6.\neg KKKKKKKKKKKKKKKId\alfa... \t 3.7.\neg KKKKKKKKKKKKKKKKKKKK\cap\ begin K;K;K;K;K end (\alfa)... \t 2.8.KKId\alfa... \t 2.9.KKKKId\alfa... \t 2.10.\neg KKKKKId\alfa... \t 2.11.\neg KKKKKKKKKKId\alfa... } \\\\\\\\\\\\\\\\\\\\\\\\ The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ \neg KKKKKKKKKKKKKKKKKKKK\cap\ begin K;K;K;K;K end (\alfa), \ff ~~KKKKKKKKKKKKU begin K;K end (\alfa), \neg KKKKKKKKKKKKKKKId\alfa, \ff ~~KKKKKKKKKKId\alfa, KKKKKKKKId\alfa, KKKKKKId\alfa, KKId\alfa, KKKKId\alfa, \ff ~~\neg KKKKKId\alfa, \neg KKKKKKKKKKId\alfa\br\ Fund THE INPUT FORMULA IS ACCEPTED \centerline{END OF IPAL DOCUMENTATION} \pu \vfill \line{\hrulefill} \vskip-4mm \line{\hrulefill} \vfill \pu uno.prn \centerline{I P A L - BEGIN OF DOCUMENTATION} INPUT: \ff K'(M(K(M \alfa))) v \neg\cap\ K(K ola) v M(U K'\beta) v K(U M \alfa) v \ff M(K(\neg\cap K\alfa)) v \neg M(\cap\ K' ala) v M(K'(U K a)) v \ff M(K'(U M ada)) v K(K(K(fred))) \eject The formula tree: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.8,5. \h 1.1.1. \h 1.2.1. \h 1.3.1. \h 1.4.1. \h 1.5.1. \h 1.6.1. \h 1.7.1. \h 1.8.1. \h 1.9.1. \t 2.1.K'MKM\alfa... \t 2.2.\neg\cap K(K(ola))... \t 2.3.MUK'(\beta)... \t 2.4.KUM(\alfa)... \t 2.5.MK\neg\cap K(\alfa)... \t 2.6.\neg M\cap K'(ala)... \t 2.7.MK'UK(a)... \t 2.8.MK'UM(ada)... \t 2.9.KKKfred... } \\\\\\\\\\\\\\\\\\\\ The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.15,5. \hh 1.1,5.1. \hh 1.3,5.1. \hh 1.5,5.1. \hh 1.7,5.1. \hh 1.9,5.1. \hh 1.11,5.1. \hh 1.13,5.1. \vv 2.1,5.1,5. \vv 2.3,5.1,5. \vv 2.5,5.1,5. \vv 2.7,5.1,5. \vv 2.9,5.1,5. \vv 2.11,5.1,5. \vv 2.13,5.1,5. \h 1.1.1. \h 2.2.1. \h 2.3.1. \h 2.4.1. \h 2.5.1. \h 2.6.1. \h 2.7.1. \h 2.8.1. \h 2.9.1. \h 2.10.1. \h 2.11.1. \h 2.12.1. \h 2.13.1. \h 2.14.1. \h 2.15.1. \h 1.16.1. \t 2.1.K'MKMId\alfa... \t 3.2.\neg KIdola... \t 3.3.\neg K\cap K(K(ola))... \t 3.4.MId\beta... \t 3.5.MK'UK'(\beta)... \t 3.6.KId\alfa... \t 3.7.KMUM(\alfa)... \t 3.8.MK\neg Id\alfa... \t 3.9.MK\neg K\cap K(\alfa)... \t 3.10.\neg MIdala... \t 3.11.\neg MK'\cap K'(ala)... \t 3.12.MK'Ida... \t 3.13.MK'KUK(a)... \t 3.14.MK'Idada... \t 3.15.MK'MUM(ada)... \t 2.16.KKKIdfred... } \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\ The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ MK'MUM(ada), MK'KUK(a), \neg MK'\cap K'(ala), MK\neg K\cap K(\alfa), \ff ~~KMUM(\alfa), MK'UK'(\beta), \neg K\cap K(K(ola)), MK'Idada, MK'Ida, \ff ~~\neg MIdala, MK\neg Id\alfa, KId\alfa, MId\beta, \neg KIdola, K'MKMId\alfa, \ff ~~KKKIdfred\br\ Not\_fund \vfill \eject Let us consider the following pair: \ff <\bl\ MK'MUM(ada), MK'KUK(a), \neg MK'\cap K'(ala), MK\neg K\cap K(\alfa), \ff ~~~KMUM(\alfa), MK'UK'(\beta), \neg K\cap K(K(ola)), MK'Idada, MK'Ida, \ff ~~~\neg MIdala, MK\neg Id\alfa, KId\alfa, MId\beta, \neg KIdola, K'MKMId\alfa, \ff ~~~KKKIdfred\br, \bl\ffi\br> Now we obtain 3 following possible pair(s) to check: \ff <\bl\ \neg K\cap K(K(ola)), KMUM(\alfa), KId\alfa, \neg KIdola, KKKIdfred\br, \bl\ffi\br> \ff <\bl\ MK'UK'(\beta), \neg MK'\cap K'(ala), MK'KUK(a), \neg MIdala, MId\beta, \ff ~~~MK'Ida, MK\neg Id\alfa, MK'Idada\br, \bl\ffi\br> \ff <\bl\ MK'UK'(\beta), \neg MK'\cap K'(ala), MK'MUM(ada), \neg MIdala, MId\beta, \ff ~~~MK'Ida, MK\neg Id\alfa, MK'Idada\br, \bl\ffi\br> Let us consider the following pair: \ff <\bl\ \neg K\cap K(K(ola)), KMUM(\alfa), KId\alfa, \neg KIdola, KKKIdfred\br, \bl\ffi\br> The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.10,5. \hh 1.1,5.1. \h 2.2.1. \hh 2.2,5.1. \h 3.3.1. \hh 3.3,5.1. \h 4.4.1. \h 4.5.1. \hh 1.5,5.1. \h 2.6.1. \hh 2.6,5.1. \h 3.7.1. \h 3.8.1. \h 1.9.1. \h 1.10.1. \h 1.11.1. \vv 2.1,5.1,0. \vv 3.2,5.1,0. \vv 4.3,5.1,5. \vv 2.5,5.1,0. \vv 3.6,5.1,5. \t 3.2.\neg KKIdola... \t 4.3.\neg KKKIdola... \t 5.4.\neg KKKKIdola... \t 5.5.\neg KKKK\cap K(K(ola))... \t 3.6.KMId\alfa... \t 4.7.KMMId\alfa... \t 4.8.KMMMUM(\alfa)... \t 2.9.KId\alfa... \t 2.10.\neg KIdola... \t 2.11.KKKIdfred... } \\\\\\\\\\\\\\\\\\\\\\\\ The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ KMMMUM(\alfa), \neg KKKK\cap K(K(ola)), KMMId\alfa, KMId\alfa, \neg KKKKIdola, \ff ~~\neg KKKIdola, \neg KKIdola, KId\alfa, \neg KIdola, KKKIdfred\br\ Not\_fund Let us consider the following pair: \ff <\bl\ KMMMUM(\alfa), \neg KKKK\cap K(K(ola)), KMMId\alfa, KMId\alfa, \neg KKKKIdola, \ff ~~~\neg KKKIdola, \neg KKIdola, KId\alfa, \neg KIdola, KKKIdfred\br, \bl\ffi\br> Now we obtain 0 following possible pair(s) to check. Let us check the next one. Let us consider the following pair: \ff <\bl\ MK'UK'(\beta), \neg MK'\cap K'(ala), MK'KUK(a), \neg MIdala, MId\beta, \ff ~~~MK'Ida, MK\neg Id\alfa, MK'Idada\br, \bl\ffi\br> \vfill\eject The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.11,5. \hh 1.1,5.1. \h 2.2.1. \h 2.3.1. \hh 1.3,5.1. \h 2.4.1. \h 2.5.1. \hh 1.5,5.1. \h 2.6.1. \h 2.7.1. \h 1.8.1. \h 1.9.1. \h 1.10.1. \h 1.11.1. \h 1.12.1. \vv 2.1,5.1,5. \vv 2.3,5.1,5. \vv 2.5,5.1,5. \t 3.2.MK'Id\beta... \t 3.3.MK'K'UK'(\beta)... \t 3.4.\neg MK'Idala... \t 3.5.\neg MK'K'\cap K'(ala)... \t 3.6.MK'KIda... \t 3.7.MK'KKUK(a)... \t 2.8.\neg MIdala... \t 2.9.MId\beta... \t 2.10.MK'Ida... \t 2.11.MK\neg Id\alfa... \t 2.12.MK'Idada... } \\\\\\\\\\\\\\\\\\\\\\\\\\ The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ MK'KKUK(a), \neg MK'K'\cap K'(ala), MK'K'UK'(\beta), MK'KIda, \ff ~~\neg MK'Idala, MK'Id\beta, \neg MIdala, MId\beta, MK'Ida, MK\neg Id\alfa, \ff ~~MK'Idada\br\ Not\_fund Let us consider the following pair: \ff <\bl\ \neg MK'K'\cap K'(ala), MK'K'UK'(\beta), \neg MIdala, MId\beta, \neg MK'Idala, \ff ~~~MK'Id\beta, MK'Ida, MK\neg Id\alfa, MK'Idada, MK'KIda\br, \bl\ffi\br> The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.14,5. \hh 1.1,5.1. \h 2.2.1. \hh 2.2,5.1. \h 3.3.1. \h 3.4.1. \hh 1.4,5.1. \h 2.5.1. \hh 2.5,5.1. \h 3.6.1. \h 3.7.1. \h 1.8.1. \h 1.9.1. \h 1.10.1. \h 1.11.1. \h 1.12.1. \h 1.13.1. \h 1.14.1. \h 1.15.1. \vv 2.1,5.1,0. \vv 3.2,5.1,5. \vv 2.4,5.1,0. \vv 3.5,5.1,5. \t 3.2.\neg MK'K'Idala... \t 4.3.\neg MK'K'K'Idala... \t 4.4.\neg MK'K'K'K'\cap K'(ala)... \t 3.5.MK'K'Id\beta... \t 4.6.MK'K'K'Id\beta... \t 4.7.MK'K'K'K'UK'(\beta)... \t 2.8.\neg MIdala... \t 2.9.MId\beta... \t 2.10.\neg MK'Idala... \t 2.11.MK'Id\beta... \t 2.12.MK'Ida... \t 2.13.MK\neg Id\alfa... \t 2.14.MK'Idada... \t 2.15.MK'KIda... } \vfill\eject %%\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\ The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ MK'K'K'K'UK'(\beta), \neg MK'K'K'K'\cap K'(ala), MK'K'K'Id\beta, \ff ~~MK'K'Id\beta, \neg MK'K'K'Idala,\neg MK'K'Idala, \neg MIdala, MId\beta, \ff ~~\neg MK'Idala, MK'Id\beta, MK'Ida, MK\neg Id\alfa, MK'Idada, MK'KIda\br \ff ~~Not\_fund Let us consider the following pair: \ff <\bl\ MK'UK'(\beta), \neg MK'\cap K'(ala), MK'MUM(ada), \neg MIdala, MId\beta, \ff ~~~MK'Ida, MK\neg Id\alfa, MK'Idada\br, \bl\ffi\br> The main sequent is not accepted The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.11,5. \hh 1.1,5.1. \h 2.2.1. \h 2.3.1. \hh 1.3,5.1. \h 2.4.1. \h 2.5.1. \hh 1.5,5.1. \h 2.6.1. \h 2.7.1. \h 1.8.1. \h 1.9.1. \h 1.10.1. \h 1.11.1. \h 1.12.1. \vv 2.1,5.1,5. \vv 2.3,5.1,5. \vv 2.5,5.1,5. \t 3.2.MK'Id\beta... \t 3.3.MK'K'UK'(\beta)... \t 3.4.\neg MK'Idala... \t 3.5.\neg MK'K'\cap K'(ala)... \t 3.6.MK'MIdada... \t 3.7.MK'MMUM(ada)... \t 2.8.\neg MIdala... \t 2.9.MId\beta... \t 2.10.MK'Ida... \t 2.11.MK\neg Id\alfa... \t 2.12.MK'Idada... } \\\\\\\\\\\\\\\\\\\\\\\\\ The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ MK'MMUM(ada), \neg MK'K'\cap K'(ala), MK'K'UK'(\beta), MK'MIdada, \ff ~~\neg MK'Idala, MK'Id\beta, \neg MIdala, MId\beta, MK'Ida, MK\neg Id\alfa, \ff ~~MK'Idada\br\ Not\_fund Let us consider the following pair: \ff <\bl\ \neg MK'K'\cap K'(ala), MK'K'UK'(\beta), \neg MIdala, MId\beta, \neg MK'Idala, \ff ~~~MK'Id\beta, MK'Ida, MK\neg Id\alfa, MK'Idada, MK'MIdada\br, \bl\ffi\br> \vfill\eject The formula tree after using IPAL rules: {\offinterlineskip \hhh 0,5.0,5.0,5. \vv 1.0,5.14,5. \hh 1.1,5.1. \h 2.2.1. \hh 2.2,5.1. \h 3.3.1. \h 3.4.1. \hh 1.4,5.1. \h 2.5.1. \hh 2.5,5.1. \h 3.6.1. \h 3.7.1. \h 1.8.1. \h 1.9.1. \h 1.10.1. \h 1.11.1. \h 1.12.1. \h 1.13.1. \h 1.14.1. \h 1.15.1. \vv 2.1,5.1,0. \vv 3.2,5.1,5. \vv 2.4,5.1,0. \vv 3.5,5.1,5. \t 3.2.\neg MK'K'Idala... \t 4.3.\neg MK'K'K'Idala... \t 4.4.\neg MK'K'K'K'\cap K'(ala)... \t 3.5.MK'K'Id\beta... \t 4.6.MK'K'K'Id\beta... \t 4.7.MK'K'K'K'UK'(\beta)... \t 2.8.\neg MIdala... \t 2.9.MId\beta... \t 2.10.\neg MK'Idala... \t 2.11.MK'Id\beta... \t 2.12.MK'Ida... \t 2.13.MK\neg Id\alfa... \t 2.14.MK'Idada... \t 2.15.MK'MIdada... } \\\\\\\\\\\\\\\\\\\\\\\\\\\\\\\ The number of sequents for the above formula tree: 1 Sequents: \ff \bl\ MK'K'K'K'UK'(\beta), \neg MK'K'K'K'\cap K'(ala), MK'K'K'Id\beta, \ff ~~MK'K'Id\beta, \neg MK'K'K'Idala, \neg MK'K'Idala, \neg MIdala, MId\beta, \ff ~~\neg MK'Idala, MK'Id\beta, MK'Ida, MK\neg Id\alfa, MK'Idada, MK'MIdada\br \ff ~~Not\_fund Let us consider the following pair: \ff <\bl\ \neg K\cap K(K(ola)), KMUM(\alfa), MK'UK'(\beta), \neg MK'\cap K'(ala), \ff ~~~\neg MIdala, KId\alfa, MId\beta, \neg KIdola, MK'Ida, MK'KUK(a), \ff ~~~MK\neg Id\alfa, MK'MUM(ada), MK\neg K\cap K(\alfa), MK'Idada, KKKIdfred, \ff ~~~K'MKMId\alfa\br, \bl\ffi\br> The main sequent is not accepted THE INPUT FORMULA IS NOT ACCEPTED \centerline{END OF IPAL DOCUMENTATION} \end