Extracting Higher-Order Goals from the Mizar Mathematical Library

TL;DR

This paper presents a method to translate Mizar articles into higher-order logic problems, enabling the use of higher-order theorem provers to handle constructs not representable in first-order logic.

Contribution

It introduces a novel translation approach for Mizar articles into higher-order logic, facilitating automated theorem proving with higher-order provers.

Findings

Higher-order theorem provers successfully processed the translated problems.

The translation enables representation of schemes, global choice, and set level binders.

Results demonstrate the potential of higher-order logic in formalizing complex mathematical constructs.

Abstract

Certain constructs allowed in Mizar articles cannot be represented in first-order logic but can be represented in higher-order logic. We describe a way to obtain higher-order theorem proving problems from Mizar articles that make use of these constructs. In particular, higher-order logic is used to represent schemes, a global choice construct and set level binders. The higher-order automated theorem provers Satallax and LEO-II have been run on collections of these problems and the results are discussed.