THF0 - The core of the TPTP language for higher-order logic

Christoph Benzmüller; Florian Rabe; Geoff Sutcliffe

doi:10.1007/978-3-540-71070-7_41

THF0 - The core of the TPTP language for higher-order logic

Christoph Benzmüller, Florian Rabe, Geoff Sutcliffe

Computer Science

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

22 Scopus citations

Abstract

One of the keys to the success of the Thousands of Problems for Theorem Provers (TPTP) problem library and related infrastructure is the consistent use of the TPTP language. This paper introduces the core of the TPTP language for higher-order logic - THF0, based on Church's simple type theory. THF0 is a syntactically conservative extension of the untyped first-order TPTP language.

Original language	English (US)
Title of host publication	Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings
Pages	491-506
Number of pages	16
DOIs	https://doi.org/10.1007/978-3-540-71070-7_41
State	Published - Oct 7 2008
Event	4th International Joint Conference on Automated Reasoning, IJCAR 2008 - Sydney, NSW, Australia Duration: Aug 12 2008 → Aug 15 2008

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	5195 LNAI
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Other

Other	4th International Joint Conference on Automated Reasoning, IJCAR 2008
Country	Australia
City	Sydney, NSW
Period	8/12/08 → 8/15/08

ASJC Scopus subject areas

Theoretical Computer Science
Computer Science(all)

Access to Document

10.1007/978-3-540-71070-7_41

Fingerprint Dive into the research topics of 'THF0 - The core of the TPTP language for higher-order logic'. Together they form a unique fingerprint.

Cite this

Benzmüller, C., Rabe, F., & Sutcliffe, G. (2008). THF0 - The core of the TPTP language for higher-order logic. In Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings (pp. 491-506). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5195 LNAI). https://doi.org/10.1007/978-3-540-71070-7_41

THF0 - The core of the TPTP language for higher-order logic. / Benzmüller, Christoph; Rabe, Florian; Sutcliffe, Geoff.

Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings. 2008. p. 491-506 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 5195 LNAI).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

Benzmüller, C, Rabe, F & Sutcliffe, G 2008, THF0 - The core of the TPTP language for higher-order logic. in Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 5195 LNAI, pp. 491-506, 4th International Joint Conference on Automated Reasoning, IJCAR 2008, Sydney, NSW, Australia, 8/12/08. https://doi.org/10.1007/978-3-540-71070-7_41

Benzmüller C, Rabe F, Sutcliffe G. THF0 - The core of the TPTP language for higher-order logic. In Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings. 2008. p. 491-506. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). https://doi.org/10.1007/978-3-540-71070-7_41

@inproceedings{79283f74d583440f9cd90ec41d7de81b,

title = "THF0 - The core of the TPTP language for higher-order logic",

abstract = "One of the keys to the success of the Thousands of Problems for Theorem Provers (TPTP) problem library and related infrastructure is the consistent use of the TPTP language. This paper introduces the core of the TPTP language for higher-order logic - THF0, based on Church's simple type theory. THF0 is a syntactically conservative extension of the untyped first-order TPTP language.",

author = "Christoph Benzm{\"u}ller and Florian Rabe and Geoff Sutcliffe",

year = "2008",

month = oct,

day = "7",

doi = "10.1007/978-3-540-71070-7_41",

language = "English (US)",

isbn = "3540710698",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

pages = "491--506",

booktitle = "Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings",

note = "4th International Joint Conference on Automated Reasoning, IJCAR 2008 ; Conference date: 12-08-2008 Through 15-08-2008",

}

TY - GEN

T1 - THF0 - The core of the TPTP language for higher-order logic

AU - Benzmüller, Christoph

AU - Rabe, Florian

AU - Sutcliffe, Geoff

PY - 2008/10/7

Y1 - 2008/10/7

N2 - One of the keys to the success of the Thousands of Problems for Theorem Provers (TPTP) problem library and related infrastructure is the consistent use of the TPTP language. This paper introduces the core of the TPTP language for higher-order logic - THF0, based on Church's simple type theory. THF0 is a syntactically conservative extension of the untyped first-order TPTP language.

AB - One of the keys to the success of the Thousands of Problems for Theorem Provers (TPTP) problem library and related infrastructure is the consistent use of the TPTP language. This paper introduces the core of the TPTP language for higher-order logic - THF0, based on Church's simple type theory. THF0 is a syntactically conservative extension of the untyped first-order TPTP language.

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

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

U2 - 10.1007/978-3-540-71070-7_41

DO - 10.1007/978-3-540-71070-7_41

M3 - Conference contribution

AN - SCOPUS:53049095806

SN - 3540710698

SN - 9783540710691

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 491

EP - 506

BT - Automated Reasoning - 4th International Joint Conference, IJCAR 2008, Proceedings

T2 - 4th International Joint Conference on Automated Reasoning, IJCAR 2008

Y2 - 12 August 2008 through 15 August 2008

ER -