STUDIES IN LOGIC, GRAMMAR AND RHETORIC 1 (14)

Anna Zalewska

A CRITERION OF DECIDABILITY OF SOME ALGORITHMIC FORMULAS

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.

1. Introduction

It was Leibniz [3] who first claimed 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.

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.

Anna Zalewska

2. Basic notions

Let us remind that the alphabet of the language of propositional algorithmic logic

A_{P AL} = V_{0} ∪ V_{p} ∪ L_{c} ∪ L_{con} ∪ I_{q} ∪ P_{c} ∪ A_{s}

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 logical constants ({true, false}), L_{con} denotes the set of logical connectives ({¬, ∨, ∧, ⇒}) and I_{q} denotes the set of iteration quantifiers ({⋃, ⋂}), P_{c} is the set of program connectives ({begin −; − end, if − then − else − fi, while − do − od}) and A_{s} is the set of auxiliary signs ({(,)}).

The set of all programs is the least extension of the set V_{p} and program constant Id such that if γ is a classical propositional formula and M, M′ are programs then the expressions begin M; M′ end, if γ then M else M′ fi, while γ do M od are programs.

The set of all formulas is the least extension of the set of classical propositional formulas such that if M is a program and α and β are formulas then (α ∨ β), (α ∧ β), (α ⇒ β), ¬α Mα, ⋃ Mα, ⋂ Mα are formulas too.

Let pref^{∘} stand for prefix i.e. finite sequence, perhaps empty, of the form ∓K_{1} ∓ K_{2} … ∓ K_{l} where K_{i} ∈ V_{p} and ∓K_{i} is ¬K_{i} when “∓”=“¬” or K_{i} when “∓”=“ε”, and “∘”=“+” if the number of programs with negation occurring in prefix is even, otherwise “∘”=“+”. An absolute value of ∓K_{i} is defined in the following way

| ∓ K_{i}| = \{ \begin{matrix}¬(∓K_{i}) & if “∓”=“¬” \\ (∓K_{i}) & if “∓”=“ε” \end{matrix}

Let pref^{∘} (pref′^{∘}) will be of the form ∓K_{1} ∓K_{2} …∓K_{l} (∓L_{1} ∓L_{2} …∓ L_{l}). The absolute value of the prefix pref^{∘} is equal to the absolute value of the prefix pref′^{∘} if for all indexes i = 1, …, n | ∓ K_{i}| = | ∓ L_{i}| (we will denote the equality writing |pref| = |pref′|). We will write pref_{k}^{−} (pref_{k}^{+}) in order to mark the fact that the first k elements of the prefix pref^{∘} set up the subprefix in which the number of programs with negation occurring in it is even (uneven).

Let Π be a finite sequence of formulas. A prefix pref is said to be removable in the sequence Π if the following conditions hold

(*) ∃_{β∈Π}(β = pref^{∘}β′) and

On a Certain Deduction System with Metainduction

(**) ∀_{k∈{1,...,l}}∃_{β∈Π}(β = pref′^{−}β′ ∧ |pref′| = |pref_{k}|)

where l denotes the length of the prefix pref and β′ is an arbitrary formula.

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]).

According to notational conventions, used in the literature, by Δ, Δ′, Γ, Γ′, Π, Π′, Σ and Σ′ (possible with indices) we denote sequents, i.e. finite sequence (maybe empty) of formulas. By {Γ, α, Δ} we shall mean a sequence in which we have first Γ, next α and lastly Δ.

In the PS system conclusion and premises of the rules will be presented as ordered pair of the form

(*) ⟨Π, 𝒜⟩

where Π denotes main sequent, 𝒜 stands for set (maybe empty) of sequents.

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

\frac{⟨Π, 𝒜⟩}{⟨Π′, 𝒜′⟩}  or  \frac{⟨Π, 𝒜⟩}{⟨Π′, 𝒜′⟩ ; ⟨Π′′, 𝒜′′⟩}

In all the below schemes Γ denotes a set of indecomposable formulas and Δ is an arbitrary set of formulas; α, β are arbitrary formulas; γ denotes an open formula; M, M′, M′′ denote arbitrary programs; p ∈ V_{0}; ∘ ∈ {−, +}; ∓ ∈ {¬, ε}; □ ∈ {∧, ∨}; Q ∈ {⋃, ⋂}.

The basic decomposition rules of PS system are presented below.

(1)

\frac{⟨\{Γ, pref^{∘}true, Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘}¬false, Δ\}, 𝒜⟩}

Anna Zalewska

(2)

\frac{⟨\{Γ, pref^{∘}¬true, Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘}false, Δ\}, 𝒜⟩}

(3)

\frac{⟨\{Γ, pref^{∘}¬¬α, Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘}α, Δ\}, 𝒜⟩}

(4)

\frac{⟨\{Γ, pref^{∘} ∓ (α ⇒ β), Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ (¬α ∨ β), Δ\}, 𝒜⟩}

(5)

\frac{⟨\{Γ, pref^{∘} ∓ (α□β), Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ α, Δ\}, 𝒜⟩; ⟨\{Γ, pref^{∘} ∓ β, Δ\}, 𝒜⟩}

where (∘, ∓, □) ∈ {(−, ε, ∨), (+, ε, ∧), (+, ¬, ∨), (−, ¬, ∧)}

(6)

\frac{⟨\{Γ, pref^{∘} ∓ (α□β), Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ α, pref^{∘} ∓ β, Δ\}, 𝒜⟩}

where (∘, ∓, □) ∈ {(+, ε, ∨), (−, ε, ∧), (−, ¬, ∨), (+, ¬, ∧)}

(7)

\frac{⟨\{Γ, pref^{∘} ∓ Idα, Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ α, Δ\}, 𝒜⟩}

where α ∉ {false, p}

(8)

\frac{⟨\{Γ, pref^{∘} ∓ α, Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ Idα, Δ\}, 𝒜⟩}

where α ∈ {false, p} and Id is not an element of the prefix pref^{∘}

(9)

\frac{⟨\{Γ, pref^{∘} ∓ begin M′; M′′ endα, Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ M′(M′′α), Δ\}, 𝒜⟩}

(10)

\frac{⟨\{Γ, pref^{∘} ∓ if γ then M′ else M′′ fiα, Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ ((γ ∧ M′α) ∨ (¬γ ∧ M′′α)), Δ\}, 𝒜⟩}

(11)

\frac{⟨\{Γ, pref^{∘} ∓ while γ do M odα, Δ\}, 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ ⋃ if γ then M fi(¬γ ∧ α), Δ\}, 𝒜⟩}

(12)

\frac{⟨\{Γ, pref^{∘} ∓ QMα, Δ), 𝒜⟩}{⟨\{Γ, pref^{∘} ∓ α, Δ, pref^{∘} ∓ MQMα\}, 𝒜⟩}

The main sequent Π of the ordered pair ⟨Π, 𝒜⟩ is said to be • indecomposable iff no P S rule can be applied to it,

• fundamental iff the formulas pref^{−}α and pref^{′+}α satisfying the conditions (I-II) belong to the sequent Π or the formula pref^{−}false satisfying the conditions (II) belongs to the sequent Π where (I) |pref| = |pref′|, (II) pref is not empty and removable in the sequent Π,

• 𝒜-provable iff there exists a sequent Σ ∈ 𝒜 such that

∀_{α∈Σ}∃_{β∈Π}(β is equal to α) (we will say sometimes that Π is 𝒜-provable with respect to the sequent Σ),

• 𝒜^{∗}-provable iff there exists a sequent Σ ∈ 𝒜 for which Σ^{−} ≠ ∅ (where Σ^{−} = {β ∈ Σ|β = ¬β′}) and there exists a sequence L of program variables L_{1} … L_{m} such that

∀_{α∈Σ}∃_{β∈Π}(β is equal to α_{L})

where α_{L} = ±L_{1} … L_{m}α′ if α = ±α′ and “±”∈ {¬, ε}

• terminal iff Π is indecomposable but Π is neither fundamental nor 𝒜provable nor 𝒜^{∗}-provable.

A proof of the sequent Π 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 ⟨Π, 𝒜⟩ where Π is fundamental or 𝒜-provable or 𝒜^{∗}-provable.

4. A criterion of decidability

In PS system its decidability is reduced to solution the problem

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.

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 < Π, A > whether another application of the scheme (12) to a given formula Π of the main sequent do not lead us to state that the sequent is fundamental or A^{∗}-provable.

The second case of described above problem is enough simple. In order to check whether the sequent {Γ,pref^{∘}∓QMα, Δ}, where (∘, ∓, Q) ∈ {(+, ϵ, ⋃), (−, ϵ, ⋂), (−, ¬, ⋃), (+, ¬, ⋂)} is A^{∗}-provable with respect to the sequent {Γ′,pref’^{∘}∓QMα, Δ′} ∈ A and the sequence of programs L_{1}, …, L_{n} it is enough to check whether the length of the prefix pref^{∘} is greater then sum of the number n and the length of the prefix pref’^{∘}. If it is true then next application of the scheme (12) is needless.

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 what is not convenient during implementation.

Presented below strategy allows us in many cases to eliminate symbols ⋃, ⋂ from formulas to which the scheme (12) can be applied.

STRATEGY:

Let Π be a sequent containing the set of formulas S = {δ_{1}, …, δ_{n}} such that their prefixes are not empty and the scheme (12) can be applied to the formulas. The formulas are in the form

pref^{∘}∓QMδ

where (∘, ∓, Q) ∈ {(+, ϵ, ⋃), (−, ϵ, ⋂), (−, ¬, ⋃), (+, ¬, ⋂)}.

1. Separate from Π the set P such that its elements are classes of formulas from the sequent Π and for each class K_{i} ∈ P two following conditions are satisfied:

– at least one formula from the set S belongs to K_{i}

– prefixes of formulas belonging to K_{i} (from which program constants Id are removed) can be presented as the following sequence

| pref1 | ⊆ | pref2 | ⊆ … ⊆ | prefm |, where m is the number of formulas in the class K_{i}

– for each two classes K_{i}, K_{j} ∈ P neither K_{i} ⊆ K_{j} nor K_{j} ⊆ K_{i}.

2. Remove from the set 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.

3. For each class K_{i} such that – exactly one formula from the set S belongs to K_{i} 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.

4. For each class K_{i} such that – at least two formulas from the set S belong to K_{i} and

– each application of the scheme (12) to K_{i} leads to fixed increment of prefix elements of a given formula

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.

5. For each class K_{i} such that – K_{i} does not satisfy conditions of the point 3 or 4 use Chlebus’s method.

Below we give two mentioned before procedures.

PROC1(K_{i}) begin let α=pref^{∘}∓QMδ ∈ K_{i} ∩ S,

β – formula with the greatest length of prefix in K_{i}

such that β ≠ α, d_{1} – length of the prefix of the formula α, d_{2} – length of the prefix of the formula β decreased

by 1, if d_{2} ≥ d_{1} then α :=pref^{∘}∓δ ∪ pref^{∘}∓Mδ ∪ … ∪ pref^{∘}∓M^{(d_{2}−d_{1})+1}δ ∪ δ′

where δ′ = pref^{∘}∓M^{(d_{2}−d_{1})+2}QMδ; build the decomposition tree for K_{i}; end

Let φ(α), where α =pref^{∘}∓QMδ i (∘, ∓, Q) ∈ {(+, ϵ, ⋃), (−, ϵ, ⋂), (−, ¬, ⋃), (+, ¬, ⋂)}, be a partial function defining the fixed increment of prefix elements of a given formula during the application of the scheme (12):

φ(α) = \{ \begin{matrix}0 & when M = Id, \\ 1 & when M ∈ V_{p}, \\ φ(N) + φ(N′) & when M = begin N; N′end and φ(N), φ(N′) are defined, \\ φ(N) & when M = if γ then N else N′ fi and φ(N), φ(N′) are defined and φ(N) = φ(N′), \\ φ(N) & when M = while γ do N od and φ(N) is defined, \\ ndef & otherwise, \end{matrix}

PROC2(K_{i}) begin let α_{1}, …, α_{n} ∈ K_{I} ∩ S,

β – formula with the greatest length of prefix in K_{i} such that

β ≠ α_{i} for i ∈ {1, …, n}, d_{i} = φ(α_{i}), d – length of the prefix of the formula β decreased by 1;

if d ≥ d_{i} then to each formula α_{i} apply the scheme (12) (d − d_{i}) + 1 times; let α′_{i}=pref’^{∘}∓QMδ be a formula obtained from α_{i} after application of the scheme (12); α′_{i} :=pref’^{∘}∓δ ∪ pref’^{∘}∓Mδ ∪ …

… ∪ pref’^{∘}∓M^{(d_{1}·...·d_{i−1}·d_{i+1}·...·d_{n})+1}δ ∪ δ′

where δ′ = pref^{∘}∓M^{(d_{1}·...·d_{i−1}·d_{i+1}·...·d_{n})+2}QMδ;

build the decomposition tree for K_{i}; end

MOTIVATION:

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.

2. From the set 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.

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).

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

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

– 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 α′_{i}=pref’^{∘}∓QMδ and the formula pref’^{∘}∓δ ∪ pref’^{∘}∓Mδ ∪ … ∪ pref’^{∘}∓M^{(d_{1}·...·d_{i−1}·d_{i+1}·...·d_{n})+1}δ.

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:

uyes.prn – the example showing described before criterion of decidability in the case when input formula is tautology,

uno.prn – the example showing described before criterion of decidability in the case when input formula is not tautology.

References

[1] Chlebus, B.: On the decidability of propositional algorithmic logic, “Zeitschr. f. math. Logik und Grundlagen d. Math.”, Bd 28, pp. 247-261, 1982

[2] Leibniz, G.W.: De Principio Individui, 1663

[3] Mirkowska, G., Salwicki, A.: Algorithmic Logic, D. Reidel Publishing Company, Dordrecht, 1987

[4] Zalewska, A.: On a certain deduction system with matainduction, “Studies in Logic, Grammar and Rhetoric”, XII//XIII, pp 95-121, 1993//94

[5] Zalewska, A.: Interactive Prover for Programs Properties Expressed in Algorithmic Logic, Doctoral Dissertation, Warsaw University, 1996

APPENDIX

uyes.prn
               I P A L - BEGIN OF DOCUMENTATION
INPUT:
    K(K(U begin K;K end  )) v  K(K(K(K(K(  begin K;K;K;K;K
    end  )))))
The formula tree:

∨

     KKU begin K;K end ( )
     KKKKK  begin K;K;K;K;K end ( )
The formula tree after using IPAL rules:

∨ \overline{∨}

\overline{∨}

        KKId
        KKKKU begin K;K end ( )
        KKKKKId
        KKKKKKKKKK  begin K;K;K;K;K end ( )
The number of sequents for the above formula tree:  1
Sequents:
    {  KKKKKKKKKK  begin K;K;K;K;K end ( ), KKKKU begin K;K
      end ( ),  KKKKKId , KKId } Not fund
Let us consider the following pair :
    <{ KKKKU begin K;K end ( ),  KKKKKKKKKK  begin K;K;K;K;K
       end ( ), KKId ,  KKKKKId }, {ø}>
The formula tree after using IPAL rules:

∨ \overline{∨}

\overline{∨}

        KKKKId
        KKKKKKU begin K;K end ( )
        KKKKKKKKKKId
        KKKKKKKKKKKKKKK  begin K;K;K;K;K end ( )
     KKId
     KKKKKId

The number of sequents for the above formula tree:  1
Sequents:
    {  KKKKKKKKKKKKKKK  begin K;K;K;K;K end ( ), KKKKKKU begin
      K;K end ( ),  KKKKKKKKKKId , KKKKId , KKId ,  KKKKKId }
      Not fund
Let us consider the following pair:
    <{ KKKKKKU begin K;K end ( ),  KKKKKKKKKKKKKKK  begin
       K;K;K;K;K end ( ), KKId , KKKKId ,  KKKKKId ,
       KKKKKKKKKKId }, {ø}>
The formula tree after using IPAL rules:

∨ \overline{∨} \overline{∨} \overline{∨}

\overline{∨}

        KKKKKKId
          KKKKKKKKId
             KKKKKKKKKKId
             KKKKKKKKKKKKU begin K;K end ( )
        KKKKKKKKKKKKKKKId
        KKKKKKKKKKKKKKKKKKKK  begin K;K;K;K;K end ( )
     KKId
     KKKKId
     KKKKKId
     KKKKKKKKKKId
The number of sequents for the above formula tree:  1
Sequents:
    {  KKKKKKKKKKKKKKKKKKKK  begin K;K;K;K;K end ( ),
      KKKKKKKKKKKKU begin K;K end ( ),  KKKKKKKKKKKKKKKId ,
      KKKKKKKKKKId , KKKKKKKKId , KKKKKKId , KKId , KKKKId ,
      KKKKKId ,  KKKKKKKKKKId } Fund
THE INPUT FORMULA IS ACCEPTED
                   END OF IPAL DOCUMENTATION

uno.prn
               I P A L - BEGIN OF DOCUMENTATION
INPUT:
    K'(M(K(M  ))) v    K(K ola) v M(U K' ) v K(U M  ) v
    M(K(  K )) v  M(  K' ala) v M(K'(U K a)) v
    M(K'(U M ada)) v K(K(K(fred)))

The formula tree:

∨ K'MKM

K(K(ola))
MUK'( )
KUM( )
MK  K( )
M K'(ala)
MK'UK(a)
MK'UM(ada)
KKKfred
The formula tree after using IPAL rules:

∨ \overline{∨}

\overline{∨}

\overline{∨}

\overline{∨}

\overline{∨}

\overline{∨}

\overline{∨}

K'MKMId
KIdola
K K(K(ola))
MId
MK'UK'( )
KId
KMUM( )
MK Id
MK K K( )
MIdala
MK' K'(ala)
MK'Ida
MK'KUK(a)
MK'Idada
MK'MUM(ada)
KKKIdfred
The number of sequents for the above formula tree:  1
Sequents:
{ MK'MUM(ada), MK'KUK(a),  MK' K'(ala), MK K K( ),
KMUM( ), MK'UK'( ),  K K(K(ola)), MK'Idada, MK'Ida,
MIdala, MK Id , KId , MId ,  KIdola, K'MKMId ,
KKKIdfred} Not fund

Let us consider the following pair:
    <{ MK'MUM(ada), MK'KUK(a),  MK' K'(ala), MK K K( ),
       KMUM( ), MK'UK'( ),  K K(K(ola)), MK'Idada, MK'Ida,
       MIdala, MK Id , KId , MId ,  KIdola, K'MKMId ,
       KKKIdfred}, {ø}>
Now we obtain 3 following possible pair(s) to check:
    <{  K K(K(ola)), KMUM( ), KId ,  KIdola, KKKIdfred}, {ø}>
    <{ MK'UK'( ),  MK' K'(ala), MK'KUK(a),  MIdala, MId ,
       MK'Ida, MK Id , MK'Idada}, {ø}>
    <{ MK'UK'( ),  MK' K'(ala), MK'MUM(ada),  MIdala, MId ,
       MK'Ida, MK Id , MK'Idada}, {ø}>
Let us consider the following pair:
    <{  K K(K(ola)), KMUM( ), KId ,  KIdola, KKKIdfred}, {ø}>
The formula tree after using IPAL rules:

∨ \overline{∨} \overline{∨} \overline{∨}

\overline{∨} \overline{∨}

        KKIdola
          KKKIdola
             KKKKIdola
             KKKK K(K(ola))
        KMId
          KMMId
          KMMMUM( )
     KId
     KIdola
     KKKIdfred
The number of sequents for the above formula tree:  1
Sequents:
    { KMMMUM( ),  KKKK K(K(ola)), KMMId , KMId ,  KKKKIdola,
      KKKIdola,  KKIdola, KId ,  KIdola, KKKIdfred} Not fund
Let us consider the following pair:
    <{ KMMMUM( ),  KKKK K(K(ola)), KMMId , KMId ,  KKKKIdola,
       KKKIdola,  KKIdola, KId ,  KIdola, KKKIdfred}, {ø}>
Now we obtain 0 following possible pair(s) to check.
Let us check the next one.
Let us consider the following pair:
    <{ MK'UK'( ),  MK' K'(ala), MK'KUK(a),  MIdala, MId ,
       MK'Ida, MK Id , MK'Idada}, {ø}>

The formula tree after using IPAL rules:

∨ \overline{∨}

\overline{∨}

\overline{∨}

  MK'Id
  MK'K'UK'( )
  MK'Idala
  MK'K' K'(ala)
  MK'KIda
  MK'KKUK(a)
MIdala
MId
MK'Ida
MK Id
MK'Idada
The number of sequents for the above formula tree:  1
Sequents:
{ MK'KKUK(a),  MK'K' K'(ala), MK'K'UK'( ), MK'KIda,
 MK'Idala, MK'Id ,  MIdala, MId , MK'Ida, MK Id ,
 MK'Idada} Not fund
Let us consider the following pair:
<{  MK'K' K'(ala), MK'K'UK'( ),  MIdala, MId ,  MK'Idala,
  MK'Id , MK'Ida, MK Id , MK'Idada, MK'KIda}, {ø}>
The formula tree after using IPAL rules:

∨ \overline{∨} \overline{∨}

\overline{∨} \overline{∨}

  MK'K'Idala
     MK'K'K'Idala
     MK'K'K'K' K'(ala)
  MK'K'Id
     MK'K'K'Id
     MK'K'K'K'UK'( )
MIdala
MId
MK'Idala
MK'Id
MK'Ida
MK Id
MK'Idada
MK'KIda

The number of sequents for the above formula tree:  1
Sequents:
    { MK'K'K'K'UK'( ),  MK'K'K'K' K'(ala), MK'K'K'Id ,
      MK'K'Id ,  MK'K'K'Idala, MK'K'Idala,  MIdala, MId ,
      MK'Idala, MK'Id , MK'Ida, MK Id , MK'Idada, MK'KIda}
      Not fund
Let us consider the following pair:
    <{ MK'UK'( ),  MK' K'(ala), MK'MUM(ada),  MIdala, MId ,
       MK'Ida, MK Id , MK'Idada}, {ø}>
The main sequent is not accepted
The formula tree after using IPAL rules:

∨ \overline{∨}

\overline{∨}
\overline{∨}

        MK'Id
        MK'K'UK'( )
        MK'Idala
        MK'K' K'(ala)
        MK'MIdada
        MK'MMUM(ada)
     MIdala
     MId
     MK'Ida
     MK Id
     MK'Idada
The number of sequents for the above formula tree:  1
Sequents:
    { MK'MMUM(ada),  MK'K' K'(ala), MK'K'UK'( ), MK'MIdada,
      MK'Idala, MK'Id ,  MIdala, MId , MK'Ida, MK Id ,
      MK'Idada} Not fund
Let us consider the following pair:
    <{  MK'K' K'(ala), MK'K'UK'( ),  MIdala, MId ,  MK'Idala,
       MK'Id , MK'Ida, MK Id , MK'Idada, MK'MIdada}, {ø}>

The formula tree after using IPAL rules:

∨ \overline{∨} \overline{∨}

\overline{∨} \overline{∨}

  MK'K'Idala
     MK'K'K'Idala
     MK'K'K'K' K'(ala)
  MK'K'Id
     MK'K'K'Id
     MK'K'K'K'UK'( )
MIdala
MId
MK'Idala
MK'Id
MK'Ida
MK Id
MK'Idada
MK'MIdada
The number of sequents for the above formula tree:  1
Sequents:
{ MK'K'K'K'UK'( ),  MK'K'K'K' K'(ala), MK'K'K'Id ,
 MK'K'Id ,  MK'K'K'Idala,  MK'K'Idala,  MIdala, MId ,
 MK'Idala, MK'Id , MK'Ida, MK Id , MK'Idada, MK'MIdada}
 Not fund
Let us consider the following pair:
<{  K K(K(ola)), KMUM( ), MK'UK'( ),  MK' K'(ala),
  MIdala, KId , MId ,  KIdola, MK'Ida, MK'KUK(a),
  MK Id , MK'MUM(ada), MK K K( ), MK'Idada, KKKIdfred,
  K'MKMId }, {ø}>
The main sequent is not accepted
THE INPUT FORMULA IS NOT ACCEPTED
             END OF IPAL DOCUMENTATION