Extracting Higher-Order Goals From The Mizar Mathematical Library
Intelligent Computer Mathematics(2016)
摘要
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.
更多查看译文
关键词
Formalized mathematics, Set theory, Higher-order logic, Automated theorem proving
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络