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
Folly220.01A first order logic library in Haskell (bsd3, library, program, theorem-provers)2015-10-030.2.0.1dillonhuff
HTab270.01Tableau based theorem prover for hybrid logics (bsd3, program, theorem-provers)2020-05-151.7.3GuillaumeHoffmann
LPPaver60.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
PropaFP70.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-haskell142.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
boolector80.01Haskell bindings for the Boolector SMT solver (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers)2020-08-200.0.0.13DeianStefan
dedukti110.01A type-checker for the λΠ-modulo calculus. (compilers-interpreters, library, program, theorem-provers)2011-04-081.1.4MathieuBoespflug
grisette270.01Symbolic evaluation as a library (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-08-140.8.0.0siruilu
grisette-monad-coroutine40.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
htaut72.01Tautology Proving Logic in Haskell (bsd3, library, theorem-provers)2016-09-260.1.1.0Ailrun
hylolib240.01Tools for hybrid logics related programs (library, theorem-provers)2019-04-251.5.4GuillaumeHoffmann
hylotab40.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)40.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-TPTP680.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-classes410.01Framework for propositional and first order logic, theorem proving (bsd3, library, logic, theorem-provers)2016-09-181.7.1DavidFox
mprover30.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
sbv3972.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
sbvPlugin420.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-proof150.01Automatic generation of Isabelle/HOL correctness proofs for security protocols. (program, security, theorem-provers)2015-06-210.10.0.1SimonMeier, lochbihl
smtlib272.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-pipe30.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
tableaux110.01An interactive theorem prover based on semantic tableaux (bsd3, program, theorem-provers)2023-07-210.3PedroVasconcelos
tamarin-prover (deprecated)330.01The Tamarin prover for security protocol analysis. (deprecated, program, theorem-provers)2015-09-070.8.6.3BenediktSchmidt, SimonMeier
tamarin-prover-term (deprecated)190.02Term manipulation library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-070.8.5.1BenediktSchmidt, SimonMeier
tamarin-prover-theory (deprecated)110.01Term manipulation library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-160.8.6.0BenediktSchmidt, SimonMeier
tamarin-prover-utils (deprecated)190.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-frontend70.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
toysolver290.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
tptp90.01Parser and pretty printer for the TPTP language (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers)2021-01-110.1.3.0EK
twee280.01An equational theorem prover (bsd3, program, theorem-provers)2022-09-152.4.2NickSmallbone
twee-lib340.01An equational theorem prover (bsd3, library, theorem-provers)2022-09-152.4.2NickSmallbone
what4852.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-easy20.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
z3302.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