Extracting Higher-Order Goals from the Mizar Mathematical Library
Logic in Computer Science
2016-05-24 v1 Artificial Intelligence
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.
Cite
@article{arxiv.1605.06996,
title = {Extracting Higher-Order Goals from the Mizar Mathematical Library},
author = {Chad Brown and Josef Urban},
journal= {arXiv preprint arXiv:1605.06996},
year = {2016}
}
Comments
Accepted to CICM 2016. The final publication will be available at Springer