TPTP
From MaRDI portal
Cited in
(only showing first 100 items - show all)- A domain-specific language for cryptographic protocols based on streams
- Lightweight relevance filtering for machine-generated resolution problems
- Computing finite models by reduction to function-free clause logic
- Solving the \$100 modal logic challenge
- Labelled splitting
- Automated verification of refinement laws
- Solving quantified verification conditions using satisfiability modulo theories
- First order Stålmarck. Universal lemmas through branch merges
- Theory reasoning in connection calculi
- Aligator
- GCLC
- ILTP
- LEO-II
- MetiTarski
- MiniSat
- MMP/Geometer
- Nitpick
- Improving the efficiency of a hyperlinking-based theorem prover by incremental evaluation with network structures
- Controlled integration of the cut rule into connection tableau calculi
- SETHEO
- lazyCoP
- Goeland
- RBAC-PAT
- RegStab
- Sympli
- ILLTP
- Nunchaku
- SOLAR
- A disjunctive positive refinement of model elimination and its application to subsumption deletion
- Theorema
- TPS
- Nagging: A distributed, adversarial search-pruning technique applied to first-order inference
- Xeukleides
- Alloy
- Clause trees: A tool for understanding and implementing resolution in automated reasoning
- Computing answers with model elimination
- Prosper
- IeanCOP: lean connection-based theorem proving
- On using ground joinable equations in equational theorem proving
- Eliminating redundant search space on backtracking for forward chaining theorem proving
- OilEd
- Isabelle/HOL
- \(\mathcal I\)-SATCHMORE: An improvement of \(\mathcal A\)-SATCHMORE
- SecureUML
- RuleML
- LWB
- PLAGIATOR
- TGTP
- MizarMode
- SATLIB
- MPTP
- MPTP 0.2
- OTTER
- VAMPIRE
- THF0
- MAYA
- PVS
- Connection tableau calculi with disjunctive constraints
- Evaluating general purpose automated theorem proving systems
- MathWebSearch
- A set solver for finite set relation algebra
- SMT-LIB
- SPASS
- Darwin
- Yices
- Metis
- Towards a unified ordering for superposition-based automated reasoning
- Hammer for Coq: automation for dependent type theory
- Isar
- SPASS+T
- STRIP
- MoMM
- Mizar
- Superposition with structural induction
- Automated theory exploration for interactive theorem proving: an introduction to the Hipster system
- Proof certificates in PVS
- Solving quantified linear arithmetic by counterexample-guided instantiation
- Mozart
- The OWL reasoner evaluation (ORE) 2015 competition report
- The TPTP problem library and associated infrastructure. From CNF to TH0, TPTP v6.4.0
- z3
- Prover9
- Model checking against arbitrary public announcement logic: a first-order-logic prover approach for the existential fragment
- TeXmacs
- Eukleides
- HOL
- Constraint solving for proof planning
- GeoProof
- Tactics and certificates in Meta Dedukti
- Superposition for -free higher-order logic
- The higher-order prover Leo-III
- Efficient encodings of first-order Horn formulas in equational logic
- A FOOLish encoding of the next state relations of imperative programs
- MædMax: a maximal ordered completion tool
- ATPboost: learning premise selection in binary setting with ATP feedback
- An abstraction-refinement framework for reasoning with large theories
- Some group theoretic examples with completion theorem provers
- ETPS
- ASASP
- FINDER
This page was built for software: TPTP
