TPTP
From MaRDI portal
Software:16327
swMATH4143MaRDI QIDQ16327FDOQ16327
Author name not available (Why is that?)
Official website: http://www.cs.miami.edu/~tptp/
Cited In (only showing first 100 items - show all)
- Zenon Modulo: When Achilles Outruns the Tortoise Using Deduction Modulo
- Satallax: An Automatic Higher-Order Prover
- Zenon: An Extensible Automated Theorem Prover Producing Checkable Proofs
- LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description)
- THF0 – The Core of the TPTP Language for Higher-Order Logic
- SOLAR: An automated deduction system for consequence finding
- GCLC
- ILTP
- LEO-II
- Title not available (Why is that?)
- Title not available (Why is that?)
- Theorema
- TPS
- Prosper
- MizarMode
- SATLIB
- MPTP 0.2
- MAYA
- SMT-LIB
- SPASS
- Isar
- MoMM
- Mizar
- Yices
- Mozart
- SPASS+T
- STRIP
- Prover9
- z3
- Eukleides
- HOL
- TeXmacs
- GeoProof
- ETPS
- ASASP
- FINDER
- HOL Light
- DCTP
- GrAnDe
- I-SATCHMO
- R-SATCHMO
- SATCHMO
- SATCHMOREBID
- SCOTT
- E-Darvin
- MUSCADET
- Satallax
- Mace4
- NiVER
- MML
- Hets
- Zenon
- Automath
- Kodkod
- E-SETHEO
- Sledgehammer
- ArgoCLP
- PicoSAT
- Twelf
- OMDoc
- QMT
- ESC4
- MaLeCoP
- TNTBase
- veriT
- CVC Lite
- LoTREC
- HipSpec
- KRATOS
- STEXIDE
- MaSh
- Zeno
- KAT-ML
- RALL
- Asparagus
- MBase
- RunLim
- Runsolver
- IMPS
- Panoptes
- Abella
- CERES
- StarExec
- CVC4
- Herod
- iProver-Eq
- Pilate
- iProver
- Mella
- MGTP
- Model evolution with equality -- revised and implemented
- MPTP-motivation, implementation, first experiments
- Integrating Dynamic Geometry Software, Deduction Systems, and Theorem Repositories
- MPTP 0.2: Design, implementation, and initial experiments
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- A coherent logic based geometry theorem prover capable of producing formal and readable proofs
- LEO-II and Satallax on the Sledgehammer test bench
- Metis
- Herbrand constructivization for automated intuitionistic theorem proving
This page was built for software: TPTP
