Scholarlink

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.

错误：搜索内容不能为空，请输入英文关键词
错误：关键词超出字数限制，请精简
高级检索

The Dependently Typed Higher-Order Form for the TPTP World

  • 会议论文

  • 出版模式：

    开放获取

  • 发表日期：

    2026年

查看全文
  • Daniel Ranalter,
  • Cezary Kaliszyk,
  • Florian Rabe,
  • Geoff Sutcliffe

摘要

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.