The TPTP Problem Library and Associated Infrastructure

By Geoff Sutcliffe. Journal of automated reasoning, 2009

651 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Computational Theory and Mathematics

View Paper: https://www.semanticscholar.org/paper/1dcb950a79cc07281d352d0a8d9cbe5c1df75bce

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Computational Theory and Mathematics

Citations in the corpus

Evaluation in artificial intelligence: from task-oriented to ability-oriented measurement (2017, methodology): “CADE ATP system competitiona Theorem proving (Sutcliffe and Suttner 2006; Sutcliffe 2009)”
Introducing StarExec: a Cross-Community Infrastructure for Logic Solving (2014, background): “Currently there is no support for multi-file benchmarks; however, StarExec supports benchmark dependencies, the referencing of other benchmark files (e.g., TPTP axioms files [14]) within a benchmark.”
Learning to Prove Theorems via Interacting with Proof Assistants (2019, methodology): “Datasets for theorem proving Our work is related to many previous theorem proving datasets (Sutcliffe, 2009; Bancerek et al., 2015; Gransden et al., 2015; Gauthier et al., 2018; Huang et al., 2019).”
MiniF2F: a cross-system benchmark for formal Olympiad-level mathematics (2021, background): “In the closely related ﬁeld of (ﬁrst-order) automated theorem proving (ATP), the TPTP (Sutcliffe, 2017) benchmark is a library of test problems in a uniﬁed format for ATP systems.”
Improving Graph Neural Network Representations of Logical Formulae with Subgraph Pooling (2019, background): “While state-of-the-art classical theorem provers excel at ﬁnding complex proofs in restricted domains (e.g. TPTP [1]), they have historically had difﬁculty when reasoning in broad contexts [2], [3].”
The SMT-LIB Standard Version 2.0 (2010, background): “for instance, the TPTP library [7] has done for theorem proving, or the SATLIB library [5] for propositional satisfiability.”
cvc5: A Versatile and Industrial-Strength SMT Solver (2022, background): “…not just for external client software, but also for its own parser and for additional language bindings in Java and Python. cvc5 also provides a textual command-line interface (CLI), built on top of the parser, which supports SMT-LIBv2 [25], SyGuS2 [104] and TPTP [134] as input languages.”
Deep Network Guided Proof Search (2017, methodology): “This is either given in the form of premises-conclusion pairs (Sutcliffe, 2009) or as procedures and intermediate steps (Wenzel, 1999).”