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

Christoph Benzmüller, Florian Rabe, Geoffrey Sutcliffe

Research output: Chapter in Book/Report/Conference proceedingConference contribution

21 Citations (Scopus)

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 languageEnglish (US)
Title of host publicationLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Pages491-506
Number of pages16
Volume5195 LNAI
DOIs
StatePublished - 2008
Event4th International Joint Conference on Automated Reasoning, IJCAR 2008 - Sydney, NSW, Australia
Duration: Aug 12 2008Aug 15 2008

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume5195 LNAI
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other4th International Joint Conference on Automated Reasoning, IJCAR 2008
CountryAustralia
CitySydney, NSW
Period8/12/088/15/08

Fingerprint

Higher-order Logic
Religious buildings
Theorem
Type Theory
Infrastructure
Language
First-order

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science

Cite this

Benzmüller, C., Rabe, F., & Sutcliffe, G. (2008). THF0 - The core of the TPTP language for higher-order logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 5195 LNAI, 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, Geoffrey.

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5195 LNAI 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 proceedingConference contribution

Benzmüller, C, Rabe, F & Sutcliffe, G 2008, THF0 - The core of the TPTP language for higher-order logic. in Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). vol. 5195 LNAI, 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 Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5195 LNAI. 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
Benzmüller, Christoph ; Rabe, Florian ; Sutcliffe, Geoffrey. / THF0 - The core of the TPTP language for higher-order logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics). Vol. 5195 LNAI 2008. pp. 491-506 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).
@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 Geoffrey Sutcliffe",
year = "2008",
doi = "10.1007/978-3-540-71070-7_41",
language = "English (US)",
isbn = "3540710698",
volume = "5195 LNAI",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
pages = "491--506",
booktitle = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

}

TY - GEN

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

AU - Benzmüller, Christoph

AU - Rabe, Florian

AU - Sutcliffe, Geoffrey

PY - 2008

Y1 - 2008

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

VL - 5195 LNAI

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

SP - 491

EP - 506

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

ER -