| We are working on new features for the TPTP, as explained
in the following proposals.
Comments from potential users will be appreciated.
|
|
|
| Many people have written software for processing TPTP format data.
These links point to software I know of (please send your link
if you have some software to add to the list).
- Geoff's Service Tools.
A bunch of tools for manipulating the TPTP,
including the JJ parser for the TPTP language
(named after the Spanish software developers, Justo
Fernandez Reche and José Taboada Berenguer).
The JJ parser will parse TPTP files and build a useful data
structure, and there are lots of "useful" API functions for
interrogating and manipulating the data structure.
There is no documentation for any of this yet, but the sample
drivers illustrate how to use the JJ parser API.
- Alex Steen's
Scala parser for the entire TPTP grammar.
- Tobias Gleißner's
ANTLR4 grammar for the SyntaxBNF-v7.0.0.
- Guy Shefner's
Java class library for parsing, structuring, and basic
manipulation of problems in first order logic.
- Matthias Fuchs'
NPM package
for the TPTP and SystemOnTPTP.
- Mark Lemay's
Xtext based
Java parser for the TPTP grammar.
- Michael Rawson's
Rust parser
for the TPTP's FOF and CNF grammars.
|
| This approximately-annual meeting is used to to discuss the
TPTP and related issues.
|
|
Other people are doing similar things for other types of ATP problems:
|
| Benchmark verification tasks in software verification, as used
in SV-COMP.
|
| This website features a series of notebooks presenting some of
Larry Wos’s most recent and hitherto unpublished research in
automated reasoning (also in 1st order logic).
|
| The major goal of SMT-LIB is to establish a library of benchmarks
for Satisfiability Modulo Theories, that is, satisfiability of
formulas with respect to background theories for which specialized
decision procedures exist.
|
| The Quantified Modal Logics Theorem Proving (QMLTP) library
provides a platform for testing and benchmarking automated
theorem proving (ATP) systems for first-order modal logics.
|
| The Dozens of Problems for Partial Deduction (DPPD) Library of
Benchmarks aims at being a standard suite of benchmarks for partial
deduction.
|
| An environment for submitting and archiving benchmarking Answer-Set
Programming (ASP) problems and instances, in which ASP systems can
be run under equal and reproducible conditions, leading to
independent results.
|
| The Intuitionistic Logic Theorem Proving (ILTP) library provides
a platform for testing and benchmarking automated theorem proving
(ATP) systems for first-order and propositional intuitionistic logic.
|
| The Termination Problems Database is a library of test problems
for termination provers.
Currently, it includes termination problems for term rewrite
systems and logic programs.
|
| A benchmark library of problems for the constraints community.
The main motivation for CSPLib is to focus research in constraints
away from purely random problems and onto more structured problems.
|
| A collection of test data sets for a variety of Operations
Research (OR) problems.
|
| The Project Scheduling Problem Library.
|
| The graph matching library, developed mainly to test the VF
graph matching algorithm, and to compare it with other known
algorithms.
|
| A collection of induction challenge problems.
|
| A collection of benchmark problems, solvers, and tools for SAT
related research.
|
| Experiments and execution traces of SAT solvers, on all benchmarks
that are provided.
|
|