Proof Search in Minimal Logic

We describe a rather natural proof search algorithm for a certain fragment of higher order (simply typed) minimal logic. This fragment is determined by requiring that every higher order variable Y can only occur in a context \(Y \vec{x}\), where \(\vec{x}\) are distinct bound variables in the scope of the operator binding Y, and of 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.

Authors and Affiliations

1. Mathematisches Institut der Universität München,  

   Helmut Schwichtenberg

Editors and Affiliations

1. Research Institute for Symbolic Computation, Johannes Kepler University, Linz, Austria

   Bruno Buchberger

2. Department of Computer Science, University College London, Gower Street, WC1E 6BT, London, UK

   John Campbell

Reprints and permissions

© 2004 Springer-Verlag Berlin Heidelberg

Policies and ethics