| • TPTP Proposals
| We are working on new features for the TPTP, as explained
in the following proposals.
Comments from potential users will be appreciated.
|
| • TPTP Software
| 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.
- João Paulo A. Almeida's
TPTP Editor as an Eclipse Plugin.
- 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.
|
| • External Projects
| Other people are collaborating with the TPTP ...
|
|
|
Other people are doing similar things for other types of ATP problems:
|
| • VeriFun
| Case studies that require induction.
|
| • SV-COMP
| Benchmark verification tasks in software verification, as used in SV-COMP.
|
| • Larry Wos' Notebooks
| 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).
|
| • SMT-LIB
| 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.
|
| • QMLTP
| 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.
|
| • DPPD
| The Dozens of Problems for Partial Deduction (DPPD) Library of Benchmarks aims at being
a standard suite of benchmarks for partial deduction.
|
| • Asparagus
| 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.
|
| • ILTP
| 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.
|
| • TPBD
| 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.
|
| • CSPLib
| 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.
|
| • OR-Library
| A collection of test data sets for a variety of Operations
Research (OR) problems.
|
| • PSPLIB
| The Project Scheduling Problem Library.
|
| • VFLib
| The graph matching library, developed mainly to test the VF graph matching algorithm,
and to compare it with other known algorithms.
|
| • SATLIB
| A collection of benchmark problems, solvers, and tools for SAT related research.
|
| • SATEX
| Experiments and execution traces of SAT solvers, on all benchmarks that are provided.
|
| • QBFLib
| QBFLIB is a collection of benchmark problems, solvers, and tools related to Quantified
Boolean Formula (QBF) satisfiability.
|
