The Dependently Typed Higher-Order Form for the TPTP World
Daniel Ranalter, Cezary Kaliszyk, Florian Rabe, Geoff Sutcliffe15th International Symposium on Frontiers of Combining Systems, Lecture Notes in Artificial Intelligence 15979, pp. 287-305, 2025.
Abstract
Much of the current research and development in the field of automated reasoning builds on the infrastructure provided by the TPTP World. The TPTP language for logical formulae is central to the farreaching adoption of the TPTP World. This paper introduces the Dependently Typed higher-order Form (DHF) of the TPTP language. It takes advantage of already established binders in the syntax, and is thus a minimally intrusive extension to the Typed Higher-order Form (THF). A starting set of over 100 problems is provided to exhibit the usefulness and incite interest in DHF. Some tools that are already able to reason about problems in the DHF language are discussed.
BibTeX
@inproceedings{DRCKFRGS-FROCOS25,
author = "Daniel Ranalter and Cezary Kaliszyk and Florian Rabe and Geoff Sutcliffe",
title = "The Dependently Typed Higher-Order Form for the {TPTP} World",
booktitle = "Frontiers of Combining Systems -- 15th International Symposium, FroCoS 2025, Reykjavik, Iceland, September 29 - October 1, 2025, Proceedings",
editor = "Ren{\'{e}} Thiemann and Christoph Weidenbach",
series = "Lecture Notes in Computer Science",
volume = 15979,
pages = "287--305",
year = 2025,
doi = "10.1007/978-3-032-04167-8_16"
}