The TPTP Problem Library and Associated Infrastructure

被引：134

作者：

Sutcliffe, Geoff ^{[1
]}

机构：

[1] Univ Miami, Dept Comp Sci, Coral Gables, FL 33124 USA

来源：

JOURNAL OF AUTOMATED REASONING | 2017年 / 59卷 / 04期

关键词：

TPTP; ATP system evaluation; ATP standards and tools; HIGHER-ORDER LOGIC; INTUITIONISTIC LOGIC; IMPLEMENTATION; VERIFICATION; LANGUAGE; SYSTEM; CASC; ATP;

D O I：

10.1007/s10817-017-9407-7

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

This paper describes the TPTP problem library and associated infrastructure, from its use of Clause Normal Form (CNF), via the First-Order Form (FOF) and Typed First-order Form (TFF), through to the monomorphic Typed Higher-order Form (TH0). TPTP v6.4.0 was the last release prior to the introduction of the polymorphic Typed Higher-order Form, and thus serves as the exemplar. This paper summarizes the aims and history of the TPTP, documents its growth up to v6.4.0, reviews the structure and contents of TPTP problems, and gives an overview of TPTP-related infrastructure.

引用

页码：483 / 502

页数：20

共 54 条

[1]

American Mathematical Society, 1992, MATH SUBJ CLASS

[2]

[Anonymous], 2010, EPIC SERIES COMPUTIN, DOI DOI 10.29007/36DT

[3]

[Anonymous], J APPL LOGIC

[4]

Barrett Clark, 2010, P 8 INT WORKSH SAT M

[5] SMTtoTPTP - A Converter for Theorem Proving Formats [J].

Baumgartner, Peter .

AUTOMATED DEDUCTION - CADE-25, 2015, 9195 :285-294

[6] Automating Godel's Ontological Proof of God's Existence with Higher-order Automated Theorem Provers [J].

Benzmueller, Christoph ;

Paleo, Bruno Woltzenlogel .

21ST EUROPEAN CONFERENCE ON ARTIFICIAL INTELLIGENCE (ECAI 2014), 2014, 263 :93-+

[7] Quantified Multimodal Logics in Simple Type Theory [J].

Benzmueller, Christoph ;

Paulson, Lawrence C. .

LOGICA UNIVERSALIS, 2013, 7 (01) :7-20

[8]

Blanchette Jasmin Christian, 2013, Automated Deduction - CADE-24. 24th International Conference on Automated Deduction. Proceedings: LNCS 7898, P414, DOI 10.1007/978-3-642-38574-2_29

[9] A Learning-Based Fact Selector for Isabelle/HOL [J].

Blanchette, Jasmin Christian ;

Greenaway, David ;

Kaliszyk, Cezary ;

Kuhlwein, Daniel ;

Urban, Josef .

JOURNAL OF AUTOMATED REASONING, 2016, 57 (03) :219-244

[10]

Böhme S, 2010, LECT NOTES ARTIF INT, V6173, P107, DOI 10.1007/978-3-642-14203-1_9

← 1 2 3 4 5 6 →