Dolmen provides a library and a binary to parse, typecheck, and evaluate languages used in automated deduction
Testing and benchmarking tool for logic-related programs.
Haskell interface to automated theorem provers
Efficient and multi-language generation from context free or sensitive grammars (CFG/CSG)
Parser and pretty printer for the TPTP language
A parser for the TPTP logic languages for automated theorem proving written in Scala
A verification conditions generator for Boogie programs
Library for TPTP-related utility services
A reasoner for Input/Output logic
Experimental first-order theorem prover in Rust, with Lean 4 proof checking and TSTP output.
Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).
Total Grip-backed TPTP/TSTP parsers for Lean 4
ProofGuard: a checker for first-order logic proofs in TSTP format. Placed 5th at ProoVer 2026 (FLoC 2026, Lisbon).
Example axiom and problem files within the TPTP Format
Sort-Stratified Semantics for Temporal Conflict Detection between pairs of ODRL policies
A formal, axiomatic treatment of libertarian property theory for Leo-III
To associate your repository with the tptp topic, visit your repo's landing page and select "manage topics."