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
Folly260.01A first order logic library in Haskell (bsd3, library, program, theorem-provers)2015-10-030.2.0.1dillonhuff
HTab230.01Tableau based theorem prover for hybrid logics (bsd3, program, theorem-provers)2020-05-151.7.3GuillaumeHoffmann
LPPaver80.00An automated prover targeting problems that involve nonlinear real arithmetic (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers, verification)2023-03-130.0.5.0JunaidRasheed
PropaFP90.01Auto-active verification of floating-point programs (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers)2023-03-120.1.2.0JunaidRasheed
atp30.00Interface to automated theorem provers (formal-methods, gpl, library, logic, math, theorem-provers)2021-01-250.1.0.0EK
atp-haskell162.02Translation from Ocaml to Haskell of John Harrison's ATP code (bsd3, library, logic, theorem-provers)2024-04-031.14.3DavidFox
bindings-yices50.02Bindings to the Yices theorem prover (ffi, foreign, library, public-domain, theorem-provers)2015-08-220.3.0.2PepeIborra
boolector90.01Haskell bindings for the Boolector SMT solver (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers)2020-08-200.0.0.13DeianStefan
dedukti120.01A type-checker for the λΠ-modulo calculus. (compilers-interpreters, library, program, theorem-provers)2011-04-081.1.4MathieuBoespflug
grisette240.01Symbolic evaluation as a library (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-08-140.8.0.0siruilu
grisette-monad-coroutine30.00Support for monad-coroutine package with Grisette (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-01-100.2.0.0siruilu
haskhol-core40.01The core logical system of HaskHOL, an EDSL for HOL theorem proving. (bsd3, library, theorem-provers)2015-02-171.1.0EvanAustin
hgen80.01Random generation of modal and hybrid logic formulas (program, theorem-provers)2012-07-051.4.0GuillaumeHoffmann
htaut82.01Tautology Proving Logic in Haskell (bsd3, library, theorem-provers)2016-09-260.1.1.0Ailrun
hylolib250.01Tools for hybrid logics related programs (library, theorem-provers)2019-04-251.5.4GuillaumeHoffmann
hylotab30.01Tableau based theorem prover for hybrid logics (program, theorem-provers)2012-07-051.2.1GuillaumeHoffmann
hyloutils20.01Very small programs for hybrid logics (program, theorem-provers)2012-07-051.0GuillaumeHoffmann
hz3 (deprecated)50.00Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers)2019-10-0196.0.0.0
ivor (deprecated in favor of idris)160.02Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)2011-06-160.1.14.1EdwinBrady, GwernBranwen
logic-TPTP540.01Import, export etc. for TPTP, a syntax for first-order logic (codec, library, math, theorem-provers)2024-09-040.5.1.0DanielSchuessler, KiYungAhn, MasahiroSakai
logic-classes450.01Framework for propositional and first order logic, theorem proving (bsd3, library, logic, theorem-provers)2016-09-181.7.1DavidFox
mprover20.01Simple equational reasoning for a Haskell-ish language (bsd3, program, theorem-provers)2011-12-150.0.0.0AdamProcter
pesca40.01Proof Editor for Sequent Calculus (compilers-interpreters, program, theorem-provers)2008-05-204.0.1GwernBranwen, dpeteler, mmhat
qed30.01Simple prover (bsd3, library, theorem-provers)2015-11-030.0NeilMitchell
sbv3712.7512SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2024-08-1110.12LeventErkok
sbvPlugin470.01Formally prove properties of Haskell programs using SBV/SMT (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2024-05-229.10.1LeventErkok
scyther-proof130.01Automatic generation of Isabelle/HOL correctness proofs for security protocols. (program, security, theorem-provers)2015-06-210.10.0.1SimonMeier, lochbihl
smtlib292.06A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-debug30.01Dump the communication with an SMT solver for debugging purposes. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-pipe40.01A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-quickcheck20.01Helper functions to create SMTLib expressions in QuickCheck (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-061.0HenningGuenther
smtlib2-timing10.01Get timing informations for SMT queries (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-071.0HenningGuenther
structural-induction100.02Instantiate structural induction schemas for algebraic data types (lgpl, library, logic, theorem-provers)2015-06-300.3DanRosen
tableaux130.01An interactive theorem prover based on semantic tableaux (bsd3, program, theorem-provers)2023-07-210.3PedroVasconcelos
tamarin-prover (deprecated)360.01The Tamarin prover for security protocol analysis. (deprecated, program, theorem-provers)2015-09-070.8.6.3BenediktSchmidt, SimonMeier
tamarin-prover-term (deprecated)200.02Term manipulation library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-070.8.5.1BenediktSchmidt, SimonMeier
tamarin-prover-theory (deprecated)100.01Term manipulation library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-160.8.6.0BenediktSchmidt, SimonMeier
tamarin-prover-utils (deprecated)210.03Utility library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-070.8.5.1BenediktSchmidt, SimonMeier
theoremquest10.01A common library for TheoremQuest, a theorem proving game. (bsd3, formal-methods, game, library, theorem-provers)2011-02-280.0.0TomHawkins
theoremquest-client10.01A simple client for the TheoremQuest theorem proving game. (bsd3, formal-methods, game, program, theorem-provers)2011-02-280.0.0TomHawkins
tip-haskell-frontend60.00Convert from Haskell to Tip (bsd3, library, program, theorem-provers)2015-10-280.2DanRosen
tip-lib130.01tons of inductive problems - support library and tools (bsd3, library, program, theorem-provers)2015-12-150.2.2DanRosen
toysolver310.04Assorted 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-170.8.1MasahiroSakai
tptp110.01Parser and pretty printer for the TPTP language (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers)2021-01-110.1.3.0EK
twee300.01An equational theorem prover (bsd3, program, theorem-provers)2022-09-152.4.2NickSmallbone
twee-lib360.01An equational theorem prover (bsd3, library, theorem-provers)2022-09-152.4.2NickSmallbone
what4932.258Solver-agnostic symbolic values support for issuing queries (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers)2024-09-231.6.2RobertDockins, ryanglscott, galoisinc, mccleeary
yices-easy30.01Simple interface to the Yices SMT (SAT modulo theories) solver. (algorithms, bsd3, library, math, theorem-provers)2010-09-290.1KeeganMcAllister
yices-painless60.01An embedded language for programming the Yices SMT solver (bsd3, formal-methods, library, math, theorem-provers)2011-01-170.1.2DonaldStewart
z3342.256Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers)2020-08-29408.2IagoAbal
zeno30.01An automated proof system for Haskell programs (mit, program, theorem-provers)2011-04-280.2.0.1WilliamSonnex
zsyntax20.00Automated theorem prover for the Zsyntax biochemical calculus (bioinformatics, bsd3, library, logic, theorem-provers)2018-12-150.2.0.0fsestini