\documentclass[a4paper]{article}
\usepackage{amssymb}
\pagestyle{empty}
\hoffset=-40pt
\voffset=-20pt
\textwidth 15.3cm
\textheight 22cm % to fit our printers

\begin{document}

\begin{center}{\huge Herbrand's Theorem and the 
Structure of Analytic Search Spaces
}\end{center}
\begin{center}{\large Lincoln Wallen}\end{center}
\begin{center}{\large Oxford University}\end{center}

\bigskip
\large
Gentzen's Hauptsatz and its immediate corollaries form the basis for
the architecture of most standard schemes of automated deduction in
both classical and nonclassical propositional logics.  Indeed, from a
proof-theoretical perspective, extension to nonclassical settings is
considered one of the main advantages of Gentzen's methods over those
of Herbrand.

The picture is less clear if we consider first-order extensions.  In
that setting Herbrand's reduction of provability in the predicate
calculus to three components: (1) restricted contraction, (2)
propositional provability, and (3) (free) equation solving for
managing dependencies between quantifiers, plays the central role in
the formulation of practical search spaces; Gentzen's results
are then used to structure the propositional component (2 above).

The failure of Herbrand's Theorem to extend beyond classical logic
suggests that its use as an architectural primitive for search spaces
is limited.  However, closer inspection reveals that its main role in
the predicate calculus is to render search involving the
non-invertible logical elements (the quantifiers) wholly dependent on
search involving the invertible elements (propositional connectives),
thereby recapturing --- as far as is possible --- the combinatorics of
the propositional case.

Following through with this observation leads to the formulation of
Herbrand-like theorems even for propositional (non-classical) logics,
where search involving non-invertible logical elements (eg.,
intuitionistic connectives) is decomposed in terms of (1) restricted
contraction, (2) search spaces involving invertible connectives
(typically classical), and (3) equation solving to manage the
dependencies.  That is to say, in all those respects that matter for
automated deduction, Herbrand's Theorem can be generalised to
nonclassical settings.

Using intuitionistic logic as an example, I shall present the results
which have led to this perspective, and illustrate how the ideas have
yielded improved results on translations and contraction.  I shall
also present some recent attempts to formulate the argument in a more
general setting using a system of type-theoretic realisers for the
classical sequent calculus.  I will sketch how these realisers can be
used to characterise the search spaces of standard algorithms, using
(intuitionistic) resolution as an example.
\end{document}