# Packages tagged theorem-provers

46 packages have this tag.

[Merge tag] (trustees only)Related tags: library (34), bsd3 (24), program (17), formal-methods (15), smt (11), math (8), symbolic-computation (7), gpl (6), deprecated (5), logic (5), bit-vectors (4), algorithms (2), compilers-interpreters (2), game (2), mit (2), bioinformatics (1), codec (1), constraints (1), dependent-types (1), ...

Name |
DLs |
Rating |
Description |
Tags |
Last U/L |
Maintainer |
---|---|---|---|---|---|---|

Folly | 462 | 0.0 | A first order logic library in Haskell | (bsd3, library, program, theorem-provers) | 2015-10-03 | dillonhuff |

HTab | 253 | 0.0 | Tableau based theorem prover for hybrid logics | (bsd3, program, theorem-provers) | 2019-04-25 | GuillaumeHoffmann |

atp-haskell | 227 | 0.0 | Translation from Ocaml to Haskell of John Harrison's ATP code | (bsd3, library, logic, theorem-provers) | 2016-09-12 | DavidFox |

bindings-yices | 120 | 0.0 | Bindings to the Yices theorem prover | (ffi, foreign, library, public-domain, theorem-provers) | 2015-08-22 | PepeIborra |

boolector | 423 | 0.0 | Haskell bindings for the Boolector SMT solver | (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers) | 2020-02-08 | DeianStefan |

dedukti | 344 | 0.0 | A type-checker for the λΠ-modulo calculus. | (compilers-interpreters, library, program, theorem-provers) | 2011-04-08 | MathieuBoespflug |

haskhol-core | 77 | 0.0 | The core logical system of HaskHOL, an EDSL for HOL theorem proving. | (bsd3, library, theorem-provers) | 2015-02-17 | EvanAustin |

hgen | 39 | 0.0 | Random generation of modal and hybrid logic formulas | (program, theorem-provers) | 2012-07-05 | GuillaumeHoffmann |

htaut | 59 | 0.0 | Tautology Proving Logic in Haskell | (bsd3, library, theorem-provers) | 2016-09-26 | Ailrun |

hylolib | 338 | 0.0 | Tools for hybrid logics related programs | (library, theorem-provers) | 2019-04-25 | GuillaumeHoffmann |

hylotab | 74 | 0.0 | Tableau based theorem prover for hybrid logics | (program, theorem-provers) | 2012-07-05 | GuillaumeHoffmann |

hyloutils | 32 | 0.0 | Very small programs for hybrid logics | (program, theorem-provers) | 2012-07-05 | GuillaumeHoffmann |

hz3 | 52 | 0.0 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers) | 2019-10-01 | MatthewFarkasDyck |

ivor (deprecated in favor of idris) | 289 | 0.0 | Theorem proving library based on dependent type theory | (bsd3, dependent-types, deprecated, library, theorem-provers) | 2011-06-16 | EdwinBrady, GwernBranwen |

logic-TPTP | 750 | 0.0 | Import, export etc. for TPTP, a syntax for first-order logic | (codec, library, math, theorem-provers) | 2020-02-16 | DanielSchuessler, KiYungAhn, MasahiroSakai |

logic-classes | 588 | 0.0 | Framework for propositional and first order logic, theorem proving | (bsd3, library, logic, theorem-provers) | 2016-09-18 | DavidFox |

mprover | 25 | 0.0 | Simple equational reasoning for a Haskell-ish language | (bsd3, program, theorem-provers) | 2011-12-15 | AdamProcter |

pesca | 98 | 0.0 | Proof Editor for Sequent Calculus | (compilers-interpreters, program, theorem-provers) | 2008-05-20 | GwernBranwen, dpeteler |

qed | 25 | 0.0 | Simple prover | (bsd3, library, theorem-provers) | 2015-11-03 | NeilMitchell |

sbv | 1863 | 2.75 | SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. | (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2020-02-09 | LeventErkok |

sbvPlugin | 152 | 0.0 | Formally prove properties of Haskell programs using SBV/SMT | (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2019-01-15 | LeventErkok |

scyther-proof | 287 | 0.0 | Automatic generation of Isabelle/HOL correctness proofs for security protocols. | (program, security, theorem-provers) | 2015-06-21 | SimonMeier, lochbihl |

smtlib2 | 167 | 2.0 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | HenningGuenther |

smtlib2-debug | 47 | 0.0 | Dump the communication with an SMT solver for debugging purposes. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | HenningGuenther |

smtlib2-pipe | 41 | 0.0 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | HenningGuenther |

smtlib2-quickcheck | 53 | 0.0 | Helper functions to create SMTLib expressions in QuickCheck | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-06 | HenningGuenther |

smtlib2-timing | 42 | 0.0 | Get timing informations for SMT queries | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-07 | HenningGuenther |

structural-induction | 172 | 0.0 | Instantiate structural induction schemas for algebraic data types | (lgpl, library, logic, theorem-provers) | 2015-06-30 | DanRosen |

tableaux | 40 | 0.0 | An interactive theorem prover based on semantic tableaux | (bsd3, program, theorem-provers) | 2013-04-05 | PedroVasconcelos |

tamarin-prover (deprecated) | 565 | 0.0 | The Tamarin prover for security protocol analysis. | (deprecated, program, theorem-provers) | 2015-09-07 | BenediktSchmidt, SimonMeier |

tamarin-prover-term (deprecated) | 358 | 0.0 | Term manipulation library for the tamarin prover. | (deprecated, library, theorem-provers) | 2014-02-07 | BenediktSchmidt, SimonMeier |

tamarin-prover-theory (deprecated) | 145 | 0.0 | Term manipulation library for the tamarin prover. | (deprecated, library, theorem-provers) | 2014-02-16 | BenediktSchmidt, SimonMeier |

tamarin-prover-utils (deprecated) | 332 | 0.0 | Utility library for the tamarin prover. | (deprecated, library, theorem-provers) | 2014-02-07 | BenediktSchmidt, SimonMeier |

theoremquest | 46 | 0.0 | A common library for TheoremQuest, a theorem proving game. | (bsd3, formal-methods, game, library, theorem-provers) | 2011-02-28 | TomHawkins |

theoremquest-client | 36 | 0.0 | A simple client for the TheoremQuest theorem proving game. | (bsd3, formal-methods, game, program, theorem-provers) | 2011-02-28 | TomHawkins |

tip-haskell-frontend | 89 | 0.0 | Convert from Haskell to Tip | (bsd3, library, program, theorem-provers) | 2015-10-28 | DanRosen |

tip-lib | 204 | 0.0 | tons of inductive problems - support library and tools | (bsd3, library, program, theorem-provers) | 2015-12-15 | DanRosen |

toysolver | 419 | 0.0 | Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc | (algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, smt, theorem-provers) | 2019-10-04 | MasahiroSakai |

tptp | 202 | 0.0 | A parser and a pretty printer for the TPTP language | (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers) | 2019-12-07 | EK |

twee | 389 | 0.0 | An equational theorem prover | (bsd3, program, theorem-provers) | 2020-02-21 | NickSmallbone |

twee-lib | 277 | 0.0 | An equational theorem prover | (bsd3, library, theorem-provers) | 2020-02-21 | NickSmallbone |

yices-easy | 26 | 0.0 | Simple interface to the Yices SMT (SAT modulo theories) solver. | (algorithms, bsd3, library, math, theorem-provers) | 2010-09-29 | KeeganMcAllister |

yices-painless | 118 | 0.0 | An embedded language for programming the Yices SMT solver | (bsd3, formal-methods, library, math, theorem-provers) | 2011-01-17 | DonaldStewart |

z3 | 509 | 2.25 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers) | 2020-01-16 | IagoAbal |

zeno | 62 | 0.0 | An automated proof system for Haskell programs | (mit, program, theorem-provers) | 2011-04-28 | WilliamSonnex |

zsyntax | 16 | 0.0 | Automated theorem prover for the Zsyntax biochemical calculus | (bioinformatics, bsd3, library, logic, theorem-provers) | 2018-12-15 | fsestini |