The Dependently Typed Higher-Order Form for the TPTP World
Fuente:
arXiv
Gespeichert in:
| Hauptverfasser: | , , , |
|---|---|
| Format: | Preprint |
| Veröffentlicht: |
2025
|
| Schlagworte: | |
| Online-Zugang: | |
| Tags: |
Tag hinzufügen
Keine Tags, Fügen Sie den ersten Tag hinzu!
|
| _version_ | 1866916825572311040 |
|---|---|
| author | Ranalter, Daniel Kaliszyk, Cezary Rabe, Florian Sutcliffe, Geoff |
| author_facet | Ranalter, Daniel Kaliszyk, Cezary Rabe, Florian Sutcliffe, Geoff |
| contents | 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 (DTF) 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 DTF. Some tools that are already able to reason about problems in the DTF language are discussed. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2507_03208 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | The Dependently Typed Higher-Order Form for the TPTP World Ranalter, Daniel Kaliszyk, Cezary Rabe, Florian Sutcliffe, Geoff Logic in Computer Science F.4.1 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 (DTF) 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 DTF. Some tools that are already able to reason about problems in the DTF language are discussed. |
| title | The Dependently Typed Higher-Order Form for the TPTP World |
| topic | Logic in Computer Science F.4.1 |
| url | https://arxiv.org/abs/2507.03208 |