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
HTab160.01Tableau based theorem prover for hybrid logics (bsd3, program, theorem-provers)2020-05-151.7.3GuillaumeHoffmann
LPPaver40.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
PropaFP50.01Auto-active verification of floating-point programs (formal-methods, library, math, mathematics, maths, mpl, program, theorem-provers)2023-03-120.1.2.0JunaidRasheed
atp50.00Interface to automated theorem provers (formal-methods, gpl, library, logic, math, theorem-provers)2021-01-250.1.0.0EK
atp-haskell452.02Translation from Ocaml to Haskell of John Harrison's ATP code (bsd3, library, logic, theorem-provers)2024-03-161.14.2DavidFox
bindings-yices100.02Bindings to the Yices theorem prover (ffi, foreign, library, public-domain, theorem-provers)2015-08-220.3.0.2PepeIborra
boolector170.01Haskell bindings for the Boolector SMT solver (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers)2020-08-200.0.0.13DeianStefan
dedukti290.01A type-checker for the λΠ-modulo calculus. (compilers-interpreters, library, program, theorem-provers)2011-04-081.1.4MathieuBoespflug
grisette260.01Symbolic evaluation as a library (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-01-100.4.1.0siruilu
grisette-monad-coroutine80.00Support for monad-coroutine package with Grisette (bsd3, formal-methods, library, smt, symbolic-computation, theorem-provers)2024-01-100.2.0.0siruilu
haskhol-core50.01The core logical system of HaskHOL, an EDSL for HOL theorem proving. (bsd3, library, theorem-provers)2015-02-171.1.0EvanAustin
hgen60.01Random generation of modal and hybrid logic formulas (program, theorem-provers)2012-07-051.4.0GuillaumeHoffmann
htaut172.01Tautology Proving Logic in Haskell (bsd3, library, theorem-provers)2016-09-260.1.1.0Ailrun
hylolib140.01Tools for hybrid logics related programs (library, theorem-provers)2019-04-251.5.4GuillaumeHoffmann
hylotab80.01Tableau based theorem prover for hybrid logics (program, theorem-provers)2012-07-051.2.1GuillaumeHoffmann
hyloutils50.01Very small programs for hybrid logics (program, theorem-provers)2012-07-051.0GuillaumeHoffmann
hz3 (deprecated)110.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)150.02Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)2011-06-160.1.14.1EdwinBrady, GwernBranwen
logic-TPTP520.01Import, export etc. for TPTP, a syntax for first-order logic (codec, library, math, theorem-provers)2020-02-280.5.0.0DanielSchuessler, KiYungAhn, MasahiroSakai
logic-classes300.01Framework for propositional and first order logic, theorem proving (bsd3, library, logic, theorem-provers)2016-09-181.7.1DavidFox
mprover50.01Simple equational reasoning for a Haskell-ish language (bsd3, program, theorem-provers)2011-12-150.0.0.0AdamProcter
pesca90.01Proof Editor for Sequent Calculus (compilers-interpreters, program, theorem-provers)2008-05-204.0.1GwernBranwen, dpeteler, mmhat
qed40.01Simple prover (bsd3, library, theorem-provers)2015-11-030.0NeilMitchell
sbv3772.7512SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2024-03-1610.6LeventErkok
sbvPlugin260.01Formally prove properties of Haskell programs using SBV/SMT (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2024-01-069.8.1LeventErkok
scyther-proof280.01Automatic generation of Isabelle/HOL correctness proofs for security protocols. (program, security, theorem-provers)2015-06-210.10.0.1SimonMeier, lochbihl
smtlib2122.06A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-051.0HenningGuenther
smtlib2-debug40.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-quickcheck40.01Helper functions to create SMTLib expressions in QuickCheck (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-061.0HenningGuenther
smtlib2-timing40.01Get timing informations for SMT queries (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-071.0HenningGuenther
structural-induction120.02Instantiate structural induction schemas for algebraic data types (lgpl, library, logic, theorem-provers)2015-06-300.3DanRosen
tableaux90.01An interactive theorem prover based on semantic tableaux (bsd3, program, theorem-provers)2023-07-210.3PedroVasconcelos
tamarin-prover (deprecated)250.01The Tamarin prover for security protocol analysis. (deprecated, program, theorem-provers)2015-09-070.8.6.3BenediktSchmidt, SimonMeier
tamarin-prover-term (deprecated)150.02Term manipulation library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-070.8.5.1BenediktSchmidt, SimonMeier
tamarin-prover-theory (deprecated)90.01Term manipulation library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-160.8.6.0BenediktSchmidt, SimonMeier
tamarin-prover-utils (deprecated)160.03Utility library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-070.8.5.1BenediktSchmidt, SimonMeier
theoremquest60.01A common library for TheoremQuest, a theorem proving game. (bsd3, formal-methods, game, library, theorem-provers)2011-02-280.0.0TomHawkins
theoremquest-client50.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-lib110.01tons of inductive problems - support library and tools (bsd3, library, program, theorem-provers)2015-12-150.2.2DanRosen
toysolver190.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
tptp120.01Parser and pretty printer for the TPTP language (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers)2021-01-110.1.3.0EK
twee430.01An equational theorem prover (bsd3, program, theorem-provers)2022-09-152.4.2NickSmallbone
twee-lib450.01An equational theorem prover (bsd3, library, theorem-provers)2022-09-152.4.2NickSmallbone
what4612.252Solver-agnostic symbolic values support for issuing queries (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers)2023-10-131.5.1RobertDockins, ryanglscott, galoisinc
yices-easy80.01Simple interface to the Yices SMT (SAT modulo theories) solver. (algorithms, bsd3, library, math, theorem-provers)2010-09-290.1KeeganMcAllister
yices-painless100.01An embedded language for programming the Yices SMT solver (bsd3, formal-methods, library, math, theorem-provers)2011-01-170.1.2DonaldStewart
z3682.256Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers)2020-08-29408.2IagoAbal
zeno100.01An automated proof system for Haskell programs (mit, program, theorem-provers)2011-04-280.2.0.1WilliamSonnex
zsyntax50.00Automated theorem prover for the Zsyntax biochemical calculus (bioinformatics, bsd3, library, logic, theorem-provers)2018-12-150.2.0.0fsestini