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, higherorder 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.
CITATION STYLE
Brown, C. E., & Urban, J. (2016). Extracting higher-order goals from the mizar mathematical library. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9791, pp. 99–114). Springer Verlag. https://doi.org/10.1007/978-3-319-42547-4_8
Mendeley helps you to discover research relevant for your work.