10.6092/issn.1972-5787/4569
The paper is devoted to the study of one of the aspects of the so-called Evidence Algorithm programme advanced by Academician V.M.~Glushkov and connected with the problem of automated theorem-proving search in the signature of first-order theories that can use different logics, such as classical, intuitionistic, and modal ones. An approach to the construction of such sequent logics (with or without equality) is described. It exploits the original notions of admissibility and compatibility, which permits to avoid preliminary skolemization being a forbidden operation for a number of non-classical logics in general. Following the approach, the cut-free sequent (modal) calculi avoiding the dependence of inference search on different orders of quantifier rules applications are described. Results on the coextensivity of sequent calculi are given. The research gives a way to the construction of computer-oriented quantifier-rule-free calculi for classical and intuitionistic logics and their modal extensions. 
application/pdf
1972-5787
4569
1
en
Alexander Lyaletski
Journal of Formalized Reasoning
modal logic
Mathematical Text Processing in EA-style: a Sequent Aspect
Text.Serial.Journal
https://jfr.unibo.it/
9
QED 20th anniversary
2016-01-29
2014-12-15
2016-01-29
2016-12-23
235-264
JFR
Alexander Lyaletski
2016/01/29
10.6092/issn.1972-5787/4569
235
Taras Shevchenko National University of Kyiv
1972-5787
1
modal logic
en
264
Mathematical Text Processing in EA-style: a Sequent Aspect
https://jfr.unibo.it/article/download/4569/5734
9
Mathematical Text Processing in EA-style:
a Sequent Approach
ALEXANDER LYALETSKI
Senior researcher of the Faculty of Cybernetics, Taras Shevchenko National University
of Kyiv, Kyiv, Ukraine


The paper devoted to the logical aspect of mathematical text processing satisfying such principles
of the so-called Evidence Algorithm as that the syntactical form of a task under consideration
should be preserved and proof search should be proceeded in the signature of an initial theory,
that is it should be carried out without performing preliminary skolemization being a forbidden
operation for a number of logics. It contains an approach to construct computer-oriented cut-free
sequent calculi for classical and intuitionistic first-order logics as well as their modal extensions
(without or with equality). The approach exploits the original notions of admissibility and compat-
ibility, which allows avoiding the dependence of proof search in sequent calculi on different orders
of quantifier rule applications. Following it, quantifier-rule-free sequent calculi are constructed.
Results on the coextensivity of these calculi with Kanger-type sequent calculi are given.




        “... the computer can significantly extend human capabilities in the area of
         establishing new mathematical (and not only mathematical) facts. Doing a
         little dreaming, one can talk about the times when fruitful creative work in
         mathematics and other exact sciences will be impossible without the usage
         of computers, and the success of a scientific study will be determined prima-
         rily by the craft of programming a strategy for scientific research...”[1]
                                                                V.M. Glushkov (1957)

1.   INTRODUCTION
In Kyiv, investigations in automated reasoning were initiated by V.M. Glushkov
at the beginning of 1960s, when the first team on formalized mathematical text
processing was gathered. Being a mathematician and algebraist, from the very
outset of his activity in Cybernetics, he first of all was interesting in the problem of
doing mathematics with the help of automated theorem proving in formal theories.
  V.M. Glushkov formulated this problem in a slightly unusual way. Let us consider
a relatively well formalized mathematical theory, e.g. the group theory. There
are a small number of basic facts (axioms) which are considered to be evident
even for beginners. After applying simple purely logical tools, one obtains several
consequences. They are also evident. Then one can apply the same logical tools
to the conclusions and so on. Are the results still evident? If the conclusions were
obtained by a programmed inference engine, the answer is “yes, they are”. From
the viewpoint of this engine. However, probably not from the human point of view.
Thus, provided the above-mentioned engine, one is able to prove/verify something
that is not evident for humans. Further to that, this “evidence-maintaining engine”
may be reinforced with heuristics, proof methods, lemma application, definition


                                       Journal of Formalized Reasoning Vol. 9, No. 1, 2016 Pages 235–264.
236      ·     Alexander Lyaletski

expansion, and so on. In this way, the notion of “being evident” could be enlarged
to the extent that might include nontrivial facts/theorems.
   This approach to automated theorem proving found its reflection in the so-called
Evidence Algorithm programme, EA, announced by V.M. Glushkov in [2], where
he wrote:
   “. . . a good (and maybe, the best) problem of the simulation [of human activ-
ity] might be the problem of automated theorem proving in mathematics. The
center of the study in this field should be displaced from constructing “universal”
theorem-proving programs towards creating programming and operating systems
that (if necessary) allow rapid programming of proof search even for a unique dif-
ficult theorem and that, in the case of necessity, are capable to interact with a
mathematician for proving this theorem in real time.”
   This Glushkov’s point of view on automated theorem proving has lead to making
simultaneous investigations on formalized mathematical texts processing, includ-
ing the creation of formalized languages for their presentation in the form most
appropriate for a user, formalization and evolutional (evidential) development of a
computer-made proof step, construction of an EA information environment having
an influence on a current evidence of a computer-made proof step, and interactive
man-assistant search of a proof. So, we see that Glushkov’s approach shares certain
ideas and has some common features with the QED manifesto [3] as well as with
Mizar [4] and Calculemus [5] projects.

2.    EA APPROACH TO MATHEMATICAL TEXT PROCESSING
A lot of investigations in automated theorem proving have being made since the
appearance of the Evidence Algorithm, EA, the modern vision of which was called
the evidential paradigm in [6]. As a result, there were constructed the Russian-
language [7] (1978) and English-language [8] (2002) SAD systems1 reflecting the
EA requirements to formalized mathematical text processing. Both the systems
have similar structures and are based on the above-given general EA principles.
(At that, accordingly to EA, the main efforts of the EA developers were primarily
directed towards the development, investigation, and implementation of linguistic
tools and logical methods of proof search in first-order logics.)
   The Russian and English SAD systems operate according to the following chains
of formalized mathematical text transformations (a more detailed description of the
Russian and English SADs can be found in [9]):
     Text prepared by a user for proving/verifying a theorem ===========>
                                                              (using a parser)
     ===========> A first-order self-contained text ============>
                                                             (using a prover)
     =========> A computer–made proof/verification ===========>
                                                             (using an editor)
     =======> Text in a form comprehensible for a human
  For writing formalized (mathematical) texts, the Russian- and English-language
versions of a formal language were constructed. The Russian version [10] was called

1 Draw  you attention to the fact that the Russian SAD had no name for a long time and all the
references to it were made as to the system for mathematical texts processing.

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
             Mathematical Text Processing in EA-style: a Sequent Approach          ·     237

Theory Language (TL), while the English version [11] — Formal Theory Language
(ForTheL). Their syntactical analyzers were designed and implemented in such a
way that their outputs are themselves computer internal presentations of the first-
order language.
   Note that TL and ForTheL reflect Glushkov’s desire to have practical formal
languages suitable for writing mathematical propositions and their proofs. At that,
they “should relate to the existing formal languages of mathematical logic as, for
example, ALGOL-60 language relates to the language of recursive functions or
normal algorithms”[2].
   Here we conclude the consideration of TL and ForTheL noting that there are
many enough publications on these languages (the most part of such references can
be found in [9]), in particular, ForTheL has its complete description in the “ForTheL
Reference” located on the site “nevidal.org”. In this connection, in what follows
the attention is focused on logical investigations prolonging the research made in
the framework of two SAD systems and oriented to the further development and
improvement of methods for inference search in the EA-style.
   The main EA principles relating to the proof search are: the syntactical form of
a task under consideration should be preserved; logical transformations should be
performed in the signature of an initial theory (i.e. without applying skolemization);
proof search should be goal-oriented; equality handling/equation solving should be
separated from proof searching.
   After considering different known approaches to the construction of automated
theorem-proving methods, one will conclude that the sequent approach is one of the
most suitable for satisfying the just given principles. This is the main reason why
the preference was given to the sequent formalism when constructing the Russian
and English SADs. Namely, its logical (possible) capabilities are studied in the paper
from the point of view of the construction of efficient enough deductive systems for
computer proof search in different first-order logics.
   Here it is important to note that the logical investigations being made for the
Russian SAD, also include the investigations on resolution-type methods and in-
terpretation of Maslov’s Inverse Method. Their description has already been given
in [12] in a complete enough form. This is one of the reasons why there is nothing
about them in what follows.
   Another reason is that the original prover of the English SAD is based on the
sequent formalism only , which is caused by that the following decision was accepted
when designing the English SAD: in the case of the necessity or desire to use a
resolution technique, a SAD user can apply one of such well-known provers as
SPASS, Vampire, E Prover, Prover9, and Otter. As a result, efforts of the paper’s
author as one of the SAD developers were and are directed mainly to studying the
sequent formalism.

3.   EA-STYLE DEDUCTION AND SEQUENT CALCULI
From the very beginning of its appearance, the EA program has paid great at-
tention to developing machine proof search methods suitable for the various fields
of mathematics and reflecting (informal) human reasoning techniques. The first
attempt in this direction was made in 1963, when V. M. Glushkov formulated the
problem of automated theorem proving in the group theory. In this connection,
                                         Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
238     ·      Alexander Lyaletski

texts from the books on the group theory were exposed to the careful analysis. As
a result, a machine procedure for proof search in the group theory was constructed
in the middle of the 1960s [13].
   Later, that procedure was generalized to the case of first-order restricted classical
predicate calculus without equality [14, 15]. The procedure admitted its interpre-
tation as a specific, sound and complete, sequent calculus later called the AGS
(Auxiliary Goals Search) calculus [16]. The primary AGS satisfied the EA princi-
ples (2) and (3), where:
   – for avoiding skolemization, a specific quantifiers handling technique was devel-
oped; it was actually a modification of Kanger’s idea [17] about using of so-called
“dummies” and “parameters” in quantifier rules as special variables with subse-
quent replacing “dummies” by “admissible” terms at certain instants of time and
   – goal-orientation, which means that at each instant of time the succedent of any
sequent under consideration should have no more than one formula-goal.
   Further development of the ASG calculus was oriented to its improvement in
the direction of optimizing quantifier handling, separating equality processing from
deduction, and goal-driven proof searching.
   The optimization of quantifier handling was achieved by the introduction of an
original notion of an admissible substitution distinguished from Kanger’s one.
   The equality separation was oriented to the development of special methods for
equality processing and equation solving. (Later algebra systems and problem
solvers were suggested to use for this purpose.)
   The goal-driven search was based on driving the process of an auxiliary goal
generation by taking a formula (goal) under consideration into account.
   All these investigations led to the construction of an original sequent calculus
(with the new notion of admissibility using in this paper) published in [18] in 1981
and implemented in the (Russian) SAD system.
   Additionally note that the Russian SAD contained certain tools for applying
definitions and auxiliary propositions at certain time moments. They reflected the
usual way of using definitions and auxiliary propositions by a mathematician and
demonstrated good results in proving usual mathematical theorems.
   Since then, the investigations on inference search in EA-style were stopped until
1998, when the author took a participation in the Intas project 96-0760 “Rewriting
Techniques and Efficient Theorem Proving”(1998-2000), which led to the further
development of the calculus from [18] in several directions. One of them was ori-
ented to the to development of a special sequent formalism allowing to improve the
positive features of AGS [19]. Another one, which found its reflection in imple-
menting the English SAD, was in studying different ways for the construction of
goal-driven sequent calculi satisfying the AGS-style proof search [20].
   In this connection note that at present, more and more attention is given to elabo-
ration of proof search methods, which are oriented to deducing in non-classical logics
as well as using a man-machine interaction. However, when well-known methods
relying upon the results of Skolem [21] and Herbrand [22] and having a sufficiently
high efficiency (such as resolution-type methods, the inverse method, connection
graph methods, etc.) are tried to use with this purpose, a number of difficulties
arise. These difficulties are caused by the fact that both the specificity of the meth-
ods consisting in the “destruction” of a proposition to be proven by transforming
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
             Mathematical Text Processing in EA-style: a Sequent Approach          ·     239

it into clauses, assembles, connection graphs, an so on and ways of organizing of a
deduction process impede the implementation of tools for the construction of such
a “natural” deduction, which could be achieved by using the standard Gentzen [23]
or Kanger [17] calculi.
   At the same time, usual Gentzen-type sequent calculi significantly yield proof
search efficiency, for example, to resolution-type methods. In general, this is mainly
connected with different possible orders of the quantifier rule applications in them
while resolution-type methods, due to skolemization, are free from this deficiency.
That is why the contemporary state of automated reasoning is characterized by
that great attention is attracted to the construction of a proof-search technique
combining the best features of the first-order sequent formalism and “combinatory”
logical methods (for example, such as sophisticated resolution- and paramodulation-
type strategies). These words are confirmed by the great number of appropriate
publications. (We refer to [24] containing such papers as [25, 26, 27, 28] and so on.)
   When quantifier rules are applied in sequent calculi, a substitution of selected
terms for variables is made. In order for this step of deduction to be sound, certain
restrictions are put on a substitution. A substitution satisfying these restrictions
is said to be admissible. Usual Gentzen (classical and intuitionistic) calculi explore
Gentzen’s admissibility requiring that a term substituted for the variable of a quan-
tifier cannot contain bound variables, which proves to be sufficient for the needs of
the proof theory. But it becomes useless from the point of view of the efficiency
of computer-oriented inference search, since it produces extreme large step-by-step
examinations of different orders of quantifier rules applications in attempting to
find at least one order leading to success.
   As a result, researchers in logical reasoning face with the following problem:
how can the Gentzen quantifier rules be modified for providing the optimization of
quantifier rules applications in sequent calculi?
   The first serious attempt in this direction, seemingly, belongs to S. Kanger [17]
who suggested his sequent calculus, in which a “pattern” of an inference tree is
first constructed with the help of propositional rules and specific quantifier rules
eliminating quantifiers and inserting only special variables, the so-called parameters
and dummies. In order for the inference process to complete successfully, at some
instants of time an attempt is made to convert a “pattern” into a proof tree by
means of replacing each dummy in the “pattern” by a term from a list connected
with the dummy. In the case of lack of success, the process is continued. But
Kanger’s approach still preserves the dependence of proof search efficiency on step-
by-step attempts to find an order of quantifier rule applications leading to the
construction of a proof tree. (Note that Kanger’s approach proposed for classical
logic was later incorporated into intuitionistic logic [29].)
   At the end of the 1990s, there appeared two publications [30] and [31] containing
the more sophisticated techniques for inference search in classical and non-classical
first-order logics. They are based on the analysis of the general logical structure
of formulas being investigated on deducibility and has led to the appearance of a
number of deduction methods such as matrix characterization method [31], different
modifications of the connection method [30] (see, for example, [32, 33, 34]), and
original sequent and tableau methods (see, for example, [35, 36]).
   The author’s approach presented in this paper is based on [37]. It shares, in a
                                         Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
240     ·      Alexander Lyaletski

certain sense, some ideas with [30] and [31] taking into account only the general
logical structure of a given formula (or sequent), while, according to the author’s
approach, the quantifier structure is extracted as the most important component of
the logical structure for its subsequent “analysis” with the help of the new notion
of an admissible substitution. It permits to optimize the step-by-step examination
of all possible orders of quantifier rule applications and leads to the construction of
efficient enough methods for proof search in classical logic using only the quantifier
structure of a given formula (or sequent) (see, for example, [19]). At that, it turned
out that the (new) notion of admissibility is not enough for the construction of
sound calculi in the intuitionistic case. This situation can be corrected by using
the notion of compatibility proposed in [38] for the construction of the sound (and
complete) intuitionistic tableau calculus with free variables (some historical details
can be found in [12]).
   This paper in a certain sense summarizes the previous author’s results concerning
machine proof search in classical and non-classical sequent first-order logics with
the subformula and cut elimination properties. It clarifies some unclear places
in the previous publications and further develops the author’s approach to the
construction of computer-oriented sequent calculi for proof search in the EA-style.

4.    MAIN NOTIONS AND DENOTATIONS
Our research concerns the sequent form of classical and intuitionistic (modal) logics
without the cut and, possibly, with equality. At that, our way of the constriction
of modal calculi has a certain correlation with the papers [31, 39].
   The first-order sequent terminology is used. The basic logical signature Sig0
of our first-order language contains logical connectives: the universal quantifier
symbols ∀ and existential quantifier symbols ∃ as well as the propositional symbols
for the implication (⊃), disjunction (∨), conjunction (∧), and negation (¬); at
that, the quantifiers ∀x and ∃x are often considered as a single whole.
   Besides, there are a set of functional symbols necessarily containing a special
constant, say, c0 , and a non-empty set of predicate symbols, containing, perhaps,
the equality (≈).
   As a rule, the arity of any modal operator (for example, 2 and 3) is equal to 1.
However, we consider a more general setting supposing that a finite set M odm =
{ 1 , . . . , m } of modal operators of any finite positive arities is given (the well-
known modal operators 2 and 3 may be among them).
   For a given M odm , the signature Sig0 ∪ M odm is denoted by Sigm . M od0 = ∅
by definition.
   Extend the signature Sigm (including the case of Sig0 when m = 0) in the
following way: for any natural numbers i and n (i, n ≥ 1) and for any symbol
   from Sigm , we add the new symbols i , n , and in to Sigm and denote this
extension of Sigm by e Sig m (e Sig m = e Sig 0 ∪ e M odm ); at that, i is called a left
upper index and n a left down index of .
   Any symbol from e Sig m is called a connective. If we want to specify that
    ∈ e M odm ( ∈ e Sig 0 ), we simply say that         is a modal (logical) connec-
tive. Besides, the symbol       (possibly, with upper and down indexes and right
subscripts) is reserved for denoting any propositional logical symbol, quantifier, or
modal operator.
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
               Mathematical Text Processing in EA-style: a Sequent Approach             ·     241

   For example, 1 ∨, 57 ∀, and 3 2, may be symbols of the extended signature e Sig m ;
at that, 1 ∨, 57 ∀ ∈ e Sig 0 while 3 2 ∈ e M odm . (Note that left upper indexes will be
used for producing so-called copies of the same expression (see below).)
   A countable set of variables used in logics under consideration is denoted by V ar.
At that, we consider that V ar consists of two disjoint countable sets: V ar0 and
e
  V ar0 (V ar = V ar0 ∪ e V ar0 ), where the following condition is satisfied: V ar0 is
a set of usual variables and for any v ∈ V ar0 and any i and n (i, n ≥ 1), e V ar0
contains the variables i v, n v, and in v.
   The notions of a term, atomic formula, literal, formula, subformula, and proper
subformula over Sig0 ∪ V ar0 and e Sig0 ∪ V ar are used in the usual sense with
the only exception: the expressions in ∀ jk x and in ∃ jk x are allowed to use for denoting
quantifiers only in the case when upper indexes and down indexes coincide if these
indexes are present (that is when i = j and n = k).
   For the case of the signature e Sigm , the notion of a formula is extended as follows:
   (I) Each formula over e Sig0 ∪ V ar is considered to be a formula over Sigm ∪ V ar.
   (II) If F1 , . . . , Fr are formulas over e Sigm ∪ V ar and         of the arity r belongs to
e
  M odm , then (F1 , . . . , Fr ) is a formula over e Sigm ∪ V ar.
   (III) If F1 and F2 are formulas over e Sigm ∪V ar, ∈ e Sigm is a logical connective
with arity 2 (i.e. ⊃, ∨, or ∧, maybe, with left upper and down indexes), and 0
is a logical connective with arity 1 (i.e. ∃x, ∀x, or ¬, maybe, with left upper and
down indexes), then F1 F2 and 0 F1 is a formula over e Sigm .
   Let a formula F over e Sigm ∪ V ar be of the form (F1 , . . . , Fr ), F1 , or F1 F2 ,
where       is a modal operator or a logical symbol. Then                  is called a principal
symbol (connective) of F and F1 , F2 , . . . , Fr are called principal subformulas of the
formula F , which sometimes will be called a -formula.
   The notions of free and bound variables of a formula and its variant (over both
e
  Sig0 ∪ V ar and e Sigm ∪ V ar) are usual.
   Sequents are defined in the usual manner, i.e. as an expression of the form F1 , . . . ,
Fp → G1 , . . . , Gq , where F1 , . . . , Fp , G1 , . . . , Gq are formulas over e Sigm ∪ V ar
except that the succedent and antecedent of a sequent are considered as finite
multisets (see, for example, [39] and [42]).
   A tree is understood in the usual sense. A tree with nodes labeled by sequents
is called a sequent tree.
   Any syntactical object over Sigm ∪ V ar0 (including variables, terms, formulas,
sequents, and so on) is called an original expression.
   As usual, the following convention holds w.r.t. bound variables: two different
quantifiers in any formula or sequent over e Sigm ∪ V ar cannot have common vari-
able; moreover, any formula or sequent cannot simultaneously contain any variable
being both bound and free. (It is known that these conditions can be achieved by
means of renaming bound variables, which does not effect on deducibility).
   A formula without free variables is called closed.
   For solving the problem of deducibility in a usual sequent calculus, we can restrict
us, without loss of generality, by establishing the deducubility of only an initial
sequent of the form → F , where F is a closed original formula.
   In what follows, the original formula F ∗ = ∃y¬2∃xP (x, f (y))⊃¬∀y 0 2∃x0 P (x0 , y 0 )
(P is a predicate symbol and f a functional symbol) deducible in GK [39] will be
used in a number of examples clarifying the notions introduced and results obtained.
                                              Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
242     ·      Alexander Lyaletski

   Any expression over e Sigm ∪ V ar, all connectives and variables of which contain
left upper indexes, is called (upper) indexed.
   Note that according to this definition, predicate and functional symbols cannot
be indexed.
   The result of any upper indexing of an expression without upper indexes (i.e.
adding left upper indexes to all connectives and variables of the expression) is
called its copy. Two copies of the same expression (including the case of a variable
or connective) are considered to be copies of each other by definition. That is the
relation “to be a copy” is transitive.
   The extension of all the necessary semantic notions to formulas and sequents
containing upper and down left indexes is obvious: it is enough to omit all their
indexes and use the usual semantic notions.
   Remark. In the case of M od0 (= ∅), all the original formulas and sequents are
those syntactical units that are used when determining the standard classical and
intuitionistic calculi. The case of M od1 = {2} leads to different modal sequent
calculi depending on what sequent rules for 2 are determined; for example, there
exists the possibility to determine GK or GS4 from [39].
   A substitution is a finite mapping from variables to terms presented in the form
{x1 7→ t1 , . . . , xn 7→ tn }, where x1 , . . . , xn are pairwise distinct variables and each
term ti is not xi for any i = 1, . . . , n; at that, each xi 7→ ti is called a substitution
component, ti a term, and xi a variable of σ (i = 1, . . . , n) (cf. [40]).
   A renaming is a substitution not containing terms distinguished from variables
and replacing different variables by different ones.
   For a substitution σ and quantifier-free expression Ex (including the cases of a
formula and sequent), the result of the application of σ to Ex is understood in the
usual sense; it is denoted by Ex · σ.
   If σ and λ are substitutions, then σ · λ denotes their composition, i.e. a substi-
tution, the result of the application of which to Ex is equal to (Ex · σ) · λ.
   The notions of a unif ier, simultaneous unifier, and the most general simultaneous
unifier of a set of expressions are understood in the usual sense [40].
   For formulas F and G, we understand the notions of positive (GbF + c) and neg-
ative (GbF − c) occurrences of F in G in the sense of the paper [41].
   More precisely, let a formula F have one or more occurrences in a formula G. Let
us fix a certain occurrence of F in G. This occurrence is called positive (negative)
in the accordance with the following:
   ◦ GbF + c, if F coincides with G;
   ◦ GbF + c (G1 bF − c), if G is of the form: G1 ∧ G2 , G2 ∧ G1 , G1 ∨ G2 , G2 ∨ G1 ,
     G2 ⊃ G1 , ∀xG1 , or ∃xG1 and G1 bF + c (G1 bF − c);
   ◦ GbF − c (GbF + c), if G is of the form: G1 ⊃ G2 or ¬G1 and G1 bF + c (G1 bF − c);
   ◦ GbF + c (GbF − c), if G is of the form (G1 , . . . , Gr ) and Gi bF + c (Gi bF − c)
      (1 ≤ i ≤ r), where         is a modal operator.
   Moreover (cf. [41]), a selected occurrence of a formula in a sequent Γ → ∆ is
called a positive (negative) one if, and only if, this occurrence is a positive one in
a formula from ∆ (from Γ) or a negative one in a formula from Γ (from ∆).
   If a formula F is of the form ∀xF 0 (∃xF 0 ) and F has a positive (negative) oc-
currence in a formula G or a sequent S, then ∀x (∃x) is called a positive quantifier
in G or S respectively; ∃x (∀x) is called a negative quantifier in G or S, if ∃xF 0
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
              Mathematical Text Processing in EA-style: a Sequent Approach            ·     243

(∀xF 0 ) has a positive (negative) occurrence in G or S respectively.
   As the convention about bound variables is satisfied, any quantifier cannot have
more then one (positive or negative) occurrence in a formula or sequent under con-
sideration. So the following definitions (cf. [17]) do not lead to misunderstanding.
   Following [17], the variable of a positive quantifier occurring in a formula G or
sequent S is called a parameter in G or S respectively; the variable of a negative
quantifier occurring in G or S is called a dummy in G or S respectively.
   Note that we preserve the name “variable” for denoting both dummies and pa-
rameters in the cases, when it is only important that they occur in a formula or
sequent under consideration.
   For F ∗ , we have: x and y 0 are its dummies and x0 and y are its parameters.
   Since the properties “to be a dummy” and “to be a parameter” are invariant
for any variable x w.r.t. any rules applications in our sequent calculi, it turns out
convenient to write x in order to indicate that x is a parameter and to write x in
order to indicate that x is a dummy in a formula or sequent under consideration.
This convention will be used often by default in what follows.
   For a formula F (sequent S), µ(F ) (µ(S)) denotes the result of the removing of
all the quantifiers from F (from S).
   The operation µ has the following obvious properties w.r.t. logical and modal
connectives (below F1 , . . ., Fr are formulas, x a variable,     a modal operator):
   µ(¬F1 ) = ¬µ(F1 ), µ(F1 ∧ F2 ) = µ(F1 ) ∧ µ(F2 ), µ(F1 ∨ F2 ) = µ(F1 ) ∨ µ(F2 ),
µ(∀xF1 ) = µ(F1 ), µ(∃xF1 ) = µ(F1 ), and µ( (F1 , . . . , Fr )) = (µ(F1 ), . . . , µ(Fr )).
   If F (S) is a formula (sequent) and x its parameter or dummy, then x is considered
as a parameter or dummy in µ(F ) (in µ(S)).
   Extend the operation of the application of a substitution σ to a quantifier-free
expression on the case of the application of σ to any formula F in the following
way (denoting the result by F · σ): produce µ(F ) (by omitting all quantifiers in F ),
construct µ(F ) · σ, and restore all the omitted qualifiers at their initial places.
   For example, for F ∗ and σ = {x 7→ g(x, y), y 0 7→ c}, we have that F ∗ · σ =
∃y¬2∃xP (g(x, y), f (y)) ⊃ ¬∀y 0 2∃x0 P (x0 , c).
   The extension of the operation “·” on sequents and sequent trees is obvious. Note
that the result of its application to a sequent or sequent tree produces a sequent or
sequent tree respectively.
   We use the usual definition of a sequent calculus while the deduction of a sequent
in it has the form of an inference tree growing “from top to bottom” according to
(counter-)applications of inference rules “from top to bottom”. An inference tree is
called a proof tree, if all its leaves are labeled by axioms. A sequent S is deducible
in a calculus, if there exist a proof tree for S in the calculus.
   Note that our sequent calculi do not contain the cut rule as the cut is supposed
to be eliminable. Becides, all their rules satisfies the usual subformula property (see,
for example, [23] or [42]).

5.   KANGER-TYPE CALCULI WITH USUAL QUANTIFIER RULES
All our first-order sequent calculi are based on certain modifications of Gentzen’s
calculi LK and LJ without equality from [23]; at that, LK≈ and LJ≈ will denote
LK and LJ containing the equality rules in Kanger’s form from [17]. The con-
sideration of the succedents and antecedents of sequents as multisets allows us to
                                            Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
244      ·       Alexander Lyaletski

convert the calculi LK and LJ into KK and KJ by removing the weakening and
exchange rules from them. After adding the equality rules in the form from [17] to
KK and KJ, we get the calculi KK≈ and KJ≈ .
   Note that in these notations, Kanger’s calculus from [17] can be considered as
coinciding with KK≈ , provided that in all the rules, the left upper indexes and
subscribes are absent. This calculus is denoted by K≈ ; K≈ without the equality
rules is denoted by K.
   All the just described calculi are presented in Fig. 1. They form a calculi family
denoted by KC containing all the rules and axioms from Fig. 1 except (Con∗ →),
(→ Con∗ ), (∃∗ →), and (→ ∃∗ ). Different its modifications lead to the family, the
most general representative of which is denoted by KK≈ . That is why we attempt
to obtain certain results for KC and then modify them in a certain way.
   For introducing the modal logics, we follow the paper [39], where necessary modal
rules are simply added to Gentsen’s calculi LK and LJ. Doing the same for a set
Modm consisting of m modal rules, we define a family KK+Modm containing
the following classes of modal logics: KK+Modm , KJ+Modm , KK≈ +Modm ,
and KJ≈ +Modm . The same concerns the modal extensions of K and K≈ .
   As to modal rules, we consider that any modal rule (Ml ) from Modm (1 ≤ l ≤ m)
is of the form:
       i                          ikl,k                    jl,1                         jl,k0
                                                                   0                           0
   Γ, nl,1
         l,1 l,1 (Φl,1 ), . . . , nl,kl
                                        l
                                           l,kl (Φl,kl ) → rl,1    l,1 (Ψl,1 ), . . . , rl,kl0
                                                                                            l
                                                                                               l,kl0 (Ψl,kl ), ∆
                                                                                                          0

                                                                                                                 ,
                                 Γ, Φl,1 , . . . , Φl,kl → Ψl,1 , . . . , Ψl,kl0 , ∆
where Φl,1 , . . . , Φl,kl and Ψl,1 , . . . , Ψl,kl0 are multisets of formulas.
   Let us introduce so-called numbered formulas having a great importance for our
considerations and being used in the description of the calculi from Fig. 1.
   Let F be an original formula (i.e. a formula over over Sigm ∪V ar0 ) being different
from an atomic formula. By (n, F ) denote the occurrence of the nth subformula of
F when reading the formula F from left to right (n does not exceed the number of
connectives occurring in F ).
   If (n, F ) is an occurrence of a -formula in a formula F , then the connective
    is said to be the n -connective in F ; at that, the -formula is called a n -
subf ormula of F , where n is explicitly indicated as a left down index of n . In the
case if is ∀x or ∃x, n is n ∀n x or n ∃n x respectively and all the other occurrences
of x in F receive n as their left down index.
   This operation of the left down indexing of all connectives and variables in an
original formula F is called the numbering operation and the result of its applica-
tion to F is called a numbered formula and denoted by ν F .
   For the formula F ∗ , we have the following result ν F ∗ of numbering its connectives
and variables: 1 ∃1 y 2 ¬ 3 2 4 ∃4 x P (4 x, f (1 y)) 5 ⊃ 6 ¬ 7 ∀7 y 0 8 2 9 ∃9 x0 P (9 x0 ,7 y 0 ) (pay
your attention that P and f have no indexes).
   Note that due to the numbering of the connectives in an original formula F ,
all these connectives become graphically pairwise different ones. At that, we con-
sider that the logical interpretation of the numbered formula F coincides with the
interpretation of F without left (upper and down) indexes.
   Let F be an original formula. If ν F contains m - and n 0 -subformulas (m 6= n)
and the m -subformula is a subformula of the n 0 -subformula, then n 0 and m
are said to be in the relation lF and this fact is denoted by n 0 lF m .

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                    Mathematical Text Processing in EA-style: a Sequent Approach                                                 ·    245



                                                            P ropositional rules :
                     Γ, A in ∧ B → ∆                                    Γ → A in ∧ B, ∆
                                                (∧ →)                            l+1 [Γ]
                                                                                                                     (→ ∧)
                         Γ, A, B → ∆                           Γ → A, ∆                    → l+1 [B], l+1 [∆]

                                                       Γ, A in ∨ B → ∆
                                                           l+1 [Γ], l+1 [B]
                                                                                               (∨ →)
                                        Γ, A → ∆                                → l+1 [∆]

                                  Γ → A in ∨ B, ∆                               Γ → A in ∨ B, ∆
                                                             (→ ∨1 )                                   (→ ∨2 )
                                       Γ → A, ∆                                    Γ → B, ∆
                                   Γ, A in ⊃ B → ∆                                                 Γ → A in ⊃ B, ∆
                                                                                   (⊃→)                                     (→⊃)
              Γ, A in ⊃ B → A, ∆              l+1 [Γ], l+1 [B]     → l+1 [∆]                         Γ, A → B, ∆

                                        Γ,   i ¬A    →∆                         Γ → in ¬A, ∆
                                             n
                                                               (¬ →)                                (→ ¬)
                                           Γ → A, ∆                              Γ, A → ∆
                                                   Contraction rules :
                                   Γ, A → ∆                      Γ → A, ∆
                                                  (Con →)                       (→ Con)
                                Γ, l+1 [A], A → ∆             Γ → A, l+1 [A], ∆

                            Γ, A → ∆                                                   Γ → A, ∆
                     i
                                                       (Con# →)                            i
                                                                                                                    (→ Con# )
                  Γ, n x<(l+1) [A], A → ∆                                       Γ → A, n x<(l+1) [A], ∆
                                                              Quantif ier rules :
            Γ → in ∀in xA, ∆                               Γ, in ∀in xA → ∆                          Γ, in ∀in xA → ∆
                      i x
                                          (→ ∀)                     i x
                                                                            (∀ →)                           i
                                                                                                                                  (∀# →)
                                                                                                                x
     Γ → l+1 [A]|     n
                      (l+1)+i x    ,∆                       Γ, A|n  ti → ∆                     Γ, l+1 [A]|n
                                                                                                          (l+1)+i          →∆
                            n                                                                                         nx

            Γ, in ∃in xA   →∆                           Γ → in ∃in xA, ∆                            Γ → in ∃in xA, ∆
                    i x
                                          (∃ →)                   i x
                                                                                 (→ ∃)                       i x
                                                                                                                                  (→ ∃# )
     Γ,   l+1       n
              [A]|(l+1)+ i       →∆                      Γ → A|n                                   → l+1 [A]|n
                                                                  ti , ∆                       Γ                (l+1)+i x   ,∆
                            nx                                                                                        n

                                                              Equality rules :
                            Γ, t0 ≈ t00 → ∆                                 Γ, t00 ≈ t0 → ∆
                            0                          0    (≈1 →)          0                   0  (≈2 →)
                         Γ|tt00 , t0 ≈ t00 → ∆|tt00                     Γ|tt00 , t00 ≈ t0 → ∆|tt00

                                                               Axioms :
                                                    Γ, A → A, ∆     Γ → t ≈ t, ∆


KC contains all the rules except (∀# →), (→ ∃# ), (Con# →), and (→ Con# ). BC contains all
the rules except (∀ →), (→ ∃), (Con# →), and (→ Con# ). QC contains all the rules except all
the quantifier rules. In (Ax), A is an atomic formula. The number l denotes the largest left upper
index in a just-constructed inference tree. In (→ ∀) and (∃ →), (l+1)+in x is a (new) parameter,
that is the eigenvariable condition is satisfies for it. In (∀# →) and (→ ∃# ), (l+1)+in x is a (new)
dummy. The terms t, t0 , and t00 do not contain dummies; moreover, besides parameters and c0 ,
all these terms may contain constants and functional symbols occurring in only an initial sequent.
    0          0
Γ|tt00 and ∆|tt00 are the results of the replacement of all the occurrences of t0 by t00 . The same
                     i                          i                       i
holds for   l+1 [A]|n x            ,   l+1 [A]|n x            , and A|n
                                                                            x                                              i x
                     (l+1)+i x                  (l+1)+i x             ti , where the term ti is free for                   n     in A. The
                           n                          n
case of classical (modal) logics takes place, if there is no restrictions for sequents. The case of
intuitionistic (modal) logics takes place, if the succedent of any sequent in any inference rule
contains no more than one formula; at that, in (→ Con) the sequent lying under the line is of the
form Γ → l+1 [A] and in (→ Con∗ ) the sequent lying under the line is of the form Γ → x<(l+1) [A].

                                             Fig. 1.       Calculi KC, BC, and QC


                                                                    Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
246     ·      Alexander Lyaletski

   We also write n 0 lF m x (n y lF m ), when m (n 0 ) is m ∀m x or m ∃m x (n ∀n y
or n ∃n y). In the case when m and n 0 simultaneously are quantifiers of one of
the just given forms, we simply write n y ≺F m x determining the relation ≺F and
underlining the fact that lF is restricted to the case of quantifier variables.
                                                              0
   Further, by definition, n 0 lF m implies that in             lF jm and n y ≺F m x
implies in y ≺F jm x for any i and j.
   For the formula F ∗ numbered above, we have for example: 5 ⊃ is the least element
of lF ∗ and, for example, 1 y ≺F ∗ 4 x, 2 ¬ lF ∗ 4 x, 6 ¬ lF ∗ 8 2; the variables x and
x0 are not comparable, the same concerns 4 x and 6 ¬ as well as 3 2 and 8 2.
   Obviously, for any numbered original formula F , the relations ≺F and lF are
irreflexive, asymmetric, and transitive, that is they are strict orders over the sets
e
  V ar and e Sigm respectively.
   It is also evident that these orders fully determined by an initial closed formula
F remain unchanged during the deduction process in any our calculi. That is why
there will not be any contradiction and misunderstanding in using such denotations
as ≺S and lS for an (indexed) sequent S, ≺Ξ and lΞ for a set Ξ of (indexed)
formulas, and ≺T r and lT r for an (indexed) sequent tree T r.
   If G distinguished from an atomic formula is a -copy of a proper subformula of
a (numbered) initial formula F , then both          and any connective 0 from G such
             0
as lF          (if it exists) are called in-connectives (inner connectives) for G w.r.t.
F . If at that time ( 0 ) are ∀x or ∃x, x is called an in-variable (inner variable)
for G w.r.t. F .
   By definition, any atomic formula is considered as not containing inner connec-
tives and variables, while all the connectives and variables of any original (closed)
formula F are considered to be only inner for F w.r.t. F .
   If G is a subformula of a numbered original formula F , then both any connective
and any variable not being inner for G w.r.t. F are called, respectively, an ex-
connective (external connective) and ex-variable (external variable) for G w.r.t. F .
   This definition implies that any original formula does not contain any external
variables w.r.t. itself.
   Let G be a formula received from a copy of a subformula G0 of an original formula
F by removing some or all quantifiers. If k is a natural number, then the formula
k
F [G] is constructed in the following way (k ≥ 1): for any in-connective (in-variable)
for G w.r.t. F , i is replaced by k+i in G provided that i is the left upper index of this
in-connective (in-variable); if there is no index in this in-connective (in-variable), k
becomes its left upper index in kF [G].
   When F is known or there is no matter what F denotes, we simply write k [G].
(This denotation is used in Fig. 1.)
   If Γ is a multiset of copies of subformulas of a formula F , then kF [Γ] = {kF [H] :
H ∈ Γ}. For a sequent S of the form Γ → ∆, kF [S] denotes the sequent kF [Γ] →
k
F [∆], where Γ and ∆ are multisets of copies of subformulas of a formula F .
   Note that the operation kF [·] transforms any graphically different connectives
and variables into graphically different ones renaming parameters into only (new)
parameters and dummies into only (new) dummies.
   All our sequent calculi are intended for the establishing of the deducibility of
an initial sequent of the form → F (F is a closed initial formula) in a standard
sequent calculus containing usual propositional, modal, and quantifier rules, to
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
              Mathematical Text Processing in EA-style: a Sequent Approach           ·     247

which the equality rules from [17] can be added, if necessary. To do this, we always
make attempt to construct a proof tree for a sequent of the form → 1 [ν F ] called a
starting sequent in our sequent calculi ν F is a numbered formula).
   Remark about numbered formulas. Let → F be an initial sequent and ν F is a
numbered original formula, containing a n -formula. Then the inference rules from
Fig. 1 show that the number n always is an invariant w.r.t. any syntactical and
logical transformations that can be performed in any calculus under consideration.
This means that n is a left down index of only a copy of the symbol n appeared
in making deduction from → 1 [ν F ] in a given calculus.
   As the calculi under consideration possess the subformula property, this will lead
to producing instants of subformulas of 1 [ν F ], their variants, and/or copies only.
   The establishing of the deducibility of any starting sequent in KC+Modm always
is made in the Kanger style, which weans the following.
   In the first step, only quantifier rules are applied in any order as many times
as possible. In the second step, we apply propositional, contraction, and/or modal
rules in any order as long as there is no possibility for applying a quantifier rule
or stopping such applications for going to the third stage. In the third step, in the
case of necessity or on the basis of some reason, we are applying only equality rules
trying to construct a proof tree; if such attempts are unsuccessful, we omit this
step and return to the first step.
   An inference tree being the result of performing first two first steps of proof search
is called an equality-independent inference tree. The one being the result of per-
forming three steps is called an equality-dependent inference tree. Correspondingly,
two first steps of the construction of an inference trees is called equality-independent
stage and the third step is called an equality-dependent one.
   Additionally note that KC+Modm was defined in such a way that the following
important property takes place: any two nodes of any inference tree in a calculus un-
der consideration, not lying in the same branch, have no common bound variables.
This property will often be used implicitly.
   Comparing KK≈ with K≈ , we obtain the following result.
  Proposition 1. An initial usual sequent → F is deducible in K≈ (K) if, and
only if, the starting sequent → 1 [ν F ] is deducible in KK≈ (KK).
   Proof. If T r is a proof tree for → 1 [ν F ] in KK≈ (KK), then after removing all
the left upper and down indexes in it, the tree T r will be transformed into a proof
tree T r0 for → F in K≈ (K).
   In the opposite direction. Let T r0 be a proof tree for → F in K≈ (K). Then
we can replace → F by → 1 [ν F ] at the root of T r0 and, after this, each applica-
tion of inference rule of K≈ (K) in T r0 can be replaced by the application of the
corresponding inference rule of KK≈ (KK) when looking through T r0 from top to
bottom and left to right, finally producing a tree T r. Obviously, T r is a proof tree
for → 1 [ν F ] in KK≈ (KK).
  Remark. Proposition 1 gives the possibility to obtain the results about the
soundness and completeness of KK≈ and KK. Therefore, the same results can
take place for KK≈ +Modm and KK+Modm in the case the soundness and com-
pleteness of the calculi K≈ +Modm and K+Modm .

                                           Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
248     ·      Alexander Lyaletski

6.    ADMISSIBILITY AND COMPATIBILITY
When trying to implement any of the calculi from KC+Modm on computer, one
faces the problem of constructing an efficient technique for looking for an order of
inference rule applications, leading to success, among all possible orders of infer-
ence rule applications. And although for the case of propositional rules there are
good enough methods for solving this problem (in particular, the goal-oriented tech-
nique), in the case of quantifier rules satisfying the Gentzen admissibility, they are
not practically working as the Gentzen admissibility says nothing essential about a
preferable order of quantifier rule applications. Likely, this fact forced researchers
in automated theorem proving to use skolemization for classical logic (cf. [43]) as
the best way for solving the just mentioned problem. Likely, this coursed the ap-
pearance of investigations, in which a technique based on the sophisticated usage
of Skolem functions was developed for logics not allowing the preliminary skolem-
ization (see, e.g., [44] and [45]).
   Beside of skolemization, one can try to use Kanger’s technique for the optimiza-
tion of quantifier rule applications by using so-called “dummies” and “parameters”
and splitting the process of an inference search into Kanger’s stages, which leads
to the Kanger notion of admissibility of a substitution. This notion is more ef-
ficient than Gentzen’s one and can be used in the case of both classical [17] and
intuitionistic [29] logics.
   However, the Kanger admissibility still does not allow to attain the efficiency
comparable with that is observed when the preliminary skolemization is made.
This is observed due to the fact that, as in the case of the Gentzen admissibility,
it is required to select a certain order of the quantifier rule applications and, if it
proves to be unsuccessful, another order of applications should be tried, and so on.
   This was one of the reasons for the paper’s author to make an attempt to elim-
inate this obstacle by means of introducing a new notion of the admissibility of a
substitution that takes into account only the quantifier structure of formulas in an
initial sequent. At last, in the late 1970s, the new notion of admissibility being
described below was proposed by the paper’s author. It first was announced in [37]
where it was used for the construction of an Herbrand theorem without preliminary
skolemization for formulas of classical logic being in prenex form. Later, this result
was generalized on the case of arbitrary formulas of classical logic [46].
   Note that for the case of classical logic and some of its modal extensions, the new
admissibility is sufficient for the soundness of deduction in some calculi [19]. But in
the case of, for example, intuitionistic logic, the usage of only admissibility cannot
guarantee the soundness of the construction of a proof tree [47] because it is still
necessary to take into account the fact that there are certain requirements either
to a form of produced sequents or a method of their processing in inference trees.
(For example, it is often required in the intuitionistic case, that the succedents
of initial and inferred sequents contain no more than one formula.) That is, in
such calculi, admissibility should be correlated in some way with the process of
constructing inference trees. Namely for providing such correlation, the notion of
the compatibility of an inference tree with a substitution is introduced below.
   For any formula F (sequent S, set Ξ of formulas or sequents, sequent tree T r),
each substitution σ induces a (possibly, empty) relation F,σ (S,σ , Ξ,σ , T r,σ )

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
               Mathematical Text Processing in EA-style: a Sequent Approach               ·     249

over the set of variables of F (S, Ξ, T r) as follows: y F,σ x (y S,σ x, y Ξ,σ x,
y T r,σ x) if, and only if, there exists x 7→ t ∈ σ such that x is a dummy in F (S,
Ξ, T r) and t a term containing y being a parameter in F (S, Ξ, T r). Obviously,
F,σ (S,σ , Ξ,σ , T r,σ ) is irreflexive and transitive.
   For example, let us consider the substitution σ ∗ = {x 7→ x0 , y 0 7→ f (y)}, where
x and y 0 are dummies and x0 and y parameters in F ∗ . Then x0 F ∗ ,σ∗ x and
y F ∗ ,σ∗ y 0 .
   In what follows, for a substitution σ and formula F (sequent S, set Ξ of formulas
or sequents, sequent tree T r), F,σ (S,σ , Ξ,σ , T r,σ ) denotes the transitive
closure of ≺F ∪ F,σ (≺S ∪ S,σ , ≺Ξ ∪ Ξ,σ , ≺T r ∪ T r,σ ). Analogously, JF,σ
(JS,σ , JΞ,σ , JT r,σ ) denotes the transitive closure of lF ∪ F,σ (lS ∪ S,σ , lΞ
∪ Ξ,σ , lT r ∪ T r,σ ).
   Obviously, F,σ ⊆ JF,σ (S,σ ⊆ JS,σ , Ξ,σ ⊆ JΞ,σ , T r,σ ⊆ JT r,σ ).
   A substitution σ is called admissible (cf. [29, 31]) for a formula F (sequent S, set
Ξ of formulas or sequents, sequent tree T r) if, and only if, for every x 7→ t ∈ σ, x
is a dummy in F (S, Ξ, T r) and F,σ (S,σ Ξ,σ , T r,σ ) is an irreflexive relation.
   For the above-given formula F ∗ and substitution σ ∗ , we have: F ∗ ,σ∗ = {hy, y 0 i,
hy, x0 i, hy, xi, hy 0 , x0 i, hy 0 , xi, hx0 , xi}. Thus, σ ∗ is admissible substitution for F ∗ .
   If σ 0 = {y 0 7→ x0 }, then x0 σ0 y 0 . Since y 0 ≺ x0 , we have hx0 , x0 i ∈ F ∗ ,σ0 .
Therefore, F ∗ ,σ0 is not irreflexive and σ 0 is not admissible for F ∗ .
   Let SC denote a Gentzen-type sequent calculus based on the usual notion of a
sequent and intended for the establishing of deducibility in a logic under consider-
ation. Suppose T r is an inference tree in SC for a numbered (original or starting)
sequent S and j1 1 , . . ., jr r a sequence of all the connectives being eliminated in
T r when applying inference rules. Let πT r (ji i ) denote an inference rule applica-
tion eliminating ji i . If T r can be constructed according to the order determined
by the sequence πT r (j1 1 ), . . ., πT r (jr r ), then j1 1 , . . ., jr r is called a proper
sequence for T rF w.r.t. SC for S. (Obviously, there may exist a connectives occur-
rences sequence, being not proper for T r.)
   An inference tree T r in SC is called compatible with a substitution σ w.r.t. SC
if, and only if, there exists a proper sequence j1 1 , . . ., jr r for T r such that for
any natural numbers m and n, the inequality m < n implies that the ordered pair
hjn n , jm m i does not belong to JT r,σ ; at that, j1 1 , . . ., jr r is called a sequence
providing the compatibility of T r with σ in SC.
   The following proposition demonstrates the connection of admissibility with com-
patibility.
  Lemma 1. Let T r be an inference tree for a starting sequent → 1 [ν F ] in a SC
calculus and σ a substitution. The relation JT r,σ is irreflexive if, and only if, so is
T r,σ .
   Proof. (=>) Since T r,σ ⊆ JT r,σ , the necessity is obvious.
   (<=) Reductio ad absurdum. Assume T r,σ is an irreflexive relation while JT r,σ
is not. This means that h , i ∈JT r,σ for a connective                distinguished from a
variable. The relation lT r is irreflexive, it coincides with its transitive closer, and
lT r ⊆ JT r,σ . Therefore, h , i ∈JT r,σ will be satisfied only in the following case.
   The substitution σ contains such substitution components x1 7→ t1 , . . . , xn 7→ tn
(n ≥ 1) that for parameters y1 , . . . , yn from t1 , . . . , tn respectively the following
                                                Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
250     ·      Alexander Lyaletski

takes place: x1 lT r , y1 T r,σ x1 , x2 ≺F y1 , y2 T r,σ x2 , x3 ≺F y2 , . . .,
yn T r,σ xn , and lT r yn .
  This implies x1 lT r yn , i.e. x1 T r,σ yn holds. Using the just given inequalities, we
obtain that x1 T r,σ x1 by the transitivity of T r,σ . This contradicts the assumption
on the irreflexivity of T r,σ .

7.    KANGER-TYPE CALCULI WITH ADMISSIBILITY AND COMPATIBILITY
The next step in our considerations is to improve the efficiency of quantifier handling
in KC+Modm using the above-given notions of admissibility and compatibility
and rejecting from the applications of any quantifier rules. For this, we determine
a family of special calculi, which, in opposite to K≈ from [17] exploiting dum-
mies and parameters as well as so-called substitution lists for determining Kanger’s
admissibility, uses the above-introduced notions of admissibility and computability.
   This family is denoted by BC+Modm , where BC is determined in Fig. 1.
Any its calculus contains all the rules of KC+Modm except (∀ →) and (→ ∃)
that are replaced by (∀# →) and (→ ∃# ). We see that similar to KC+Modm ,
its special cases (with or without equality and modal rules) lead to the following
calculi: BK≈ +Modm , BK+Modm , BK≈ , and BK for the classical case and
BJ≈ +Modm , BJ+Modm , BJ≈ , and BJ for the intuitionistic case, where BK
and BJ denote classical and intuitionistic calculi respectively.
   As in the case of KC+Modm , proof search in BC+Modm is of the form of
an inference tree for a starting sequent of the form → 1 [ν F ] and is performed in
the Kanger style, i.e. it consists of two stages: equality-independent and equality-
dependent ones.
   The equality-independent stage includes two steps that have been described for
KC+Modm , but in opposite to KC+Modm , it is completed by the construction
of an inference tree, say, T r, and the selection of a certain substitution, say, σ,
replacing all the free dummies from T r by terms without dummies. If not all the
leaves of T r · σ are axioms, then in the equality-dependent stage, only equality rules
are applied to the non-axiom leaves of T r · σ, after this to their “heirs”, and so on,
attempting to construct a proof tree (i.e. a tree containing only axioms in leaves).
In the case of success, the deduction is completed and T r is declared as a latent
proof tree for → 1 [ν F ] w.r.t. σ in BK≈ +Modm . Otherwise, the same is being
repeated for → 1 [ν F ] again, if necessary.
   The Kanger style proof search in BC+Modm gives the possibility to impose
some restrictions on a substitution that can be selected before going to the equality-
dependent stage.
   Lemma 2. Let T r be a latent proof tree for a starting sequent → 1 [ν F ] w.r.t.
a substitution σ in BC+Modm . Then σ can be considered as a substitution re-
placing all the free dummies in T r by terms without dummies. Moreover, for any
substitution component of x 7→ t ∈ σ, x can be considered as to be a free dummy
and t as to be a term containing only functional and constant symbols from → 1 [ν F ]
(including, possibly, c0 ) as well as free parameters from T r.
  Proof. Since a substitution component in x 7→ c0 , where in x is a free dummy not
being a variable of σ and occurring in T r · σ and, therefore, in T r, can be added

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
              Mathematical Text Processing in EA-style: a Sequent Approach            ·     251

to σ, then σ can be considered as to replace all the free dummies in T r and only
them by terms without dummies.
   Now suppose that in terms of σ there are functional symbols (including constant
symbols distinct from c0 ) not occurring in → 1 [ν F ]. Then in T r can be leaves with
axioms containing such functional symbols and/or constants. These axioms are of
the form Γ, A → A, ∆, where A can supposed an atomic formula. All the rules of
our calculi possess the subformula property. Therefore, in → 1 [F ] there are two
atomic formulas, for copies A1 and A2 of which A1 · σ = A2 · σ = A. Hence, σ is a
simultaneous unifier of all such pairs of atomic formulas.
   Using the most general unifier algorithm from [40], it is possible to generate
the most general simultaneous unifier σ 0 of all the just described pairs of atomic
formulas with the following property satisfied: all the terms of σ 0 contain only
functional and constant symbols (including, maybe, c0 ) from → 1 [ν F ] as well as
dummies and parameters from T r and there is such a substitution λ that σ = σ 0 · λ.
This means that only terms of λ (not containing dummies) can contain functional
and constant symbols not occurring in → 1 [ν F ].
   Transform λ in a substitution λ0 by means of the replacement of all its (maximal)
terms beginning with such a functional or constant symbol by the constant c0 . For
λ0 we have that the terms of λ0 do not contain dummies and σ 0 · λ0 is a simultaneous
unificator of all the above-mentioned pairs of atomic formulas.
   Let us take in T r such a leaf with a sequent S that S · σ is not an axiom. Then
on the equality-dependent stage, the sequent S · σ(= (S · σ 0 ) · λ = S · (σ 0 · λ)) can
be transformed into an axiom by applying only equality rules. But in this case it
is obvious that there exists a sequence of equality rules applications transforming
the leaf S · (σ 0 · λ0 ) (without dummies) into an axiom of BC+Modm . Since this
takes place for any such S, for completing the proof, it remains to note that σ 0 · λ0
can be taken as σ, to which is referred in the lemma.
  In what follows, the restriction on σ given in Lemma 2 is always supposed to be
satisfied.
   Proposition 2. For a closed formula F , the initial sequent → F is deducible
in the KC+Modm calculus if, and only if, an inference tree T r for the start-
ing sequent → 1 [ν F ] can be constructed at the equality-independent stage in the
BC+Modm calculus and a substitution σ of terms without dummies for all the
free dummies from T r can be selected in such a way that the following conditions
take place: (i) T r is a latent proof tree for → 1 [ν F ] w.r.t. σ in BC+Modm ,
(ii) σ is admissible for T r, (iii) T r is compatible with σ w.r.t. BC+Modm .
   Proof. First of all note that because of the construction of KC+ Modm and
BC+Modm (distinguished by the quantifier rules only), it is sufficient to prove
Proposition 2 for the calculi KK≈ and BK≈ . Moreover, because of the requirement
of making proof search in both KK≈ and BK≈ in the Kanger style, it is sufficient
to prove the following:
   (*) If T r is an inference tree for → 1 [ν F ] in BK and a substitution σ is selected in
such a way that (ii) and (iii) are satisfied, then one can construct such an inference
tree T r0 for → 1 [ν F ] in KK that T r · σ coincides with T r0 , and vice versa, if T r0 is
an inference tree in KK, then one can construct an inference tree T r for → 1 [ν F ]

                                            Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
252     ·      Alexander Lyaletski

in BK and select a substitution σ in such a way that (ii) and (iii) are satisfied and
T r0 coincides with T r · σ.
   Additionally note that Lemma 1 allows us to replace (ii) (requiring the irreflex-
ivity of T r,σ ) by the requirement of the irreflexivity of JT r,σ .
   The following reasonings lead to proving (*) with the modified item (ii).
   (=>) Remind that according to Lemma 2, σ replaces all the free dummies in
T r by terms without dummies and any such term can contain constants (including
c0 ), functional symbols, and free parameters from T r. The formula F is closed.
Therefore, any dummy of σ is introduced by the application of (∀# →) or (→ ∃# ).
That is why it is sometimes convenient to write its substitution component as
(l+1)+i                                     #              #
        n x 7→ ti (see the definitions of (∀ →) and (→ ∃ ) in Fig. 1).
   By condition, the relation JT r,σ is irreflective. Thus, JT r,σ can be extended to a
strict linear order relation J + T r,σ such that JT r,σ ⊆ J + T r,σ . That is J + T r,σ takes
place for any pair of distinct elements        and 0 from JT r,σ and h , 0 i ∈ JT r,σ
                 0       +
implies h , i ∈ J T r,σ .
   As a result, we obtain that J + T r,σ can be taken as a proper sequence for T r
providing the compatibility of T r with σ w.r.t BK. This along with the linearity
of J + T r,σ implies that if (l+1)+in x 7→ ti ∈ σ, then for any parameter qm y from ti ,
hqm y, (l+1)+in x 7→ ti i ∈ J + T r,σ .
   Keeping in mind the just said and Lemma 2, we conclude that the tree T r · σ can
be constructed by the “multiplication” of T r by any arbitrarily selected substitution
component of σ at the first step, the “multiplication” of the obtained result by any
other arbitrarily selected substitution component of σ at the second step, and so
on until all the substitution components of σ have been exhausted.
   By this property of T r · σ, now it is easy to see that T r · σ can be considered
as an inference tree in the KK calculus, the way of the construction of which is
determined by the rules applications order J + T r,σ , which means that the first
connective of J + T r,σ determines the selection of the first rule for its application for
the construction of T r · σ, the second connective of J + T r,σ determines the selection
of the second rule application for the construction of T r · σ, and so on until all the
connectives of J + T r,σ have been looked through.
   Indeed, the application of any rule of BK eliminating a connective in T r and
distinguished from both (∀# →) and (→ ∃# ) can be considered as the application
of the same rule in T r · σ, but already in the KK calculus.
   Let us consider the case of the rule (∀# →) ((→ ∃# )) that is applied at a node
N of T r after applying all other rules proceeding to this application according to
the order J + T r,σ .
   Let it be of the form
                 Γ, in ∀in xA → ∆                       Γ → in ∃in xA, ∆
                       i x              (∀∗ →)    (            i   x
                                                                              (→ ∃∗ )),
               Γ, A|   n
                       (l+1)+i x   →∆                  Γ → A|n(l+1)+i x , ∆
                             n                                         n

                            (l+1)+i
where for a dummy              there is a term ti such that (l+1)+in x 7→ ti ∈ σ;
                                  nx
moreover, as it was said earlier, for any parameter qm y from ti , hqm y, (l+1)+in xi
                                                                                       i
                                                                                           x
∈ J + T r,σ , which means that the term ti is free for                 (l+1)+i
                                                                             nx   in A|n(l+1)+i x and,
                                                                                               n
therefore, ti is free for in x in A. Hence, it can considered that at the node N of the

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
               Mathematical Text Processing in EA-style: a Sequent Approach                  ·    253

tree T r · σ, the rule
                   Γ, in ∀in xA → ∆                    Γ → in ∃in xA, ∆
                              i x         (∀ →)    (               i   x
                                                                               (→ ∃))
                      Γ, A|   n
                              ti    →∆                  Γ → A|nti , ∆
of KK satisfying the Gentzen admissibility is applied.
   Thus, T r · σ can be constructed according to the order J + T r,σ . For completing
the proving of the necessity in (*), it remains to take T r · σ as T r0 .
   (<=) Suppose that T r0 is an inference tree for → 1 [ν F ] in KK and α10 , . . ., αk0
the sequence of rules applications in T r0 (among of which the applications of both
Con → and → Con may occur) leading to the construction of T r0 when looking
through it from left to right.
   This means that the process of the construction of T r0 in KK can be considered
as the subsequent construction of trees T r00 , T r10 , . . . , T rk0 , where T r00 is the tree
with the only root N0 labeled by → 1 [ν F ], T r10 is generated by the application of
α10 to the unique leaf N0 of T r00 , T r20 is generated by the application of α20 to a leaf
N1 of T r10 , . . ., and T rk0 (coinciding with T r0 ) is generated by the application of αk0
                          0
to a leaf Nk−1 of T rk−1       .
   Let j1 1 , . . ., jr r is a sequence of all the connectives being eliminated in T r0
by some applications from α10 , . . ., αr0 and written from left to right according to
their elimination (r ≤ k).
   Let us make the subsequent construction of inference trees T r0 , T r1 , . . . , T rk in
BK, simultaneously determining inference rules α1 , . . ., αk of BK and defining
substitutions σ0 , σ1 , . . . , σr in the following way.
   (I) T r0 coincides with T r00 ; σ0 = ∅.
                  0
   (II) Let T rj−1     be already constructed and σj−1 be already defined (1 ≤ j ≤ r).
        (II.1) Suppose αj0 is the application of (∀ →) ((→ ∃)) to the node Nj−1 in
    0
T rj−1  and is of the form
                   Γ, in ∀in xA → ∆                    Γ → in ∃in xA, ∆
                            i   x
                                         (∀ →)     (               i   x
                                                                               (→ ∃)),
                      Γ, A|nti → ∆                      Γ → A|nti , ∆
where ti is a term being a free for in x in A. Then αj denotes the application of the
following rule
                Γ, in ∀in xA → ∆                        Γ → in ∃in xA, ∆
                      i x                (∀∗ →)    (           i   x
                                                                                 (→ ∃∗ )),
              Γ, A|   n
                      (l+1)+i x     →∆                 Γ → A|n(l+1)+i x , ∆
                            n                                              n


to Nj−1 in T rj−1 , thereby generating T rj ; σj is defined as the set σj−1 ∪ {(l+1)+in x
7→ ti } being a substitution because l + 1 is a new index (w.r.t. T rj−1 ) and any
two nodes of T rj−1 lying in different branches of T rj−1 have no common bound
variables.
       (II.2) In all the other cases, αj denotes the application αj0 (i.e. the application
                                                   0
of the same rule that was applied to Nj−1 of T rj−1    for generating T rj0 ), T rj denotes
the result of application αj to T rj−1 , and σj is defined as equal to σj−1 .
   If we take T rk as T r and σk as σ, it is obvious that T r is an inference tree in
BK, σ is a substitution of terms without dummies for all the free dummies from
T r, and T r0 coincides with T r · σ.
   Now we can prove that (ii) and (iii) from (*) take place.
                                                  Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
254     ·      Alexander Lyaletski

    Let us consider the sequence α1 , . . ., αk . According to its definition, each αk is
(Con →) or (→ Con) or eliminates one of the connectives j1 1 , . . ., jr r ; at that,
these connectives and only they occur in T r.
    Obviously, j1 1 , . . ., jr r can be considered as a strict linear order (say, Λ) cor-
responding to the elimination of the connectives in T r according to the subsequent
applications of α1 , . . ., αk in T r. This implies that j1 1 , . . ., jr r is a proper
sequence for T r.
    Suppose (l+1)+in x 7→ ti ∈ σ is a substitution component defined at the step
(II.1). Since the term ti is free for in x in A, then for any parameter i y from ti ,
hi y, in x(l+1)+in x i ∈ Λ, which proves the inclusion T r,σ ⊆ Λ.
    In its turn, if hy, xi ∈ lT r , then y and x occur in Λ and hy, xi ∈ Λ. This and
the coincidence of the sets of all dummies and parameters from Λ and lT r lead to
the inclusion JT r,σ ⊆ Λ. Λ is a strict linear order. Therefore, it is irreflexive and
it coincides with its transitive closer. Hence, JT r,σ ⊆ Λ, which means that JT r,σ
is an irreflexive relation. The proof of (ii) form (*) is completed.
    For proving (iii) from (*) , it is enough to note that the inclusion JT r,σ ⊆ Λ
provides the compatibility of T r with σ w.r.t. BK, since T r was constructed
according to the subsequent applications α1 , . . ., αk containing the applications
eliminating j1 1 , . . ., jr r in the accordance with the order Λ.
   Now we can transform this proposition into its special forms.
   Suppose F is a formula and σ a substitution. Let J−         F,σ denote all the pairs
h , 0 i from JF,σ such that both and 0 are not quantifier connectives (or their
variables). (The same concerns J−          −          −
                                    S,σ , JΞ,σ , and JT r,σ , where S is a sequent, Ξ a
set of formulas or sequents, and T r an inference tree.)
   An inference tree T r is called propositionally compatible with a substitution σ
w.r.t. a sequent calculus SC if, and only if, the condition of the compatibility of
T r with σ w.r.t. SC is satisfied for any pair hjn n ,jm m i from J−    T r,σ .

  Theorem 1. For a closed formula F , the initial sequent → F is deducible in an
intuitionistic (modal) calculus KJ≈ +Modm if, and only if, an inference tree T r for
the starting sequent → 1 [ν F ] can be constructed at the equality-independent stage
in BJ≈ +Modm and a substitution σ of terms without dummies for all the free
dummies from T r can be selected in such a way that the following conditions take
place: (i) T r is a latent proof tree for →1 [ν F ] w.r.t. σ in BJ≈ +Modm , (ii) σ is
admissible for T r, (iii) T r is propositionally compatible with σ w.r.t. BJ+Modm .
   Proof. According to Proposition 2, this theorem will take place if we show that
the compatibility from (iii) of Proposition 2 can be replaced by the propositional
compatibility w.r.t. BJ+Modm .
   On the basis of Lemma 1, the admissibility of σ for T r is equivalent to the
irreflexivity of JT r,σ . This means that in the case of the admissibility of the sub-
stitution σ for the tree T r in BJ + Modm , it is enough to check the propositional
compatibility of the T r with σ. (The restriction providing the intuitionistic case in
the paper consists in that the succedent of any deduced sequent should contain no
more than one formula.)
   Since proof search in BJ≈ +Modm is always made in the Kanger style, the
applications of the equality rules (and only them) on the equality-dependent stage

Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                  Mathematical Text Processing in EA-style: a Sequent Approach                            ·    255

have no influence on the relation JT r,σ generated earlier. This means that it is
enough to check the compatibility of the tree T r with the substitution σ only w.r.t.
BJ+Modm .
   As for the classical case, when there are no restrictions on on the form of sequents
and orders of propositional and modal rule applications, Proposition 2 takes the
following form.
   Theorem 2. For a closed formula F , the initial sequent → F is deducible in a
classical (modal) calculus KK≈ +Modm if, and only if, an inference tree T r for
the starting sequent → 1 [ν F ] can be constructed at the equality-independent stage
in BK≈ +Modm and a substitution σ of terms without dummies for all the free
dummies from T r can be selected in such a way that the following conditions take
place: (i ) T r is a latent proof tree for →1 [ν F ] w.r.t. σ in BK≈ +Modm and
(ii) σ is admissible for T r.
   Proof. Since there are no restrictions on the form of sequents and orders of ap-
plications of logical and modal rules in BK≈ +Modm , the item (iii) in Proposition
2 becomes redundant: any latent proof tree T r constructed in BK≈ +Modm is
compatible with any σ if, and only if, σ is an admissible for T r.
    EXAMPLE 1. Let us demonstrate the peculiarities of proof search in BC+
Modm for its concretizations as the calculi BK≈ and BJ≈ .
    Consider the classical-type modal calculus GK and intuitionistic-type modal
calculus JGK from [39]. In our notation, GK with equality can be determined as
KK≈ +{(2)} and JGK with equality as KJ≈ +{(2), (3)}, where (2) is the modal
        2Γ → 2G                                                 3Γ → 3G
rule                     and (3) the modal rule                                  . (Here, G is a formula, Γ
            Γ→G                                                    Γ→G
is a multiset of formulas F1 , . . . , Fk , and 2Γ and 3Γ denote multisets of formulas
2F1 , . . . , 2Fk and 3F1 , . . . , 3Fk respectively.)
    Consider the formula H ∗ = ∃y¬2∃x(y ≈ f (y) ⊃ P (x, y)) ⊃ ¬∀y 0 2∃x0 P (x0 , f (y 0 ))
being the modification of F ∗ for the case of logics with equality.
    Looking along H ∗ from left to right, we are “numbering” all its connectives with
the help of left down indexes in the following way: ∃y receives 1, ¬ receives 2, . . .,
∃x0 receives 10.
    Now we can construct the following tree T r for → 1 [H ∗ ] being an inference tree
                                                                                    ∗          1
in both BK≈ + {(2)} and BJ≈ + {(2), (3)} (here, 1 [H ] = 11 ∃11 y 12 ¬3 214 ∃14 x(11 y ≈
                                      1         1                      0         0
f (11 y) 15 ⊃ P (14 x,11 y)) 16 ⊃ 17 ¬8 ∀18 y 0 9 2110 ∃110 x0 P (110 x , f (18 y ))):
                                                ∗
                                        → 1 [H ]                                           (a starting sequent)
1 1 1 1 1 1                                                    1 1 1 01 1                     0   1 0
1 ∃1 y 2 ¬3 24 ∃4 x(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y)) → 7 ¬8 ∀8 y 9 210 ∃10 x P (10 x , f (8 y ))
                       1             1      1      1 1                           1   0    1
                                                                                                        (by (→⊃))
   3 3 3 3                                                  1 1 1 01 1                      0   1 0
   2 ¬3 24 ∃4 x(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y)) → 7 ¬8 ∀8 y 9 210 ∃10 x P (10 x , f (8 y ))
                  3              3     3        3 3                           1    0   1
                                                                                                        (by (∃ →))
         3                                                 1 1 01 1                   0       0
     2 ¬3 24 ∃4 x(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y)), 8 ∀8 y 9 210 ∃10 x P (10 x , f (8 y )) →
     3      3 3      3             3     3       3 3                    1    0   1          1
                                                                                                        (by (→ ¬))
        3 3 3 3                                                                         5 0
          ¬3 24 ∃4 x(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y)), 9 210 ∃10 x P (10 x , f (8 y )) →
                         3             3      3     3 3      5 5    5   0     5   0
                                                                                                        (by (∀ →))
                                           5 0
          9 210 ∃10 x P (10 x , f (8 y )) → 3 24 ∃4 x(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y))
          5 5     5     0     5     0                3 3 3   3        3     3        3 3
                                                                                                        (by (¬ →))
          5   5    0      5    0       5  0       3 3   3       3   3          3 3
          10 ∃10 x P (10 x , f (8 y )) → 4 ∃4 x(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y))                            (by (2))
                                       0
                 P (11      0      5            3 3   3      3    3        3 3
                      10 x , f (8 y )) → 4 ∃4 x(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y))                          (by (→ ∃))
                        11 0          5 0         3       3    15        15 3
                   P (10 x , f (8 y )) → (1 y ≈ f (1 y)) 5 ⊃ P (4 x,1 y)                                (by (∃ →))
                                                        Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
256     ·      Alexander Lyaletski

                                0
                  P (11  0     5      3        3         15 3
                     10 x , f (8 y )),1 y ≈ f (1 y) → P (4 x,1 y))                   (by (→⊃))
   According to definitions, x and y 0 are dummies in H ∗ , while x0 and y parameters
(in H ∗ ). Hence, 14 x, 34 x, 15    1 0      5 0                       1 0 5 0 11 0 1
                              4 x, 8 y , and 8 y are dummies while 10 x , 10 x , 10 x , 1 y, and
3
1 y are parameters.
                                                           11 0 5 0
   The application of the substitution σ = {15                            3
                                                    4 x 7→ 10 x , 8 y 7→ 1 y} to T r transforms
                                     11 0    3     3        3           11 0 3
the unique leaf of T r into P (10 x , f (1 y)), 1 y ≈ f (1 y) → P (10 x ,1 y). By applying
the rule (→≈) to this sequent w.r.t. 31 y ≈ f (31 y), we can deduce the axiom P (11             0
                                                                                            10 x ,
3     3        3             11 0 3
1 y), 1 y ≈ f (1 y) → P (10 x ,1 y). Thus, T r is a latent proof tree w.r.t. σ in both
BK≈ + {(2)} and BJ≈ + {(2), (3)}. We can check the admissibility of σ for
T r and propositional compatibility of T r with σ w.r.t. BJ≈ + {(2), (3)}. By
Theorems 1 and 2, we obtain the deducibility of → H ∗ in both KK≈ + {(2)} and
KJ≈ + {(2), (3)}.
   For the formula H1∗ = ¬∀y2∃x(y ≈ f (y) ⊃ P (x, y)) ⊃ ∃y 0 ¬2∃x0 P (x0 , f (y 0 )),
being a modification of H ∗ , T r can be easily transformed into a latent proof tree
T r0 for → 1 [H1∗ ] w.r.t. σ 0 in both BK≈ + {(2)} and BJ≈ + {(2), (3)}, where σ 0
is the corresponding transformation of σ. The substitution σ 0 will be admissible
for T r0 . Therefore, → H1∗ becomes deducible in KK≈ + {(2)} by Theorem 2. At
the same time, it can be proved that for → 1 [H1∗ ], neither T r0 nor any other latent
proof tree will be propositionally compatible with σ 0 or any other “reasonable”
substitution. Hence, by Theorem 1, → H1∗ is not deducible in KJ≈ + {(2), (3)}.
   For the formula H2∗ = ∀y¬∀x2(y ≈ f (y) ⊃ P (x, y))⊃¬∀y 0 2∃x0 P (x0 , f (y 0 ))
being another modification of H ∗ , T r can be transformed into T r00 being a latent
tree for → 1 [H2∗ ] w.r.t. corresponding σ 00 in both the calculi. At that, σ 00 will not
be admissible for T r00 . Moreover, it can be proved that for any other latent proof
tree for → 1 [H2∗ ], there is no substitution admissible for it. Hence, by Theorems 1
and 2, → H2∗ cannot be deduced neither in BK≈ + {(2)} nor in BJ≈ + {(2), (3)}.
   Pay your attention to the fact that the order of quantifier rules applications in
T r from Example 1 is immaterial; it can be any. The other peculiarity is that
the quantifier rules simply introduce new parameters and dummies participating in
checking admissibility and compatibility. This observation serves as a “guide” to
constructing quantifier-rule-free sequent calculi.

8.    QUANTIFIER-RULE-FREE SEQUENT CALCULI
Now we can move to the construction of first-order quantifier-rule-free sequent
calculi on the basis of the introduced notions of admissibility and compatibility.
   At first sight it may seem that the best way to achieve this is to simply initiate
a search of a sequent → µ(1 [ν F ]) in BC+Modm without using its quantifier rules.
Obviously, with this approach, Proposition 2 holds for all the sequents deduced in
KC+Modm . However, it also turns out to be valid for some sequences, which are
not deducible in KC+Modm . This is coursed by that during the transformation
of → F into → µ(1 [ν F ]), the loss of the information about locations of quantifiers
in F is observed, while this information is used in proof search in BC+Modm for
renaming certain variables when applying this or that quantifier rule.
   For example, for F1∗ = ((P (a) ∨ P (b)) ⊃ ∃xP (x)) and F2∗ = ∃x((P (a) ∨ P (b)) ⊃
P (x)), where a and b are constants and x a dummy, both the sequents → F1∗
and → F2∗ are deducible in KK, while → F1 is deducible in KJ and → F2 is
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
               Mathematical Text Processing in EA-style: a Sequent Approach              ·     257

not. For µ(1 [ν F1∗ ]) = (P (a) 11 ∨ P (b)) 12 ⊃ P (13 x) and µ(1 [ν F2∗ ]) = (P (a) 12 ∨
P (b))13 ⊃ P (11 x), both the sequents → µ(1 [ν F1∗ ]) and → µ(1 [ν F2∗ ]) are not deducible
even in BK, despite 11 x and 13 x are dummies: after removing the quantifier rules,
there is no possibility to produce the necessary copies of P (11 x) and P (13 x) with new
dummies. On the other hand, if we allow doubling, for example, all atomic formulas
with possible reindexing all their dummies and parameters, we can establish the
deductibility of sequences → µ(1 [ν F1∗ ]) and → µ(1 [ν F2∗ ]) in both BK and BJ and,
as a result, establish the deducibility of → F1∗ and → F2∗ in both KK and KJ on the
basis of Theorems 1 and 2. But, as it was mentioned above, the sequent → F2∗ is not
deducible in KJ. So, we should develop a special technique for indexing variables
that takes into account the locations of the quantifiers in an original formula.
   Let formulas G and F be taken from the definition of kF [G], where k is a natural
number (k ≥ 1). Suppose there is such an ex-variable (i.e., parameter or dummy)
i
n x for G relative to F that there is no external connectives         (including the case of a
                                                                                     i
variable) for G w.r.t. F , for which n xlF takes place. Then the formula n x<k F [G]
                                         i

is defined in the following way: it coincides with akF [G], in which all occurrences of
                                                                                  i
i                                                      k+i                        n x<k [G] is
n x are replaced simultaneously by a variable            n x. In all other cases,        F
                             k
declared to be equal to F [G].
                          i                     i
   For short we write n x<k [G] instead of n x<kF [G] in the cases when F is considered
to be known.
   Analogously to kF [·], the operation x<kF [·] converts graphically distinct connec-
tives and variables into graphically distinct connectives and variables, inducing a
renaming of parameters with parameters only and dummies with dummies only.
   For example, for the formula G = ¬1 21 ∃1 x P (1 x, f (1 y)) (with the missed left
down indexes) being a copy of the subformula ¬2∃xP (x, f (y)) of F ∗ , the formu-
                                             1
las 2 [G] = 2 ¬3 23 ∃3 xP (3 x, f (1 y)) and y<2 [G] = 2 ¬3 23 ∃3 xP (3 x, f (3 y)) (2 [G] and
1
  y<2
      [G] are distinguished by the variables 1 y and 3 y) only. If G0 = P (3 x, f (1 y)),
                                      3
then 2 [G0 ] = P (3 x, f (1 y)) and x<2 [G0 ] = P (5 x, f (1 y)). If G00 = 3 ∃3 xP (3 x, f (3 y)),
then 2 [G00 ] = 5 ∃5 xP (5 x, f (3 y) =z<2 [G00 ] for any variable z.
   The operation x<k F   [·] makes it possible to refuse all the quantifier rules, replacing
them by the rules (Con# →) and (→ Con# ) (see Fig. 1). As a result, we get
a family of first-order quantifier-rule-free sequent calculi denoted by QC+Modm ,
where QC contains all the propositional, contraction, and equality rules as well as
all the axioms.
   Analogously to BC+Modm , we get the following modifications of QC+Modm :
QK≈ +Modm , QJ≈ +Modm , QK+Modm , QK+Modm , QK≈ , QJ≈ , QK, QJ,
where QK and QJ denote the calculi for classical and intuitionistic logics without
equality respectively.
   Note that inference search in QC+Modm is made in the Kanger style, the
equality-independent stage of which, due to the absence of quantifiers, consists of
the second step only.
   Proposition 3. For a closed formula F , the initial sequent → F is deducible in
the KC+Modm calculus if, and only if, an inference tree T r for → µ(1 [ν F ]) can
be constructed at the equality-independent stage in the QC+Modm calculus and a
substitution σ of terms without dummies for all the free dummies from T r can be
selected in such a way that the following conditions take place: (i) T r is a latent
                                               Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
258     ·      Alexander Lyaletski

proof tree for → µ(1 [ν F ]) w.r.t. σ in QC+Modm , (ii) σ is admissible for T r,
(iii) T r is propositionally compatible with σ w.r.t. QC+Modm .
   Proof. By Proposition 2, → 1 [ν F ] is deducible in KC+Modm if, and only if,
an inference tree T r0 can be produced in BC+Modm and a substitution σ 0 of
terms without dummies for all the free dummies from T r can be selected in such a
way that (i), (ii), and (iii) from Proposition 2 take place for T r0 and σ 0 . Obviously,
it can be assumed that T r0 is constructed from top to bottom and left to right and
that all the leaves of T r0 do not contain quantifiers and some part of these leaves are
axioms, while the other leaves, not being axioms, can be transformed into axioms
by applying equality rules at the equality-dependent stage.
   Let us consider a sequent tree µ(T r0 ) being the result of the application of µ to
all the sequents of T r0 . Denote it by T r (T r = µ(T r0 )). The sequent → µ(1 [ν F ])
lies in its root. Besides, it is quantifier-free and contains the same axioms as T r0
contains. At the equality-dependent stage, all leaves of T r not being axioms are
transformed into axioms. This means that for proving that T r is a latent proof tree
for →1 [ν F ] w.r.t. σ in QC+Modm , it is enough to prove that any sequent of T r
not being its root is deduced by an inference rule.
   Suppose a sequent S from T r0 is deduced by a propositional rule, modal rule, or
contraction rule (either (→ Con) or (Con →)). Then, on the basis of the properties
of µ, we conclude that the quantifier-free sequent µ(S) can be considered as it was
deduced in QC+Modm by the application of the same propositional, modal, or
contraction rule that was used when deducing S in KC+Modm .
   Suppose S is deduced in T r0 by one of the quantifier rules, say, for certainty,
                    Γ, in ∀in xA → ∆                                  i
       #                                                     l+1      nx
by (∀ →):                   i x            . (That is S = Γ,     [A]| (l+1)+i x → ∆). Then
                Γ, l+1 [A]|n(l+1)+ i x → ∆                                  n
                                  n
                          µ(Γ), µ(A) → µ(∆)
T r contains                       i   x               , being the application of (Con# →),
                µ(Γ), l+1 [µ(A)]|n(l+1)+i x → µ(∆)
                                           n
                  i
                      x                                         i
since l+1 [µ(A)]|n(l+1)+i x is another form of the formula n x<(l+1) [µ(A)].
                        n
   The consideration of all the possible applications of the other quantifier rules
in T r0 is made similar. This lead to that quantifier rules applications in T r0 can
be replaced by the applications of an appropriate contraction rule (Con# →) or
(→ Con# ) finally producing T r.
   Hence, T r is a latent proof tree for → µ(1 [ν F ]) w.r.t. σ in QC+Modm . Ac-
cording to the construction of T r, we have that the sets of free variables of T r and
T r0 are coincided and that JT r,σ =JT r0 ,σ . Thus, (i), (ii), and (iii) take place for T r
and σ in the case of QC+Modm .
   The poof in one direction is completed.
   Now suppose that σ is a substitution and T r an inference tree for → µ(1 [ν F ]) in
QC+Modm satisfying (i), (ii), and (iii). Convert T r into a sequent tree T r0 in the
BC+Modm calculus in a way, similar to the just given above, but starting this
conversation with the leaves of T r and moving through T r from right to left and
bottom to top.
   This means that all the leaves of T r are declared as leaves of T r0 and any ap-
plication of a propositiona,l, modal , or one of the contraction rules (→ Con) and
(Con →) in T r is replaced by the application of the same inference rule, but already
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
              Mathematical Text Processing in EA-style: a Sequent Approach           ·     259

in the BC+Modm calculus. As to the contraction rules (Con# →) and (→ Con# ),
the application of any of them is replaced by the application of a certain quanti-
fier rule from BC+Modm , the selection of which is determined by which of the
rules (Con# →) or (→ Con# ) is under consideration and the type of a variable in x
(dummy or parameter) introduced by this application.
   Suppose for certainty that at some step of the construction of T r0 , the rule
(→ Con# ) was applied (the consideration of the other cases of the possible appli-
                                                      Γ → A, ∆
cations of (Con# →) and (→ Con# ) is similar):               i x           producing
                                                Γ → l+1 [A]|n(l+1)+i x , ∆
                                                                             n
                          i                                              i
                              x                                              x
the sequent Γ → l+1 [A]|n(l+1)+i x , ∆, in which the formula l+1 [A]|n(l+1)+i x is already
                                  n                                         n
generated in T r0 (remind that the construction of T r0 in made from right to left and
bottom to top). Then this application of (→ Con# ) in T r becomes the (→ ∀)-rule
                    Γ → in ∀in xA0 , ∆
application:                  i x          in T r0 .
              Γ → l+1 [A0 ]|n(l+1)+i x , ∆
                                     n
   Making all such replacements of inference rule applications, when moving in T r
from right to left and bottom to top, we finally produce the root of T r0 with the
sequent → 1 [ν F ].
   According to the construction of T r0 , T r0 is a latent proof tree for → 1 [ν F ]
w.r.t. σ in BC≈ +Modm . Besides, the sets of free variables of T r and T r0 coincide
and JT r,σ =JT r0 ,σ , which means that (i), (ii), and (iii) take place for T r0 and σ in
BC+Modm . By Proposition 2, → F is deducible in the calculus KC+Modm .
  Now we can reformulate Proposition 3 for the case of our intuitionistic modal
logics in the following way, the proof of which “repeats” the proof of Theorems 1.
   Theorem 3. For a closed formula F , the initial sequent → F is deducible in
the intuitionistic modal calculus KJ≈ +Modm if, and only if, an inference tree T r
for the sequent → µ(1 [ν F ]) can be constructed at the equality-independent stage in
QJ≈ +Modm and a substitution σ of terms without dummies for all the dummies
from T r can be selected in such a way that the following conditions take
place: (i) T r is a latent proof tree for →1 [ν F ] w.r.t. σ in QJ≈ +Modm , (ii) σ is
admissible for T r, (iii) T r is propositionally compatible with σ w.r.t. QJ+Modm .
   As for the classical case, when there are no any restrictions on the form of sequents
and order of propositional and modal rule applications, Proposition 3 takes the
following form.
   Theorem 4. For a closed formula F , the initial sequent → F is deducible in
the classical modal calculus KK≈ +Modm if, and only if, an inference tree T r
for the sequent → µ(1 [ν F ]) can be constructed at the equality-independent stage in
QK≈ +Modm and a substitution σ of terms without dummies for all the dummies
from T r can be selected in such a way that the following conditions take place:
(i) T r is a latent proof tree for →1 [ν F ] w.r.t. σ in QC≈ +Modm and (ii) σ is
admissible for T r.
  The below-given examples give a possibility to gain some insight about proof
search in our quantifier-rule-free calculi.

                                           Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
260        ·     Alexander Lyaletski

  EXAMPLE 2. Let us demonstrate some peculiarities of the applications of
(→ Con∗ ) and (Con∗ →) in QC≈ + Modm using F1∗ and F2∗ given at the beginning
of this section. For them we have µ(1 [ν F1∗ ]) = ((P (a) 11 ∨ P (b)) 12 ⊃ P (13 x)) and
µ(1 [ν F2∗ ]) = ((P (a) 12 ∨ P (b)) 13 ⊃ P (11 x)).
  For → µ(1 [ν F1∗ ]), we can construct the below-given tree T r being an inference
tree T r in both QJ and QK:
                              → (P (a)11 ∨P (b))12 ⊃ P (13 x)        (a starting sequent)
                                 P (a)11 ∨P (b) → P (13 x)                     (by (→⊃))
                            P (a) → P (13 x)       P (b) → P (13 x)            (by (∨ →))
                        P (a) → P (33 x), P (13 x)                  (by (→ Con∗ ), when
                              n = 3, i = l = 1, F = F1∗ , and A = P (11 x) (see definition))
   The application of the substitution σ = {13 x 7→ b,33 x 7→ a} converts the leaves of
this tree into axioms. Hence, T r is a latent proof tree. Obviously, σ is admissible for
T r; moreover, T r is compatible with σ both w.r.t. QJ. Theorems 3 and 4 provide
the deducibility of → F1∗ in KJ and KK. (As a result, we obtain the deducibility
of → F1∗ in Gentzen’s calculi LJ and LK.)
   If for constructing a latent proof tree for → µ(1 [ν F2∗ ]) in QJ we will try to apply
(→ Con) or (→ Con∗ ) to → (P (a) 12 ∨P (b))13 ⊃ P (11 x), we will be able to deduce
only copies of → µ(1 [ν F2∗ ]). Therefore, their applications will give nothing new for
our purpose and it only remains to apply propositional rules. As a result, we will
be able to construct the following inference tree:
                     → (P (a)12 ∨P (b))13 ⊃ P (11 x)                  (a starting sequent)
                         P (a)12 ∨P (b) → P (11 x)                             (by (→⊃))
                    P (a) → P (11 x) P (b) → P (11 x)                          (by (∨ →))
  For converting two last sequents into axioms, it is necessary that 11 x 7→ a and
1
1x 7→ b take place, which is impossible. Hence, → µ(1 [ν F2∗ ]) is not deducible in QJ.
On the basis of Theorem 3, it cannot be deduced in KJ and, as a result, → F2∗ is
not deducible in LJ.
  The sequent → µ(1 [ν F2∗ ]) is deducible in QK, since (→ Con∗ ) can be applied to
the starting sequent → (P (a) 12 ∨ P (b)) 13 ⊃ P (11 x), giving the possibility to produce
the following inference tree:
                          → (P (a)12 ∨P (b))13 ⊃ P (11 x)                       (a starting sequent)
                        1        1       1           3         3
            → (P (a)2 ∨P (b))3 ⊃ P (1 x), (P (a)2 ∨P (b))3 ⊃ P (1 x)     3
                                                                                        (by (→ Con∗ ))
                          1              1           3         3         3
                   P (a)2 ∨P (b) → P (1 x), (P (a)2 ∨P (b))3 ⊃ P (1 x)                      (by (→⊃))
                     P (a)12 ∨P (b), P (a)32 ∨P (b) → P (11 x), P (31 x)                    (by (→⊃))
     P (a), P (a)22 ∨P (b) → P (11 x), P (31 x) P (b), P (a)32 ∨P (b) → P (11 x), P (31 x) (by (∨ →))
  This tree is a latent proof tree, since the substitution {11 x 7→ a,31 x 7→ b} converts
two last sequents into axioms. Obviously, it is admissible for the constructed tree.
Therefore, the sequent → 1 [ν F2∗ ] is deducible in the KK calculus by Theorem 4
and, as a result, the sequent → F2∗ is deducible in LK.
  EXAMPLE 3. For the formula H ∗ from Example 1, we can construct the fol-
lowing inference tree T r for → µ(H ∗ ) in QC.
           1 1                                               1                 0
           2 ¬3 2(1 y   ≈ f (11 y) 15 ⊃ P (14 x,11 y)) 16 ⊃ 17 ¬9 2P (110 x0 , f (18 y )) (a starting sequent)
                  1
       →
Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
                Mathematical Text Processing in EA-style: a Sequent Approach                     ·     261

       1 1                                               1 1                  1 0
       2 ¬3 2(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y)) → 7 ¬9 2P (10 x , f (8 y ))
               1           1     1       1 1                      1     0
                                                                                           (by (→⊃))
          1 1                                                             1 0
          2 ¬3 2(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y)), 9 2P (10 x , f (8 y )) →
                 1            1     1       1 1         1     1   0
                                                                                          (by (→ ¬))
                              1 0
            9 2P (10 x , f (8 y )) → 3 2(1 y ≈ f (1 y) 5 ⊃ P (4 x,1 y))
            1     1    0                  1    1         1   1         1 1
                                                                                          (by (¬ →))
                                   0
                P (110 x0 , f (18 y )) → 11 y ≈ f (11 y) 15 ⊃ P (14 x,11 y)                  (by (2))
                            0         0
                  P (110 x , f (18 y )), 11 y ≈ f (11 y) → P (14 x,11 y)                  (by (→⊃))

  It is obvious that T r and the substitution σ = {14 x 7→ 110 x0 , 18 y 0 7→ 11 y} satisfy the
conditions of both Theorem 3 and Theorem 4. We again obtain the deducibility of
→ H ∗ in KJ≈ and KK≈ , but already on the basis of Theorems 3 and 4.
  Draw your attention to that the just given inference is purely propositional al-
though the initial sequent → H ∗ contains quantifiers and quantifier rules should be
applied in KC for their elimination.
  Turning back to the formulas H1∗ and H2∗ from Example 1 and applying Theorems
3 and 4 for obvious modifications of T r and σ, we can “confirm” the results on the
deducibility of → H1∗ and → H2∗ given in Example 1.
  Taking into consideration all the above-given theorems, we can obtain the sound-
ness and completeness theorem for any of our calculi if, and only if, such theorems
take place for its Gentzen or Kanger analogue. For example, we conclude that
the validity of a closed formula F in classical (intuitionistic) logic with equality is
equivalent to the deductibility of the sequent → 1 [ν F ] in QK≈ (QJ≈ ).

9.   CONCLUSION
The research presented in this paper demonstrates how the attempts to satisfy the
EA principles in logical proof search gave rise to introducing the original notions of
admissibility and compatibility, which is a good enough decision of the problem of
the optimization of selecting such an order of quantifier rule applications that leads
to the success in inference search in the fastest way in some sense of this word.
As a result, a number of the quantifier-rule-free sequent calculi were constructed.
They replace the step-by-step examination of all possible orders of quantifier rules
applications by checking the conditions of admissibility and compatibility.
  Proof search in such quantifier-rule-free calculi can be divided into four steps:
propositional deduction, generating a substitution, checking admissibility and com-
patibility, applying equality rules if necessary. The notions of admissibility and
compatibility permitted to replace quantifier rules applications by the certain tech-
nique for handling bound variables. Hence, further increasing of the efficiency of
proof search in these calculi can be achieved by using, studying, and developing
special (for example, goal-oriented) methods for propositional deduction in a con-
crete logic, technique for generating a necessary substitution (applying, for example,
the results of the unification theory), tools for equality handling (developing, for
example, a paramodulation and/or E-unification techniques).
  Additionally note that the admissibility introduced in the paper has been incor-
porated into the classical logic “engines” of both the Russian and English SAD
systems and demonstrated the good results.



                                                       Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
262     ·      Alexander Lyaletski

References
 [1] V.M. Glushkov. On some problems of computer technology and related mathematical
     problems. Ukrainian Mathematical Journal, 9(4): 369-376, 1957. In Russian.
 [2] V.M. Glushkov. Some problems in the theories of automata and artificial intelligence.
     Cybernetics and System Analysis, 6(2), Springer, New York, 17-27, 1970.
 [3] R. Boyer et al. The QED manifesto. Lecture Notes in Artificial Intelligence, 814:
     238-251, 1994.
 [4] The Mizar project. Web site at http://www.mizar.org/project/.
 [5] The Calculemus project: Systems for integrated computations and deduction. Web
     site at http://www.calculemus.net/.
 [6] A.V. Lyaletski and M.K. Morokhovets. Evidential paradigm: A current state. Ab-
     stracts of AMS National Meeting “Mathematical Challenges of the 21st century”.
     USA, Los Angeles, 81, 7-12 August, 2000.
 [7] Yu. V. Kapitonova, K. P. Vershinin, A. I. Degtyarev, A. P. Zhezherun, and A. V.
     Lyaletski. System for processing mathematical texts. Cybernetics and System Anal-
     ysis, 15(2): 209–210, Springer, New York, 1979.
 [8] A. Lyaletski, K. Verchinine, A. Degtyarev, and A. Paskevich. System for Automated
     Deduction (SAD): linguistic and deductive peculiarities. Intelligent Information Sys-
     tems, 11th International Symposium, IIS 2002, Sopot, Poland, June 2002, Advances
     in Soft Computing, 413-422, 2003.
 [9] A. Lyaletski, M. Morokhovets, and A. Paskevich. Kyiv school of automated theo-
     rem proving: a historical chronicle. Logic in Central and Eastern Europe: History,
     Science, and Discourse. University Press of America, 431-469, 2012.
[10] V. M. Glushkov, Yu. V. Kapitonova, A. A Letichevskii, K. P. Vershinin, and N.
     P. Malevanyi. Construction of a practical formal language for mathematical theories.
     Cybernetics and Systems Analysis, 8(5): 730-739, 1972.
[11] , K. Vershinin and A. Paskevich, ForTheL — the language of formal theories, Inter-
     national Journal of Information Theories and Applications, 7(3): 120-126, 2000.
[12] Alexander Lyaletski and Mykola Nikitchenko. Logical and Semantic Investigations in
     Kyiv School of Automated Reasoning. Trends in Contemporary Computer Science,
     Bialystok University of Technology Publishing Office, Poland, 83-98, 2014.
[13] F. V. Anufriev, V. V. Fedyurko, A. A. Letichevskii, Z. M. Asel’derov, and I. I. Didukh.
     An algorithm for proving theorems in group theory. Cybernetics and System Analysis,
     2(1), Springer, New York,20-25, 1966.
[14] F. V. Anufriev. An algorithm for proving theorems in set theory. Theory of Automata,
     volume 4, GIC AS UkrSSR, Kiev, 3-24, 1967. In Russian.
[15] F. V. Anufriyev. An algorithm of search for proofs of theorems in logical calculi.
     Theory of Automata, GIC AS UkrSSR, Kiev, 3-26, 1969. In Russian.
[16] A. I. Malashonok. The soundness and completeness of the Evidence Algorithm.
     Computer-Aided Theorem Proving in Mathematics, GIC AS UkrSSR, Kiev, 75-95,
     1974. In Russian.
[17] S. Kanger. Simplified proof method for elementary logic. Comp. Program. and Form.
     Sys., 87–93, 1963.
[18] A. I. Degtyarev and A. V. Lyaletski. Logical inference in the system for automated
     deduction, SAD. Mathematical Foundations of Artificial Intelligence Systems, GIC
     AS UkrSSR, Kiev, 3-11, 1981. In Russian.


Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
              Mathematical Text Processing in EA-style: a Sequent Approach            ·     263

[19] A. Degtyarev, A. Lyaletski, and M. Morokhovets. Evidence algorithm and se-
     quent logical inference search. LNAI (Proceedings of the International Conference
     LPAR’99), 1705: 44–61, 1999.
[20] A. Lyaletski and A. Paskevich. Goal-driven inference search in classical propositional
     logic. Proc. International Workshop STRATEGIES’2001, Siena, Italy, 65–74, 2001.
[21] T. Skolem. Logisch-kombinatorische Untersuchungen uber die Erfullbarkeit oder Be-
     weisbarkeit mathematischer Satze. Skriftner utgit ar Videnskapsselskaper i Kristia-
     nia, 4: 4-36, 1920.
[22] J. Herbrand. Recherches sur la theorie de la demonstration. Travaux de la Societe des
     Sciences et de Lettres de Varsovie, Class III, Sciences Mathematiques et Physiques,33,
     1930.
[23] G. Gentzen. Untersuchungen uber das logische schliessen (I, II). Math. Zeit., 39:
     176–210, 405–443, 1934.
[24] J. A. Robinson and A. Voronkov, editors. Handbook of Automated Reasoning (in 2
     volumes), Elsevier and MIT Press, 2001.
[25] R. Hahnle. Tableaux and related methods. Handbook of Automated Reasoning (Edited
     by A.Robinson and A.Voronkov), Elsevier Science Publishers, 101-178, 2001.
[26] A. Degtyarev and A. Voronkov. Equality reasoning and sequent-based calculi. Hand-
     book of Automated Reasoning (Edited by A.Robinson and A.Voronkov), Elsevier Sci-
     ence Publishers, 609-704, 2001.
[27] R. Nieuwenhuis and A. Rubio A. Paramodulation-based theorem proving. Handbook
     of Automated Reasoning (Edited by A.Robinson and A.Voronkov), Elsevier Science
     Publishers, 371-444, 2001.
[28] R. Letz and G. Stenz. Model elimination and connection tableau procedures. Hand-
     book of Automated Reasoning (Edited by A.Robinson and A.Voronkov), Elsevier Sci-
     ence Publishers, 2017–2116, 2001.
[29] A. Voronkov. Proof search in intuitionistic logic based on constraint satisfaction and
     related complexity problems. L.J. of the IGPL, Oxford University Press, 1996.
[30] W. Bibel. Automated Theorem Proving. Vieweg Verlag, 1987.
[31] L. Wallen. Automated proof search in non-classical logics., Oxford University Press,
     1990.
[32] J. Otten and C. Kreitz. Connection-based theorem proving in classical and non-
     classical logics. J. UCS, 5(3): 88–112, 1999.
[33] J. Otten and C. Kreitz. A connection based proof method for intuitionistic logic.
     Lecture Notes in Computer Science, 918: 122–137, 1995.
[34] J. Otten and C. Kreitz. A uniform proof procedure for classical and non-classical
     logics. Lecture Notes in Computer Science,1137: 307–319, 1996.
[35] A. Waaler and L. Wallen. Tableaux for intuitionistic logics, Handbook of Tableau
     Methods, 255-296, 1999.
[36] A. Waaler and R. Antonsen. A free variable sequent calculus with uniform variable
     splitting, Lecture Notes in Computer Science, 2796: 214–229, Springer, 2003.
[37] A. Lyaletski. Variant of Herbrand theorem for formulas in prefix form. Cybernetics,
     1: 12–116, 1981. In Russian.
[38] B. Konev and A. Lyaletski. Tableau proof search with admissible substitutions. Pro-
     ceedings of the International Workshop on First-order Theorem Proving, Koblenz,
     Germany, 35-50, 2005.


                                            Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
264     ·      Alexander Lyaletski

[39] O. Hiroakira. Proof-theoretic methods in non-classical logic — an introduction. The-
     ories of Types and Proofs (M. Takahashi and M. Okada and M. Dezani-Ciancaglini,
     Eds.), Mathematical Society of Japan, Tokyo, 207-254, 1998.
[40] J. Robinson. A machine-oriented logic based on resolution principle, J. of the
     ACM, 12(1): 23-41, 1965.
[41] G. Mints. Herbrand theorem. Mathematical Theory of Logical Inference, 311-350,
     Nauka, Moscow, 1967. In Russian.
[42] J.H. Gallier. Logic for Computer Science: Foundations of Automatic Theorem Prov-
     ing, Harper & Row, 1986.
[43] S. Autexier, H. Mantel, and W. Stephan. Simultaneous quantifier elimination,
     Lecture Notes in Computer Science, 1504: 141-152, 1998.
[44] M. Baaz and R. Iemhoff. The Skolemization of existential quantifiers in intu-
     itionistic logic, Annals of Pure and Applied Logic, 142 (1): 269–295, 2006.
[45] B.B. Lewis. Decidable Fragments and Skolemization in Superintuitionistic and
     Modal Logics, Undergraduate Honors Thesis, Stanford University, 2012.
[46] A. Lyaletski.: Sequent forms of Herbrand theorem and their applications. An-
     nals of Mathematics and Artificial Intelligence, 46(1-2): 191–230, Springer,
     2006.
[47] A. Lyaletski. On some problems of efficient inference search in first-order
     cut-free modal sequent calculi. Proceeding of the International Symposium
     SYNASC 2008, 39-46, 2008.




Journal of Formalized Reasoning Vol. 9, No. 1, 2016.
