Extracting Higher-Order Goals from the Mizar Mathematical Library
This work addresses a specific challenge in automated theorem proving for mathematical formalization, but it is incremental as it builds on existing methods for handling higher-order logic.
The paper tackled the problem of representing certain Mizar mathematical library constructs that are not expressible in first-order logic by converting them into higher-order theorem proving problems, and reported results from running automated provers Satallax and LEO-II on these problems.
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.