
\documentstyle[10pt]{article}
\hsize=13.5cm
\vsize=18.5cm
%\title{\bf PARALLEL DEDUCTION-SEARCH ALGORITHM FOR THE PREDICATE LOGIC FORMULAS}
%\author{S.Norgela (VU)}
\begin{document}
%\begin{verse}
%{\scriptsize Lietuvos matematik\c{u} draugijos mokslo darbai, III tomas, 1999\\
%\copyright MII}
%\end{verse}
%\vspace{5mm}
%\begin{center}
\title{Parallel deduction-search algorithm for the\\ predicate logic formulas}
%\vspace{5mm}
\author{S.Norg\.{e}la (VU)\\
e-mail: Stasys.Norgela@maf.vu.lt}
%\end{center}
\date{}
\maketitle
\begin{abstract}
We consider the deductions of the first-order predicate logic formulas. We consider parallel
a derivation by resolution method of the empty clause from the set of clauses corresponding 
to the formula 
{\em F} and a derivation by inverse method of the empty disjunction from the set of disjuncts
corresponding to the formula $\neg F$.\\
    The relation is considered between derivable clauses and favorable disjuncts. One shows which
clauses are superfluous in the search of a derivation by resolution method of the empty clause in
 according with the obtained favorable disjuncts of the some form. We use search-proof
of empty disjunct as an auxiliary result for the diminuation of the set of derivable clauses.
The set is nonmonotonic.\\
   {\bf Key words:} first-order logic, parallel algorithm, deduction-search.
\end{abstract}
\vspace{5mm}
{\bf 1. Introduction}\\

Considering the deduction of the first-order predicate logic formula $\neg F$ on the basis
 of inverse method. Formula {\em F} is in the prenex normal form and its matrix 
(quantifier-free formula) is in the disjunctive normal form. We form the set {\em M(i)} 
of such favorable unit disjunctions, that they are derivable at the moment {\em i}.
We consider in parallel a derivation of {\em F} on the basis of the resolution method
with the following resolution rule \[\frac{\sigma C_{1}, \sigma C_{2}: M(i)}{\sigma C}\]
{\em M(i)} plays the role of the set of the justifications formulas at the moment {\em i}.
The application of the rule has been based on the restrictions on the choice of substitution.
The rule is applicable if such substitution $\gamma$ and formula $\rho C_{1} \in M(i)$ that
$(\gamma \circ \rho) C_{1}$ absorb $\sigma C$ do not exist at the moment.\\

The realization of some systems of the inverse method have shown that, if the derivation 
of an empty disjunct is obtained after the step {\em n} and {\em m} unit favorable
disjuncts are obtained during the process, then the majority of unit favorable disjuncts
are obtained not more than after steps ${\em n}/4$ for almost all formulas. So, most of the unit
favorable disjuncts are obtained rather quickly. They are used in order to show which
 clauses are useless.\\

The deduction in sequential calculus with the following rules is simulated by the deduction
based on the inverse method:
\[(\vdash \&)\hspace{15mm} \frac{\vdash \Gamma, F_{1}, \Delta \hspace{5mm} \vdash \Gamma,
F_{2}, \Delta \ldots \vdash \Gamma, F_{n}, \Delta}{\vdash \Gamma, \&^{n}_{i=1} F_{i}, \Delta}\]\\

\[(\vdash \vee) \hspace{20mm} \frac{\vdash \Gamma, F_{1}, F_{2},\ldots, F_{n}, \Delta}
{\vdash \Gamma, \vee^{n}_{i=1} F_{i}, \Delta}\]\\

\[(\vdash \exists) \hspace{20mm} \frac{\vdash \Gamma, \sigma F, \exists x_{1} \ldots
\exists x_{n}, \Delta}{\vdash \Gamma, \exists x_{1} \ldots \exists x_{n}, \Delta}\]\\

$\sigma$ is a substitution satisfying usually restrictions.\\
The inverse method is presented in many divers papers (see, for example [1]).\\

We can easy construct the deduction based on the inverse method of the empty disjunct $\Box$
in accordance with the deduction tree of the sequent $\vdash F$ in considerable sequential
calculus and on the contrary (see [1]). We denote the unit favorable disjuncts ${\em [i, B]}$
 by $\sigma C_{i}$, where $\sigma$ denotes the substitution corresponding to {\em B}.\\

\vspace{5mm}
{\bf 2. Basic result}\\

{\bf Theorem 1}. {\em If} $\sigma_{j} D_{k}$ {\em is derivable by inverse method then it
belongs to the set of superfluous clauses M.}\\

{\em Proof}. Let $\vdash \sigma C$ is derivable by inverse method. It means that if $\sigma C$ is in
some branch of the proof-search tree, then we are able to extend this branch of the tree
 started from $\sigma C$ to the axioms. We consider only the saturated formulas of the form
$F=D_{1} \& D_{2} \& \ldots \& D_{s}$ where $D_{j}$ are disjuncts, i.e. such formulas as
any atomic formula {\em F} or its negation occur in each disjunct. More precisely we consider
the matrix of {\em F} which does not contain function symbols before Skolemization.
Then $\neg F= F'=D' \& D'' \& \ldots \& D^{p}$. This is all of the remaining disjuncts,
which we can obtain from atoms occurred in {\em F} i.e. the formula $F \& F'$ contains all
possible disjuncts formed from the initial formula. We construct the following formula
 according to the deduction tree in sequent calculus.\\

\[(\sigma_{1} D_{1} \& \sigma_{1} D_{2} \& \ldots \& \sigma_{1} D_{s}) \vee \ldots
\vee (\sigma_{j} D_{1} \& \sigma_{j} D_{2} \& \ldots \& \sigma_{j} D_{s}) \vee \ldots\]
\[\ldots \vee (\sigma_{l} D_{1} \& \sigma_{l} D_{2} \& \ldots \& \sigma_{l} D_{s})
\hspace{15mm}(1)\]\\

Each application of the rule $(\vdash \exists)$ is met in the tree correspond to any formula\\

\[(\sigma_{u} D_{1} \& \sigma_{u} D_{2} \& \ldots \& \sigma_{u} D_{s})\]\\

Assume $\vdash \sigma_{j} D_{k}$ is derivable by inverse method. Then (1) is a valid formula
if and only if\\

\[(\sigma_{1} D_{1} \& \sigma_{1} D_{2} \& \ldots \& \sigma_{1} D_{s}) \vee \ldots
\vee (\sigma_{j} D_{1} \& \ldots 
\&  \sigma_{j} D_{k-1} \& \sigma_{j} D_{k+1} \& \ldots \& \sigma_{j} D_{s}) \vee \ldots\]
\[\ldots \vee (\sigma_{l} D_{1} \& \sigma_{l} D_{2} \& \ldots \& \sigma_{l} D_{s})
\hspace{15mm}(2)\]\\
is valid.\\
It means the negation of (2)\\

\[\neg (\sigma_{1} D_{1} \& \sigma_{1} D_{2} \& \ldots \& \sigma_{1} D_{s}) \& \ldots
\& \neg (\sigma_{j} D_{1} \& \ldots \]
\[ \ldots \&  \sigma_{j} D_{k-1} \& \sigma_{j} D_{k+1} \& \ldots \& \sigma_{j} D_{s}) \& \ldots\]
\[\ldots \& \neg (\sigma_{l} D_{1} \& \sigma_{l} D_{2} \& \ldots \& \sigma_{l} D_{s})\]\\
is equivalent with\\

\[\sigma_{1} F' \& \sigma_{2} F' \& \ldots \& (\sigma_{j} F' \& \sigma_{j} D_{k}) \&
\ldots \& \sigma_{l} F' \hspace{10mm}(3)\]\\

The previous formula is equivalent and with negation of (1) i.e.\\

\[\sigma_{1} F' \& \sigma_{2} F' \& \ldots \& \sigma_{j} F' \& 
\ldots \& \sigma_{l} F' \hspace{15mm}(4)\]\\

We have obtained that (3) is a contradictory formula if and only if (4) is a
contradictory formula.\\

{\bf Definition.} {\em The favorable disjunct $[i_{1}, i_{2}, \ldots, i_{u}, j_{1},
j_{2}, \ldots , j_{l} ; B]$ is decomposable into $[i_{1}, i_{2}, \ldots, i_{u}; B']$
and $[j_{1}, j_{2}, \ldots , j_{l} ; B'']$ if the variables of disjuncts
$ i_{1}, i_{2}, \ldots, i_{u}$ have no occurences in any set of basis B with any variable
of disjuncts $j_{1}, j_{2}, \ldots , j_{l}$, except the case when any constant belong to
considerable set.}\\

Detailed description of the formation of basis {\em B'} and {\em B''} is in [2].\\

{\bf Theorem 2.} {\em If we obtain any disjunct $[i_{1}, i_{2}, \ldots, i_{u}; B]$ 
decomposable into unit favorable disjuncts in the proof search of $\Box$ by the inverse
method from the set of initial disjuncts correponding to $\neg F$ and we obtain the
clauses $\sigma_{l} D_{j} (l=1,\ldots, u; j=i_{1}, i_{2},...,i_{u}$; the substitutions
$\sigma_{l}$ are correspondence of the unit favorable disjuncts) in the proof search of
$\Box$ by resolution method from the set of initial clauses corresponding to F, then
$\Box$ is derivable by resolution method not using any clause from $\sigma_{l} D_{j}$.}\\

{\em Proof}. We can use only such replacements of variables that transpose of rules, 
that become permissible (after rename of certain variables) in the deduction tree of the 
formula $\neg F$ in sequential calculus. It means we can obtain that the unit considerable
 disjunct $\sigma_{l} D_{j}$ becomes the final node in the branch. Because we are able to
prolong considerable node until axioms, then we can delete the formula corresponding
 to final node in (2) i.e. $\sigma_{l} D_{j}$ belong to the set {\em M} of superfluous
disjuncts. Theorem is proved.\\

We can enumerate certain decidable classes without functional symbols. Favorable
disjuncts derivable from formulas of following classes decompose into unit favorable
disjuncts.\\

 \begin{enumerate}
\item Monadic class (see [2]).
\item G\H{o}del class. This is the formulas in prenex normal form with prefix
$\exists x_{1} \exists x_{2} \forall y_{1} \forall y_{2} \ldots \forall y_{l}$ (see[2]).
\item The formulas in prenex normal form with matrix $P_{1} \vee P_{2} \vee \ldots
\vee P_{n} \vee M$, where $P_{j}$ are literals containing no much as one negative
variable and {\em M} is formula containing only positive occurrences of variables
(see [3]).
\end{enumerate}

Remember that favorable disjuncts decompose into unit of not all decidable classes.\\

\vspace{5mm}
{\bf 3. The case of monadic class.}\\
 
Consider the closed formulas with monadic predicate variables in prenex normal form.
Matrix is in conjunctive normal form i.e. we consider the formulas of the form
$Q_{1} x_{1} Q_{2} x_{2} \ldots Q_{n} x_{n} G$, where the $Q_{i} (i=1,...,n)$ are 
quantifiers, {\em G} is quantifier-free formula in conjunctive normal form.\\

We will show that there exists equivalent formula of the form\\
 $\exists x_{1} \ldots
\exists x_{k} \forall y_{1} \ldots \forall y_{l} H$ ({\em H} is quantifier-free formula)
for any formula {\em F}. Search of such formula require much time. I would like to
accentuate that one can consider only such formulas and this is a general form of the case 
of formulas with monadic predicate variables.\\

{\bf Theorem 3.} {\em Let F be a formula of monadic class. Then there exists equivalent
formula of the form\\
$\exists x_{1} \ldots \exists x_{k} \forall y_{1} \ldots \forall y_{l} G \hspace {10mm}$\\
where G is in conjunctive normal form.}\\

{\em Proof}. Consider the prenex normal form of {\em F}
 $Q_{1} x_{1} Q_{2} x_{2} \ldots Q_{m} x_{m} H$, where the {\em H} is in conjunctive
normal form, and $Q_{i}=\forall$ or $Q_{i}=\exists (i=1,...,m)$. Consider two cases,
when $Q_{m}=\forall$ and when $Q_{m}=\exists$.\\
\begin{itemize}
\item Let $Q_{m}=\forall$. Bring $\forall x_{m}$ in the brackets using equivalence
$\forall y_{m} (P \& R) \equiv \forall x P \& \forall x R$ i.e. $\forall x_{m}$ is only
immediate before elementary disjunction. Then if formula does not contain $x_{m}$ we use
the equivalence $\forall x_{m} (P \vee R) \equiv \forall x_{m} P \vee R$.
\item Let $Q_{m}=\exists$. Transform {\em H} into disjunctive normal form. Bring
$\exists x_{m}$ in the brackets using equivalence $\exists x_{m} (P \vee R) \equiv
\exists x_{m} P \vee \exists x_{m} R$ i.e. $\exists x_{m}$ is only immediate before elemetary conjunction.
Then if formula {\em R} does not contain $x_{m}$ we use equivalence
 $\exists x_{m} (P \& R) \equiv \exists x_{m} P \&  R.$
\end{itemize}
We apply {\em m} time described method and a disjunction of the formulas of the following
form is obtained in this way (may be still after the transformation into disjunctive normal
form)\\
 
\[R^{j}_{1} \& R^{j}_{2} \& \ldots R^{j}_{v}\]
Where $R^{j}_{l} (l=1,...,v)$ is a formula of the form\\
$\forall y (P^{u}_{1} (y) \vee P^{u}_{2} (y) \vee \ldots \vee P^{u}_{r} (y))$
(where $P^{u}_{i} (y)$ are literals) or\\
 $\exists x (S^{j}_{1} (x) \& S^{j}_{2} (x) \&
\ldots \& S^{j}_{l} (x))$ (where $S^{j}_{l}(x)$ are literals). More forward
 quantifier $\exists$ (the number of quantifiers may be increase with respect to initial
formula). We obtain the formula $\exists x_{1} \ldots \exists x_{k} L$. Transform {\em L}
 into conjunctive normal form and then bring all quantifiers $\forall$ in front of the
 formula (the number of quantifiers may be increase again). Because we transform using
equivalent formula then the obtained formula $\exists x_{1} \ldots \exists x_{k}
\forall y_{1} \ldots \forall y_{l} G$ is equivalent to initial {\em F}. Theorem is proved.\\

We want to verify a formula {\em F} of the form (5) is an unsatisfiable formula.
For this reason we search deduction by resolution method of empty clause using the
default rule from the set of clauses corresponding to {\em F}. We search at the same
time parallel deduction by inverse method of empty clause from the set of clauses
correponding to $\neg F$ (it means we try to verify the considerable formula is valid) and
we form the set of justifications.\\
{\em G} is in conjunctive normal form i.e. of the form $D_{1} \& D_{2} \& \ldots \&
D_{s}$ (where $D_{i}$ are clauses). We obtain \\
$\sigma \forall y_{1} \ldots \forall y_{l} (D_{1} \& D_{2} \& \ldots \& D_{s}$ after
the Skolemization of (5). $\sigma$ is the substitution
 $(a_{1}/x_{1}, a_{2}/x_{2},..., a_{m}/x_{m})$ i.e. we will have a set of clauses\\
$S=\{ D'_{1}, D'_{2},...,D'_{s} \}$ (where $D'_{i}=\sigma D_{i}$). We will search
 a deduction of the formula $\neg F$ i.e. of the $\forall x_{1}...\forall x_{k}
\exists y_{1} ... \exists y_{l} \neg G$. It means we will search a deduction of the
formula $\sigma \exists y_{1} ... \exists y_{l} \neg G$ with the same substitution\\
$\sigma = (a_{1}/x_{1}, a_{2}/x_{2},..., a_{m}/x_{m})$.\\

\begin{center}
{\bf REFERENCES}
\end{center}
\vspace{5mm}
1.S.Yu.Maslov, The inverse method for establiching deducibility in the classical
predicate calculus, {\em Soviet Mathematics Doklady}, 5, 1420-1424(1964).\\
2.S.Yu.Maslov, The inverse method of establiching deducibility for logical
calculi, {\em Proceedings of the Steklov Institute of Mathematics},98, 25-96(1971).\\
3.S.Norgela, On approximation of some classes of the classical predicate calculus
by decidable classes II, {\em Lithuanian Journal of Mathematics}, 20(4), 89-96(1980).\\

{\bf Lygiagretus \c{i}rodymo paie\v{s}kos algoritmas predikat\c{u} logikos formul\.{e}ms}\\
\begin{center}
{\em S.Norg\.{e}la}\\
\end{center}

Pirmos eil\.{e}s 
formul\.{e}s i\v{s}vedimas ie\v{s}komas rezoliucij\c{u} metodu, o jos neigimas
lygiagre\v{c}iai atvirk\v{s}tiniu metodu. Nagrin\.{e}jamas ry\v{s}ys tarp gaunam\c{u}
disjunkt\c{u}. 
 
\end{document}
