Packages tagged theorem-provers
52 packages have this tag.
[Merge tag] (trustees only)Related tags: library (40), bsd3 (27), formal-methods (21), program (20), smt (14), math (11), symbolic-computation (10), gpl (7), deprecated (6), logic (6), bit-vectors (4), algorithms (2), compilers-interpreters (2), game (2), mathematics (2), maths (2), mit (2), mpl (2), bioinformatics (1), codec (1), constraints (1), dependent-types (1), ...
Name |
DLs |
Rating |
Rev Deps |
Description |
Tags |
Last U/L |
Last Version |
Maintainers |
|---|---|---|---|---|---|---|---|---|
| Folly | 53 | 0.0 | 1 | A first order logic library in Haskell | (bsd3, library, program, theorem-provers) | 2015-10-03 | 0.2.0.1 | dillonhuff |
| HTab | 26 | 0.0 | 1 | Tableau based theorem prover for hybrid logics | (bsd3, program, theorem-provers) | 2020-05-15 | 1.7.3 | GuillaumeHoffmann |
| LPPaver | 9 | 0.0 | 0 | An automated prover targeting problems that involve nonlinear real arithmetic | (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers, verification) | 2023-03-13 | 0.0.5.0 | JunaidRasheed |
| PropaFP | 8 | 0.0 | 1 | Auto-active verification of floating-point programs | (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers) | 2023-03-12 | 0.1.2.0 | JunaidRasheed |
| atp | 5 | 0.0 | 0 | Interface to automated theorem provers | (formal-methods, gpl, library, logic, math, theorem-provers) | 2021-01-25 | 0.1.0.0 | EK |
| atp-haskell | 21 | 2.0 | 2 | Translation from Ocaml to Haskell of John Harrison's ATP code | (bsd3, library, logic, theorem-provers) | 2024-04-03 | 1.14.3 | DavidFox |
| bindings-yices | 19 | 0.0 | 2 | Bindings to the Yices theorem prover | (ffi, foreign, library, public-domain, theorem-provers) | 2015-08-22 | 0.3.0.2 | PepeIborra |
| boolector | 43 | 0.0 | 1 | Haskell bindings for the Boolector SMT solver | (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers) | 2020-08-20 | 0.0.0.13 | DeianStefan |
| dedukti | 38 | 0.0 | 1 | A type-checker for the λΠ-modulo calculus. | (compilers-interpreters, library, program, theorem-provers) | 2011-04-08 | 1.1.4 | MathieuBoespflug |
| grisette | 50 | 0.0 | 1 | Symbolic evaluation as a library | (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers) | 2024-11-08 | 0.9.0.0 | siruilu |
| grisette-monad-coroutine | 8 | 0.0 | 0 | Support for monad-coroutine package with Grisette | (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers) | 2024-01-10 | 0.2.0.0 | siruilu |
| haskhol-core | 6 | 0.0 | 1 | The core logical system of HaskHOL, an EDSL for HOL theorem proving. | (bsd3, library, theorem-provers) | 2015-02-17 | 1.1.0 | EvanAustin |
| hgen | 9 | 0.0 | 1 | Random generation of modal and hybrid logic formulas | (program, theorem-provers) | 2012-07-05 | 1.4.0 | GuillaumeHoffmann |
| htaut | 8 | 2.0 | 1 | Tautology Proving Logic in Haskell | (bsd3, library, theorem-provers) | 2016-09-26 | 0.1.1.0 | Ailrun |
| hylolib | 27 | 0.0 | 1 | Tools for hybrid logics related programs | (library, theorem-provers) | 2019-04-25 | 1.5.4 | GuillaumeHoffmann |
| hylotab | 9 | 0.0 | 1 | Tableau based theorem prover for hybrid logics | (program, theorem-provers) | 2012-07-05 | 1.2.1 | GuillaumeHoffmann |
| hyloutils | 4 | 0.0 | 1 | Very small programs for hybrid logics | (program, theorem-provers) | 2012-07-05 | 1.0 | GuillaumeHoffmann |
| hz3 (deprecated) | 12 | 0.0 | 0 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers) | 2019-10-01 | 96.0.0.0 | |
| ivor (deprecated in favor of idris) | 28 | 0.0 | 2 | Theorem proving library based on dependent type theory | (bsd3, dependent-types, deprecated, library, theorem-provers) | 2011-06-16 | 0.1.14.1 | EdwinBrady, GwernBranwen |
| logic-TPTP | 70 | 0.0 | 1 | Import, export etc. for TPTP, a syntax for first-order logic | (codec, library, math, theorem-provers) | 2024-11-09 | 0.6.0.0 | DanielSchuessler, KiYungAhn, MasahiroSakai |
| logic-classes | 49 | 0.0 | 1 | Framework for propositional and first order logic, theorem proving | (bsd3, library, logic, theorem-provers) | 2016-09-18 | 1.7.1 | DavidFox |
| mprover | 6 | 0.0 | 1 | Simple equational reasoning for a Haskell-ish language | (bsd3, program, theorem-provers) | 2011-12-15 | 0.0.0.0 | AdamProcter |
| pesca | 9 | 0.0 | 1 | Proof Editor for Sequent Calculus | (compilers-interpreters, program, theorem-provers) | 2008-05-20 | 4.0.1 | GwernBranwen, dpeteler, mmhat |
| qed | 5 | 0.0 | 1 | Simple prover | (bsd3, library, theorem-provers) | 2015-11-03 | 0.0 | NeilMitchell |
| sbv | 671 | 2.75 | 12 | SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. | (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2024-11-07 | 11.0 | LeventErkok |
| sbvPlugin | 62 | 0.0 | 1 | Formally prove properties of Haskell programs using SBV/SMT | (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers) | 2024-05-22 | 9.10.1 | LeventErkok |
| scyther-proof | 32 | 0.0 | 1 | Automatic generation of Isabelle/HOL correctness proofs for security protocols. | (program, security, theorem-provers) | 2015-06-21 | 0.10.0.1 | SimonMeier, lochbihl |
| smtlib2 | 17 | 2.0 | 6 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-debug | 5 | 0.0 | 1 | Dump the communication with an SMT solver for debugging purposes. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-pipe | 6 | 0.0 | 1 | A type-safe interface to communicate with an SMT solver. | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-05 | 1.0 | HenningGuenther |
| smtlib2-quickcheck | 4 | 0.0 | 1 | Helper functions to create SMTLib expressions in QuickCheck | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-06 | 1.0 | HenningGuenther |
| smtlib2-timing | 5 | 0.0 | 1 | Get timing informations for SMT queries | (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers) | 2017-01-07 | 1.0 | HenningGuenther |
| structural-induction | 23 | 0.0 | 2 | Instantiate structural induction schemas for algebraic data types | (lgpl, library, logic, theorem-provers) | 2015-06-30 | 0.3 | DanRosen |
| tableaux | 12 | 0.0 | 1 | An interactive theorem prover based on semantic tableaux | (bsd3, program, theorem-provers) | 2023-07-21 | 0.3 | PedroVasconcelos |
| tamarin-prover (deprecated) | 82 | 0.0 | 1 | The Tamarin prover for security protocol analysis. | (deprecated, program, theorem-provers) | 2015-09-07 | 0.8.6.3 | BenediktSchmidt, SimonMeier |
| tamarin-prover-term (deprecated) | 37 | 0.0 | 2 | Term manipulation library for the tamarin prover. | (deprecated, library, theorem-provers) | 2014-02-07 | 0.8.5.1 | BenediktSchmidt, SimonMeier |
| tamarin-prover-theory (deprecated) | 18 | 0.0 | 1 | Term manipulation library for the tamarin prover. | (deprecated, library, theorem-provers) | 2014-02-16 | 0.8.6.0 | BenediktSchmidt, SimonMeier |
| tamarin-prover-utils (deprecated) | 30 | 0.0 | 3 | Utility library for the tamarin prover. | (deprecated, library, theorem-provers) | 2014-02-07 | 0.8.5.1 | BenediktSchmidt, SimonMeier |
| theoremquest | 6 | 0.0 | 1 | A common library for TheoremQuest, a theorem proving game. | (bsd3, formal-methods, game, library, theorem-provers) | 2011-02-28 | 0.0.0 | TomHawkins |
| theoremquest-client | 3 | 0.0 | 1 | A simple client for the TheoremQuest theorem proving game. | (bsd3, formal-methods, game, program, theorem-provers) | 2011-02-28 | 0.0.0 | TomHawkins |
| tip-haskell-frontend | 14 | 0.0 | 0 | Convert from Haskell to Tip | (bsd3, library, program, theorem-provers) | 2015-10-28 | 0.2 | DanRosen |
| tip-lib | 15 | 0.0 | 1 | tons of inductive problems - support library and tools | (bsd3, library, program, theorem-provers) | 2015-12-15 | 0.2.2 | DanRosen |
| toysolver | 32 | 0.0 | 4 | Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc | (algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, smt, theorem-provers) | 2022-09-17 | 0.8.1 | MasahiroSakai |
| tptp | 22 | 0.0 | 1 | Parser and pretty printer for the TPTP language | (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers) | 2021-01-11 | 0.1.3.0 | EK |
| twee | 62 | 0.0 | 1 | An equational theorem prover | (bsd3, program, theorem-provers) | 2022-09-15 | 2.4.2 | NickSmallbone |
| twee-lib | 61 | 0.0 | 1 | An equational theorem prover | (bsd3, library, theorem-provers) | 2022-09-15 | 2.4.2 | NickSmallbone |
| what4 | 108 | 2.25 | 8 | Solver-agnostic symbolic values support for issuing queries | (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers) | 2024-09-23 | 1.6.2 | RobertDockins, ryanglscott, galoisinc, mccleeary |
| yices-easy | 3 | 0.0 | 1 | Simple interface to the Yices SMT (SAT modulo theories) solver. | (algorithms, bsd3, library, math, theorem-provers) | 2010-09-29 | 0.1 | KeeganMcAllister |
| yices-painless | 10 | 0.0 | 1 | An embedded language for programming the Yices SMT solver | (bsd3, formal-methods, library, math, theorem-provers) | 2011-01-17 | 0.1.2 | DonaldStewart |
| z3 | 63 | 2.25 | 6 | Bindings for the Z3 Theorem Prover | (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers) | 2020-08-29 | 408.2 | IagoAbal |
| zeno | 9 | 0.0 | 1 | An automated proof system for Haskell programs | (mit, program, theorem-provers) | 2011-04-28 | 0.2.0.1 | WilliamSonnex |
| zsyntax | 5 | 0.0 | 0 | Automated theorem prover for the Zsyntax biochemical calculus | (bioinformatics, bsd3, library, logic, theorem-provers) | 2018-12-15 | 0.2.0.0 | fsestini |