Michael Beeson

Title: Lambda unification and its application to finding proofs by
mathematical induction.

Abstract: Lambda logic is the union of first order logic and lambda
calculus.  Lambda unification is a version of unification appropriate
for use in lambda logic.  Otter-lambda is an extension of Otter to
lambda logic, using lambda unification.  Otter-lambda is pretty good
at finding proofs by mathematical induction, among other things.  The
talk will illustrate lambda-unification by application to mathematical
induction and give examples of proofs that have been obtained.

Title:   Calling external simplification programs from within Otter.

Abstract: Otter (and Otter-lambda) have been connected to the computer
algebra system MathXpert.  Derived clauses are passed to MathXpert for
simplification.  Since MathXpert is logically sound, the
simplification can generate additional assumptions, whose negations
are added as new literals to the returned clause.  The combined system
is able to do standard undergraduate-level proofs such as inductive
proofs of the formula for the sum of the first N integers (or squares
of integers), and more algebraic proofs such as the
arithmetic-geometric mean inequality.

Title:  Implicit typing in lambda logic.

Abstract: lambda logic seems to be on the verge of paradox to some
referees; for instance the axioms of group theory, in lambda logic,
imply that everything equals the identity.  Does that mean I must
relativize the group theory axioms to a unary predicate G(x), with the
accompanying loss of efficiency in proof search?  No, it doesn't, and
the notion of "implicit typing" explains why not.  Implicit typing is
an old and almost obvious notion in first order theorem proving,
although it still could be more widely used than it is; its extension
to lambda logic is less obvious.