TH1

The TPTP typed higher-order form with rank-1 polymorphism

Cezary Kaliszyk, Geoffrey Sutcliffe, Florian Rabe

Research output: Contribution to journalArticle

7 Citations (Scopus)

Abstract

The TPTP world is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) 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), and monomorphic typed higher-order form (TH0) have been added. The TF0, TF1, and TH0 languages also include constructs for arithmetic. This paper introduces the TH1 form, an extension of TH0 with TF1-style rank-1 polymorphism. TH1 is designed to be easy to process by existing reasoning tools that support ML-style polymorphism. The hope is that TH1 will be implemented in many popular ATP systems for typed higher-order logic.

Original languageEnglish (US)
Pages (from-to)41-55
Number of pages15
JournalUnknown Journal
Volume1635
StatePublished - 2016

Fingerprint

Theorem proving
theorem proving
polymorphism
Polymorphism
Hope
Language
logic
research and development
Research

ASJC Scopus subject areas

  • Computer Science(all)

Cite this

TH1 : The TPTP typed higher-order form with rank-1 polymorphism. / Kaliszyk, Cezary; Sutcliffe, Geoffrey; Rabe, Florian.

In: Unknown Journal, Vol. 1635, 2016, p. 41-55.

Research output: Contribution to journalArticle

Kaliszyk, Cezary ; Sutcliffe, Geoffrey ; Rabe, Florian. / TH1 : The TPTP typed higher-order form with rank-1 polymorphism. In: Unknown Journal. 2016 ; Vol. 1635. pp. 41-55.
@article{97381c9271a640ecb213e01983453c93,
title = "TH1: The TPTP typed higher-order form with rank-1 polymorphism",
abstract = "The TPTP world is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) 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), and monomorphic typed higher-order form (TH0) have been added. The TF0, TF1, and TH0 languages also include constructs for arithmetic. This paper introduces the TH1 form, an extension of TH0 with TF1-style rank-1 polymorphism. TH1 is designed to be easy to process by existing reasoning tools that support ML-style polymorphism. The hope is that TH1 will be implemented in many popular ATP systems for typed higher-order logic.",
author = "Cezary Kaliszyk and Geoffrey Sutcliffe and Florian Rabe",
year = "2016",
language = "English (US)",
volume = "1635",
pages = "41--55",
journal = "Scientific Computing and Instrumentation",
issn = "1078-8956",
publisher = "Springer Wien",

}

TY - JOUR

T1 - TH1

T2 - The TPTP typed higher-order form with rank-1 polymorphism

AU - Kaliszyk, Cezary

AU - Sutcliffe, Geoffrey

AU - Rabe, Florian

PY - 2016

Y1 - 2016

N2 - The TPTP world is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) 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), and monomorphic typed higher-order form (TH0) have been added. The TF0, TF1, and TH0 languages also include constructs for arithmetic. This paper introduces the TH1 form, an extension of TH0 with TF1-style rank-1 polymorphism. TH1 is designed to be easy to process by existing reasoning tools that support ML-style polymorphism. The hope is that TH1 will be implemented in many popular ATP systems for typed higher-order logic.

AB - The TPTP world is a well established infrastructure that supports research, development, and deployment of Automated Theorem Proving (ATP) 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), and monomorphic typed higher-order form (TH0) have been added. The TF0, TF1, and TH0 languages also include constructs for arithmetic. This paper introduces the TH1 form, an extension of TH0 with TF1-style rank-1 polymorphism. TH1 is designed to be easy to process by existing reasoning tools that support ML-style polymorphism. The hope is that TH1 will be implemented in many popular ATP systems for typed higher-order logic.

UR - http://www.scopus.com/inward/record.url?scp=84983082078&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=84983082078&partnerID=8YFLogxK

M3 - Article

VL - 1635

SP - 41

EP - 55

JO - Scientific Computing and Instrumentation

JF - Scientific Computing and Instrumentation

SN - 1078-8956

ER -