The Dependently Typed Higher-Order Form for the TPTP World
Ranalter D, Kaliszyk C, Rabe F, Sutcliffe G (2026)
Publication Type: Conference contribution
Publication year: 2026
Journal
Publisher: Springer Science and Business Media Deutschland GmbH
Book Volume: 15979 LNAI
Pages Range: 287-305
Conference Proceedings Title: Lecture Notes in Computer Science
Event location: Reykjavik, ISL
ISBN: 9783032041661
DOI: 10.1007/978-3-032-04167-8_16
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 far-reaching 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.
Authors with CRIS profile
Involved external institutions
Austria (AT)How to cite
APA:
Ranalter, D., Kaliszyk, C., Rabe, F., & Sutcliffe, G. (2026). The Dependently Typed Higher-Order Form for the TPTP World. In René Thiemann, Christoph Weidenbach (Eds.), Lecture Notes in Computer Science (pp. 287-305). Reykjavik, ISL: Springer Science and Business Media Deutschland GmbH.
MLA:
Ranalter, Daniel, et al. "The Dependently Typed Higher-Order Form for the TPTP World." Proceedings of the 15th International Symposium on Frontiers of Combining Systems, FroCoS 2025, Reykjavik, ISL Ed. René Thiemann, Christoph Weidenbach, Springer Science and Business Media Deutschland GmbH, 2026. 287-305.
BibTeX: Download