\documentclass{llncs}
\usepackage{makeidx}  % allows for indexgeneration
\def\plus{{\rm plus}}
\def\type{type}  % changed my mind about {\rm type} 
\def\bool{{\rm bool}}
\begin{document}
\frontmatter          % for the preliminaries
\pagestyle{headings}  % switches on printing of running heads
%
\title{Otter-lambda}
\author{Michael Beeson\inst{1}}
\authorrunning{Michael Beeson}  
%
%%%% modified list of authors for the TOC (add the affiliations)
\tocauthor{Michael Beeson (San Jos\'e State University)}
\institute{San Jos\'e State University, San Jos\'e, Calif.\\
\email{beeson@cs.sjsu.edu,\\
\texttt{www.cs.sjsu.edu/faculty/beeson}}
}
\maketitle              % typeset the title of the contribution

\begin{abstract}  % should be 70-150 words
Otter-lambda is a theorem-prover based on an untyped logic with lambda calculus, called Lambda Logic.  Otter-lambda is built on Otter, so it uses resolution proof search, supplemented by demodulation and paramodulation for equality reasoning,  but it also uses a new algorithm, lambda unification, for instantiating variables for functions or predicates.  The underlying logic 
of Otter-lambda is lambda logic, an untyped logic combining lambda calculus and first-order logic.
The use of lambda unification allows Otter-lambda to prove some theorems usually thought of as
``higher-order''.  There are theoretical questions about lambda logic and its relation to first-order and higher-order logic, and theoretical questions about lambda unification and its relation to higher-order unification, but the demonstration will focus on the practical capabilities of Otter-lambda.  Specifically, several proofs in algebra and number theory will be discussed, with special focus on the use of Otter-lambda in connection with mathematical induction.
Otter-lambda has had some successes in this area, since lambda logic can state the general induction schema (with a variable for a predicate), and lambda unification can sometimes find the appropriate instance(s) of induction for a particular problem, even when nested multiple inductions are required.  Once that it is done, the full resources of Otter are available to carry out the base case and the induction step, with lambda-unification still available if another induction is needed.  Some examples are carried out directly from Peano's axioms, such as the commutativity of multiplication. Some involve algebra, for example, there are no nilpotents in an integral domain.  Others are carried out with the aid of external simplification by MathXpert, for example, a proof by induction on $n$ of Bernoulli's inequality $1 + nx \le (1+x)^n$ if $x > -1$.
\end{abstract}

\end{document}