TFX: The TPTP extended typed first-order form

Geoffrey Sutcliffe, Evgenii Kotelnikov

Research output: Contribution to journalConference article

1 Scopus citations

Abstract

The TPTP world is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving systems for classical logics. The TPTP language is one of the keys to the success of the TPTP world. Originally the TPTP world supported only first-order clause normal form (CNF). Over the years support for full first-order form (FOF), monomorphic typed first-order form (TF0), rank-1 polymorphic typed first-order form (TF1), monomorphic typed higher-order form (TH0), and rank-1 polymorphic typed higher-order form (TH1), have been added. TF0 and TF1 together form the TFF language family; TH0 and TH1 together form the THF language family. This paper introduces the eXtended Typed First-order form (TFX), which extends TFF to include boolean terms, tuples, conditional expressions, and let expressions.

Original languageEnglish (US)
Pages (from-to)72-87
Number of pages16
JournalCEUR Workshop Proceedings
Volume2162
StatePublished - Jan 1 2018
Event6th Workshop on Practical Aspects of Automated Reasoning, PAAR 2018 - Oxford, United Kingdom
Duration: Jul 19 2018 → …

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'TFX: The TPTP extended typed first-order form'. Together they form a unique fingerprint.

  • Cite this