\documentclass[twocolumn,11pt]{article}
\usepackage{times}
\usepackage{amsmath}     %von mir hinzugefuegt
\usepackage{tikz}        %von mir hinzugefuegt
%
% DO NOT CHANGE THE FOLLOWING PART
%
\setlength{\textwidth}{6.9in}
\setlength{\textheight}{9.5in}
\setlength{\oddsidemargin}{-0.25in}
\setlength{\evensidemargin}{-0pt}
\setlength{\topmargin}{-0.25in}
\setlength{\columnsep}{0.4in}
\setlength{\parindent}{4ex}
%
\newtheorem{definition}{Definition}
\newtheorem{remark}[definition]{Remark}
\newtheorem{lemma}[definition]{Lemma}
\newtheorem{theorem}[definition]{Theorem}
\newtheorem{proposition}[definition]{Proposition}
\newtheorem{corollary}[definition]{Corollary}
%
%
% THIS IS THE PLACE FOR YOUR OWN DEFINITIONS
%
\newcommand{\R}{{\rm I}\!{\rm R}} % the set of real numbers
% boldface characters in mathematical formulas
\newcommand{\bff}{\mbox{\boldmath $f$}}
\newcommand{\bfl}{\mbox{\boldmath $l$}}
\newcommand{\bfn}{\mbox{\boldmath $n$}}
\newcommand{\bfu}{\mbox{\boldmath $u$}}
\newcommand{\bfx}{\mbox{\boldmath $x$}}
\newcommand{\bfy}{\mbox{\boldmath $y$}}
\newcommand{\bfzero}{\mbox{\boldmath $0$}}
\newcommand{\bfcurl}{{\bf curl}} % curl of a vector field
\newcommand{\rmdiv}{{\rm div}} % divergence of a vector field
\newcommand{\eop}{\hfill $\sqcap\!\!\!\!\sqcup$} % end of proof
%
% Meine Definitionen:
% result of replacing every free occurrence of #1 with #2
\newcommand{\rep}[2]{{}^{#1}_{#2}}
% rule of a Frege-Hilbert calculus
\newcommand{\regel}[2]{\dfrac{#1}{#2}}
% name of the constraint for rule #1
\newcommand{\constraint}[1]{C\ref{#1}}
% if constraint for rule #1
\newcommand{\ifconstraint}[1]{\rlap{\qquad if C\ref{#1}}}
% definition of constraint for rule #1
\newcommand{\defconstraint}[1]{\mbox{\constraint{#1}:}\qquad}
%
%
%
% THE BEGINNING OF THE DOCUMENT
%
\begin{document}
\global\def\refname{{\normalsize \it References:}}
%
\baselineskip 12.5pt
%
%
% TITLE, AUTHOR, ABSTRACT, KEYWORDS
%
\title{\LARGE \bf Automated Deduction in Frege-Hilbert Calculi}

\date{}

\author{\hspace*{-10pt}
\begin{minipage}[t]{2.7in} \normalsize \baselineskip 12.5pt
\centerline{ELMAR EDER}
\centerline{University of Salzburg}
\centerline{Department of Computer Sciences}
\centerline{Jakob-Haringer-Str. 2}
\centerline{AUSTRIA}
\centerline{eder@cosy.sbg.ac.at}
\end{minipage}
%
%
\\ \\ \hspace*{-10pt}
\begin{minipage}[b]{6.9in} \normalsize
\baselineskip 12.5pt {\it Abstract:}
% The text of the abstract follows.
In this paper the appropriateness of Frege-Hilbert calculi and other
cut calculi for automated deduction is discussed. Unification of
formula schemes and composition of rules of Frege-Hilbert calculi
lead to proof systems which may be suited for automation.
%
\\ [4mm] {\it Key--Words:}
% The key-words follow.
Automated deduction, Frege-Hilbert calculi, Composition of rules, Cut rule
\end{minipage}
\vspace{-10pt}}

\maketitle

\thispagestyle{empty} \pagestyle{empty}
% numbers of pages are supplemented by the editor
%
% THE BEGINNING OF THE TEXT
%
\section{Introduction}
\label{int} \vspace{-4pt}

In this paper we give a brief account of some results on automated
deduction in Frege-Hilbert calculi using the operation of composition
of rules. We restrict ourselves to classical first order predicate
logic with or without function symbols. Whereas there are many
successful systems for automated deduction in resolution and in
systems related to backward reasoning in cut-free sequent calculi
(connection method, tableau calculus), automated reasoning in
Frege-Hilbert calculi or generally in proof systems with the cut rule
is much more difficult. For a long time it seemed to be entirely
impossible because in each proof step rules can be applied in an
infinite number of possible ways making automatic proof search a
nightmare. On the other hand, resolution and cut-free calculi are
hopelessly inefficient even in terms of shortest possible proofs (not
even regarding the problem of finding the proof) for some classes
formulas. Also, cut is a natural tool used by humans when reasoning
and so should be used in automated reasoning too.

In conventional automated deduction, a proof is constructed by
constructing the formulas of a proof tree one by one. This cannot be
done efficiently in calculi with cut. However, it is possible to
construct formula schemes and compositions of rules of the calculus
and later instantiate them to obtain the final proof. So the proof
procedure proposed in this paper has as its inference rule the
operation of composition of rules of the Frege-Hilbert calculus.  In
this way it is possible to obtain a proof, for example in a
Frege-Hilbert calculus, without having to choose from an infinite
number of possibilities in a single proof step.


\section{Calculi With Cut and Calculi Without Cut}
\label{sec:cut} \vspace{-4pt}


The first formulation of a language of full first order predicate
logic given in the history of logic was Gottlob Frege's
Begriffsschrift \cite{Fre1879} (concept language) in 1879. In his
Begriffsschrift, Frege also provided a proof calculus which was later
proved to be sound and complete when restricted to what we now call
first order predicate logic. Frege's idea was to provide a set of
\emph{axioms} which are formulas known to be valid, and a set of
\emph{rules} to derive new valid formulas from formulas which have
already been derived. Similar calculi were introduced and investigated
to a great extent by David Hilbert and others.

Here is a typical Frege-Hilbert calculus with four axiom schemes
\begin{gather}
  A\to B\to A\label{A1}\\[1ex]
  (A\to B\to C)\to(A\to B)\to A\to C\label{A2}\\[1ex]
  (\lnot A\to\lnot B)\to B\to A\label{A3}\\[1ex]
  \forall xF\to F\rep xt\label{A4}
\end{gather}
and two rules
\begin{gather}
  \regel{A\qquad A\to B}{B}\label{R1}\\[2ex]
  \regel{A\to F\rep xp}{A\to\forall xF}\label{R2}
\end{gather}
where ``$F\rep xt$'' denotes the result of replacing every free
occurrence of the variable $x$ in the formula $F$ with the ground term
$t$. The symbol $p$ in the last rule is called a \emph{parameter}. It
is subject to the constraint that $p$ must not occur in the conclusion
$A\to\forall xF$. Rule (\ref{R1}) is called \emph{modus ponens}. An
axiom scheme can be considered as a rule with no premise.

Even nowadays most proof calculi used by logicians for classical as
well as non-classical logic are of the Frege-Hilbert type. The reason
for this is that Frege-Hilbert calculi have a simpler syntactic
structure than some of the calculi introduced later and yet are very
powerfull for expressing proofs of logical formulas.

On the other hand, Frege-Hilbert calculi are difficult to use for
automated deduction. If you want to prove some given formula, it would
be very inefficient to construct the proof in a forward way, randomly
producing axioms and trying to use the rules to derive conclusions
from them until you get the formula you wanted to prove. Rather, the
more obvious way would be to use backward reasoning. You start from
the formula you want to prove and apply the rules backward until all
your premises are axioms. The problem with this idea is that a
backward application of modus ponens is not unique.
If you want to prove a formula $B$ with modus ponens, you have to
guess the formula $A$, and there are an infinite number of
possibilities what $A$ could be. An automated system would be
completely lost. This problem appears in a Frege-Hilbert calculus
whenever there is a rule with a formula $A$ occurring in at least one
of the premises but not occurring in the conclusion. Such a rule is
called a \emph{cut rule} and the formula $A$ is called a \emph{cut
  formula}. Unfortunately, there is no sound and complete
Frege-Hilbert calculus which does not have a cut rule.

In the history of logic, cut rules caused a headache to logicians for
similar reasons when they wanted to prove the consistency of logical
calculi long before the advent of modern computers and thus long
before the birth of automated deduction. In 1935 Gerhard Gentzen
introduced his \emph{sequent calculus} \cite{Gentz35} in a version
with cut rule and a version without cut rule. The sequent calculus is
similar to Frege-Hilbert calculi but uses the data structure of a
sequent (of formulas) instead of formulas. So you prove a sequent of
formulas rather than proving a formula. Gentzen showed that in his
calculus applications of the cut rule can be eliminated. A proof with
cut can be transformed to a proof without cut. The cut-free version of
Gentzen's sequent calculus can be used for \emph{analytic} backward
reasoning. This means that the backward reasoning (backward
application of rules) amounts to decomposing (analyzing) the given
formula rather than guessing a cut formula.

There are a number of calculi and proof systems derived from Gentzen's
sequent calculus. One of them is Wolfgang Bibel's \emph{connection
  method} \cite{Bibel87}.
Another one is Beth's and Smullyan's \emph{tableau calculus}
\cite{Beth55,Beth59,Smull71}. Both of them
can be viewed as refinements of the sequent calculus with the use of
structure sharing techniques. All these calculi are characterized by a
rather directed proof search.

The calculus most often used for automated deduction is the
\emph{resolution calculus} \cite{Robin65} introduced in 1965 by
J.~A.~Robinson. It works by proving the unsatisfiability of a formula
in conjunctive normal form. It is characterized by a particularly
simple deduction rule, the \emph{resolution rule}, and works by
deriving new clauses from a given set of clauses until an empty clause
is derived, indicating a contradiction. In resolution it is more
difficult to get a well directed proof search than in calculi based on
the sequent calculus.

Unfortunately, cut elimination may be extremely expensive, as
R.~Statman \cite{Statm79} and V.~P.~Orevkov \cite{Orevkov:1979} have
shown. More precisely, there is a sequence $(F_n)$ of formulas and a
polynomial $p$ such that each $F_n$ has a proof of length $\le p(n)$
in the full sequent calculus, but the shortest proof of $F_n$ in the
cut-free sequent calculus has length
$\ge\underbrace{2^{2^{\dots^{2^2}}}}_{n\text{ times}}$. Moreover,
these formulas are not just some academic examples but formulas from
combinatory logic which may very well occur in the everyday life of a
logician or of a computer scientist. As a consequence, for these
formulas even a stupid generation of all possible finite sequences of
formulas and testing whether they are proofs in the full sequent
calculus would be more efficient than even the most clever proof
search in the cut-free sequent calculus.

This result of Statman and Orevkov carries over to all calculi based
on the cut-free sequent calculus including the connection method and
the tableau calculus, and also to some other calculi such as the
resolution calculus. Some of these calculi can be extended to allow
something similar to a cut rule. For example, the tableau calculus can
be extended by allowing a case distinction between $A$ and $\lnot A$
where $A$ is some arbitrary formula. This amounts to the same thing as
the cut rule in the sequent calculus. However, again this destroys the
analytic character of the calculus. An automated deduction system
would have the same problem guessing the formula $A$ as in the full
sequent calculus. Even for a human mathematician it is often hard to
decide how to make a case distinction, i.e., which formula $A$ to
choose. However, as every mathematician knows, case distinction is a
very powerful tool in mathematical theorem proving. Therefore we
should try hard to find ways to also employ case distinction or a cut
rule in systems of automated deduction.



\section{Construction of a Proof}
\label{sec:pro} \vspace{-4pt}

Since Frege-Hilbert calculi are syntactically comparatively simple, it
seems that for a theoretical investigation of possible proof systems
with cut the Frege-Hilbert calculi would be a good start. Of course,
for a later practical system the full sequent calculus and systems
based on it seem to be more adequate, since the sequence calculus is
complete also without cut and therefore a well dosed sparse
application of cuts is possible there.

So let us consider the Frege-Hilbert calculus given at the beginning
of section~\ref{sec:cut} again. One idea how to deal with a cut rule
such as modus ponens is not to guess the cut formula $A$ but to leave
the symbol ``$A$'' there instead and to continue applying rules
backwards.  Assume, for example, that we want to prove the formula
$P(a)$. If we try to do this with the modus ponens, we get the
premises $A$ and $A\to P(a)$. At this point we do not know yet which
formula the symbol ``$A$'' is going to stand for.  The decision which
formula ``$A$'' is to stand for is postponed until later. The same
technique is used by automated deduction calculi on the level of terms
rather than formulas. There a term is determined by \emph{unification}
(or equation solving). For our purpose we need unification of formulas
in addition to unification of terms.

The symbol ``$A$'' can be viewed as a meta-symbol standing for a
formula. Similarly we have meta-symbols for terms, variables, and
parameters. Since we have meta-symbols such as ``$A$'' during our
deduction process, we do not only deal with formulas. Rather we deal
with \emph{formula schemes}. A formula scheme is the result of
replacing within a formula some subformulas or terms with adequate
meta-symbols.

Now, backward reasoning in a Frege-Hilbert system (with cut) can be
done as follows. We start with the formula to be proved. Then we apply
rules of the calculus in a backward direction, in each step replacing
the conclusion of the rule application with the premises. In each
step, a formula scheme (the conclusion of the rule application) is
replaced with zero or more new formula schemes (the premises of the
rule application). Since axiom schemes are rules with zero premises,
our proof is finished when no formula schemes are left.

Actually, the premises and the conclusion of a rule of a Frege-Hilbert
calculus are formula schemes. It turned out \cite{eder:backw} that two
rules $R_1$ and $R_2$ of a Frege-Hilbert calculus can be composed to
give a new rule $R$ such that $H$ is the conclusion of an instance of
$R$ with premises $G_1,\dots,G_{k-1},F_1,\dots,F_m,G_{k+1},\dots,G_n$
if and only if there is a formula $G_k$ such that $G_k$ is the
conclusion of an instance of $R_1$ with premises $F_1,\dots,F_m$ and
$H$ is the conclusion of an instance of $R_2$ with premises
$G_1,\dots,G_n$. Composition of rules can be depicted in a way similar
to composition of components of an electric circuit:
\begin{center}
  \begin{tikzpicture}[scale=0.4]
    \draw[ultra thick] (6,3.6) rectangle (12,6);
    \foreach \x in {7,11} {\draw (\x,6) -- +(0,1);}
    \foreach \x/\n in {7/F_1,9/\dots,11/F_m} {\draw (\x,5.3) node {$\n$};}
    \draw (9,4.2) node {$G_k$};
    \draw (9,3.6) -- (9,2.4);
    \foreach \x in {1,5,13,17} {\draw (\x,2.4) -- +(0,1);}
    \draw[ultra thick] (0,0) rectangle (18,2.4);
    \foreach \x/\n in
    {1/G_1,3/\dots,5/G_{k-1},9/G_k,13/G_{k+1},15/\dots,17/G_n} {\draw
      (\x,1.7) node {$\n$};}
    \draw (9,0.6) node {$H$};
    \draw (9,0) -- +(0,-1);
  \end{tikzpicture}
\end{center}
For example, a composition of the modus ponens rule with itself can be
depicted as
\begin{center}
  \begin{tikzpicture}[scale=0.4]
    \draw[ultra thick] (0,3.6) rectangle (7,6);
    \foreach \x in {1,5} {\draw (\x,6) -- +(0,1);}
    \foreach \x/\n in {1/A,5/A\to B} {\draw (\x,5.3) node {$\n$};}
    \draw (3.5,4.2) node {$B$};
    \draw (3.5,3.6) -- (3.5,2.4);
    \draw (8,2.4) -- +(0,1);
    \draw[ultra thick] (2.5,0) rectangle (10,2.4);
    \foreach \x/\n in
    {3.5/B,8/B\to C} {\draw
      (\x,1.7) node {$\n$};}
    \draw (6,0.6) node {$C$};
    \draw (6,0) -- +(0,-1);
  \end{tikzpicture}
\end{center}
which results in the rule
\begin{center}
  \begin{tikzpicture}[scale=0.4]
    \draw[ultra thick] (0,0) rectangle (12,2.4);
    \foreach \x in {1,5,10} {\draw (\x,2.4) -- +(0,1);}
    \foreach \x/\n in {1/A,5/A\to B,10/B\to C} {\draw (\x,1.7) node {$\n$};}
    \draw (6,0.6) node {$C$};
    \draw (6,0) -- +(0,-1);
  \end{tikzpicture}
\end{center}
or
\begin{equation*}
  \regel{A\qquad A\to B\qquad B\to C}{C}
\end{equation*}
for short.

The idea in computing the composition of two rules is to use a kind of
unification with meta-symbols. However, formula schemes and
unification alone do not suffice. Rather, some constraints have to be
added.

So we can go a step further and use the operation of composition of
rules in order to construct a proof tree. The proof tree can then not
only be constructed from its root. Rather we can start constructing
parts of the tree in various places somewhere in the middle of the
tree and later join them, again using the operation of composition of
rules.



\section{Composition of Rules}
\label{sec:com} \vspace{-4pt}

As a simple example to see how the composition of rules works in first
order predicate logic, let us look at a proof of the formula $\forall
xP(x)\to\forall yP(y)$ in our Frege-Hilbert calculus:
\begin{gather*}
  \forall xP(x)\to P(p)\\
  \forall xP(x)\to\forall yP(y).
\end{gather*}
In the first step we obtain $\forall xP(x)\to P(p)$ as an instance of
the axiom scheme (\ref{A4}). From this we derive $\forall xP(x)\to
P(y)$ by rule (\ref{R2}). Now let us compute the composition of rules
(\ref{A4}) and (\ref{R2}). First we observe that (\ref{A4}) and
(\ref{R2}) share the meta-symbols ``$F$'' and ``$x$''. Therefore we
standardize the two rules apart by renaming in (\ref{R2}) the
meta-symbol ``$F$'' to ``$G$'' and the meta-symbol ``$x$'' to ``$y$''
and we get
\begin{equation*}
  \regel{A\to G\rep yp}{A\to\forall yG}
\end{equation*}
Now, if an application of rule (\ref{A4}) is to be followed by an
application of this rule then $A=\forall xF$ and $F\rep xt=G\rep yp$
must hold. Also, the parameter $p$ must not occur in $A\to\forall yG$
and thus it must not occur in $F$ and not in $G$. We write $p\notin
FG$ for short. In summary, the composition of the rules (\ref{A4}) and
(\ref{R2}) is the axiom scheme (i.e.\ nullary rule)
\begin{equation*}
  \forall xF\to\forall yG
\end{equation*}
with the constraints $F\rep xt=G\rep yp$ and $p\notin FG$.

We can depict this process of composition of rules as follows.
\begin{center}
  \begin{tikzpicture}[scale=0.4]
    \draw[ultra thick] (0,3.6) rectangle (6,6);
    \draw (3,4.2) node {$\forall xF\to F\rep xt$};
    \draw (3,3.6) -- (3,2.4);
    \draw[ultra thick] (0,0) rectangle (6,2.4);
    \draw (3,1.7) node {$\forall xF\to G\rep yp$};
    \draw (3,0.6) node {$\forall xF\to\forall yG$};
    \draw (3,0) -- +(0,-1);
  \end{tikzpicture}
\end{center}
with the constraints $F\rep xt=G\rep yp$ and $p\notin FG$. The
constraint $F\rep xt=G\rep yp$ guarantees that the conclusion $\forall
xF\to F\rep xt$ of the application of rule (\ref{A4}) equals the
premise $\forall xF\to G\rep yp$ of the application of rule
(\ref{R2}). The resulting rule (axiom scheme) is depicted as
\begin{center}
  \begin{tikzpicture}[scale=0.4]
    \draw[ultra thick] (0,0) rectangle (6,2.4);
    \draw (3,0.6) node {$\forall xF\to\forall yG$};
    \draw (3,0) -- +(0,-1);
  \end{tikzpicture}
\end{center}
with the same constraints.

If we set $F=P(x)$ and $G=P(f(y))$ and $t=f(p)$ then we see that this
composition of rules also yields a proof of the formula
\begin{equation*}
  \forall xP(x)\to\forall yP(f(y)).
\end{equation*}
The proof is
\begin{gather*}
  \forall xP(x)\to P(f(p))\\
  \forall xP(x)\to\forall yP(f(y)).
\end{gather*}

The most general form of a rule obtained by repeated compositions of
rules of Frege-Hilbert calculi is
\begin{equation*}
  \regel{\Phi_1\quad\dots\quad\Phi_n}{\Psi}
\end{equation*}
together with a sequence $\mathcal{C}$ of constraints where
$\Phi_1,\dots,\Phi_n$ and $\Psi$ are formula schemes. Symbols such as
``$F\rep xt$'' and ``$F\rep xp$'' denoting the result of replacing a
variable with a term can be pushed into the constraints.  For example,
our Frege-Hilbert calculus can then be presented as follows.

\bigskip

\noindent
Axioms:
\begin{gather}
  A\to B\to A\label{a1}\\[1ex]
  (A\to B\to C)\to(A\to B)\to A\to C\label{a2}\\[1ex]
  (\lnot A\to\lnot B)\to B\to A\label{a3}\\[1ex]
  \forall xF\to E\ifconstraint{a4}\label{a4}
\end{gather}
In axiom scheme (\ref{a4}) there is a constraint
\begin{equation*}
  \defconstraint{a4} E=F\rep xt.
\end{equation*}
Rules:
\begin{gather}
  \regel{A\qquad A\to B}{B}\label{r1}\\[2ex]
  \regel{A\to E}{A\to\forall xF}\ifconstraint{r2}\label{r2}
\end{gather}
In rule (\ref{r2}) there is a constraint
\begin{equation*}
  \defconstraint{r2} E=F\rep xp, \quad p\notin AF.
\end{equation*}

Now the formula schemes occurring in the rules without their
constraints can be regarded as terms of a free term algebra with the
logical connectives and quantifiers as function symbols and the
meta-symbols as variables. Therefore the composition of two rules can
be computed with the usual technique of first standardizing apart and
then unifying the conclusion of the first rule with one of the
premises of the second rule. Finally, the sets of constraints have to be
merged.

If we look at the constraints \constraint{a4} and \constraint{r2} we
see that they do not contain any propositional connectives or
quantifiers. The formula schemes occurring in constraints of rules
have the form $\Gamma\rep{\xi\dots\zeta}{\mu\dots\nu}$ where $\Gamma$
is a meta-symbol for a formula, $\xi,\dots,\zeta$ are meta-symbols for
variables, and $\mu,\dots,\nu$ are meta-symbols for terms or
parameters. We call such a formula scheme an \emph{atomic formula
  scheme}. Constraints have always the form $\Phi=\Psi$ or
$\alpha\notin\Phi$ where $\Phi$ and $\Psi$ are atomic formula schemes
and $\alpha$ is a meta-symbol for a parameter.

Note that any set of such constraints has a solution. For example,
replacing all meta-symbols for formulas with one and the same
proposition symbol $P$ solves all possible constraints. Let us call a
composition of rules \emph{failed} if it has no instance. Then it
follows that a failure of a composition of rules is always accompanied
by a failure of the unification process, never by a failure of the
constraints. It can therefore easily be recognized.


\section{Conclusion}
\vspace{-4pt}

Automated deduction in proof calculi with a cut rule can be used to
prove formulas which have extremely long shortest proofs in cut-free
calculi and in resolution if suitable search strategies for proof
search can be found. The results stated in this paper show at least
that the problem of infinitely branching search trees can be overcome
by using unification on the formula level to compute compositions of
rules. A student at our department is currently implementing an
interactive and automatic deduction system based on composition of
rules in Frege-Hilbert calculi as his master's thesis. This deduction
system will be used for further investigation of rules and the
operation of composition as well as for practical testing.

\bibliography{a}
\bibliographystyle{plain}
\end{document}








We use symbols ``$A$'', ``$B$'', ``$C$'', ``$D$'', ``$E$'' to
denote closed formulas and symbols ``$F$'', ``$G$'', ``$H$'' to denote
formulas which may contain free occurrences of variables. Symbols
``$u$'', \ldots, ``$z$'' denote variables.


--------------------------

The constraint is best understood by starting from the conclusion
$A\to\forall xF$. In order to prove $A\to\forall xF$ you have to
introduce a parameter $p$ not occurring in $A\to\forall xF$ and show
that $A\to F\rep xp$ holds for every value of $p$. Then an application
of the rule gives the conclusion $A\to\forall xF$. We say that $p$ is
the \emph{critical parameter} of the rule application.

Frege-Hilbert Calculi can be used to prove the validity of a formula.
The connection between calculi and the semantics is given by the
soundness and completeness theorems. Namely, for those Frege-Hilbert
calculi which have been established for first order predicate logic, a
formula is derivable in the calculus if and only if it is valid.

-----------------------------------------------------------
