Proof Search in Minimal Logic - Artificial Intelligence and Symbolic Computation - page 15

Proof Search in Minimal Logic

Helmut Schwichtenberg

Mathematisches Institut der Universitat Munchen
[e-mail]
http://www.mathematik.uni-muenchen.de/~schwicht/

1 Introduction

We describe a rather natural proof search algorithm for a certain fragment of
higher order (simply typed) minimal logic. This fragment is determined by re-
quiring that every higher order variable

Y Y x

can only occur in a context ,where

x ,andof

opposite polarity. Note that for first order logic this restriction does not mean
anything, since there are no higher order variables. However, when designing a
proof search algorithm for first order logic only, one is naturally led into this
fragment of higher order logic, where the algorithm works as well.
In doing this we rely heavily on Miller's [1], who has introduced this type
of restriction to higher order terms (called patterns by Nipkow [2]), noted its
relevance for extensions of logic programming, and showed that the unification
problem for patterns is solvable and admits most general unifiers. The present
paper was motivated by the desire to use Miller's approach as a basis for an
implementation of a simple proof search engine for (first and higher order) min-
imal logic. This goal prompted us into several simplifications, optimizations and
extensions, in particular the following.

are distinct bound variables in the scope of the operator binding Y

- Instead of arbitrarily mixed prefixes we only use those of the form .

Nipkow in [2] already had presented a version of Miller's pattern unification
algorithm for such prefixes, and Miller in [1, Section 9.2] notes that in such
a situation any two unifiers can be transformed into each other by a variable
renaming substitution. Here we restrict ourselves to

∀∃∀

∀∃∀ -prefixes throughout,

i.e., in the proof search algorithm as well.

- The order of events in the pattern unification algorithm is changed slightly,

by postponing the raising step until it is really needed. This avoids unnec-
essary creation of new higher type variables. - Already Miller noted in [1,
p.515] that such optimizations are possible.

- The extensions concern the (strong) existential quantifier, which has been

left out in Miller's treatment, and also conjunction. The latter can be avoided
in principle, but of course is a useful thing to have.

Moreover, since part of the motivation to write this paper was the necessity to
have a guide for our implementation, we have paid particular attention to write
at least the parts of the proofs with algorithmic content as clear and complete
as possible.