Packages tagged theorem-provers

48 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (36), bsd3 (25), program (18), formal-methods (17), smt (12), math (9), symbolic-computation (8), gpl (7), deprecated (6), logic (6), 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
Folly450.0A first order logic library in Haskell (bsd3, library, program, theorem-provers)2015-10-03dillonhuff
HTab200.0Tableau based theorem prover for hybrid logics (bsd3, program, theorem-provers)2020-05-15GuillaumeHoffmann
atp40.0Interface to automated theorem provers (formal-methods, gpl, library, logic, math, theorem-provers)2021-01-25EK
atp-haskell270.0Translation from Ocaml to Haskell of John Harrison's ATP code (bsd3, library, logic, theorem-provers)2016-09-12DavidFox
bindings-yices240.0Bindings to the Yices theorem prover (ffi, foreign, library, public-domain, theorem-provers)2015-08-22PepeIborra
boolector390.0Haskell bindings for the Boolector SMT solver (bit-vectors, formal-methods, library, math, mit, smt, theorem-provers)2020-08-20DeianStefan
dedukti340.0A type-checker for the λΠ-modulo calculus. (compilers-interpreters, library, program, theorem-provers)2011-04-08MathieuBoespflug
haskhol-core50.0The core logical system of HaskHOL, an EDSL for HOL theorem proving. (bsd3, library, theorem-provers)2015-02-17EvanAustin
hgen40.0Random generation of modal and hybrid logic formulas (program, theorem-provers)2012-07-05GuillaumeHoffmann
htaut92.0Tautology Proving Logic in Haskell (bsd3, library, theorem-provers)2016-09-26Ailrun
hylolib370.0Tools for hybrid logics related programs (library, theorem-provers)2019-04-25GuillaumeHoffmann
hylotab70.0Tableau based theorem prover for hybrid logics (program, theorem-provers)2012-07-05GuillaumeHoffmann
hyloutils70.0Very small programs for hybrid logics (program, theorem-provers)2012-07-05GuillaumeHoffmann
hz3 (deprecated)90.0Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, deprecated, formal-methods, library, math, smt, theorem-provers)2019-10-01
ivor (deprecated in favor of idris)150.0Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)2011-06-16EdwinBrady, GwernBranwen
logic-TPTP800.0Import, export etc. for TPTP, a syntax for first-order logic (codec, library, math, theorem-provers)2020-02-28DanielSchuessler, KiYungAhn, MasahiroSakai
logic-classes370.0Framework for propositional and first order logic, theorem proving (bsd3, library, logic, theorem-provers)2016-09-18DavidFox
mprover70.0Simple equational reasoning for a Haskell-ish language (bsd3, program, theorem-provers)2011-12-15AdamProcter
pesca80.0Proof Editor for Sequent Calculus (compilers-interpreters, program, theorem-provers)2008-05-20GwernBranwen, dpeteler
qed20.0Simple prover (bsd3, library, theorem-provers)2015-11-03NeilMitchell
sbv5092.75SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2021-08-18LeventErkok
sbvPlugin220.0Formally prove properties of Haskell programs using SBV/SMT (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)2021-03-22LeventErkok
scyther-proof350.0Automatic generation of Isabelle/HOL correctness proofs for security protocols. (program, security, theorem-provers)2015-06-21SimonMeier, lochbihl
smtlib2182.0A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-05HenningGuenther
smtlib2-debug90.0Dump the communication with an SMT solver for debugging purposes. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-05HenningGuenther
smtlib2-pipe70.0A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-05HenningGuenther
smtlib2-quickcheck80.0Helper functions to create SMTLib expressions in QuickCheck (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-06HenningGuenther
smtlib2-timing60.0Get timing informations for SMT queries (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)2017-01-07HenningGuenther
structural-induction140.0Instantiate structural induction schemas for algebraic data types (lgpl, library, logic, theorem-provers)2015-06-30DanRosen
tableaux100.0An interactive theorem prover based on semantic tableaux (bsd3, program, theorem-provers)2013-04-05PedroVasconcelos
tamarin-prover (deprecated)370.0The Tamarin prover for security protocol analysis. (deprecated, program, theorem-provers)2015-09-07BenediktSchmidt, SimonMeier
tamarin-prover-term (deprecated)300.0Term manipulation library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-07BenediktSchmidt, SimonMeier
tamarin-prover-theory (deprecated)130.0Term manipulation library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-16BenediktSchmidt, SimonMeier
tamarin-prover-utils (deprecated)260.0Utility library for the tamarin prover. (deprecated, library, theorem-provers)2014-02-07BenediktSchmidt, SimonMeier
theoremquest70.0A common library for TheoremQuest, a theorem proving game. (bsd3, formal-methods, game, library, theorem-provers)2011-02-28TomHawkins
theoremquest-client70.0A simple client for the TheoremQuest theorem proving game. (bsd3, formal-methods, game, program, theorem-provers)2011-02-28TomHawkins
tip-haskell-frontend110.0Convert from Haskell to Tip (bsd3, library, program, theorem-provers)2015-10-28DanRosen
tip-lib220.0tons of inductive problems - support library and tools (bsd3, library, program, theorem-provers)2015-12-15DanRosen
toysolver4510.0Assorted decision procedures for SAT, SMT, Max-SAT, PB, MIP, etc (algorithms, bsd3, constraints, formal-methods, library, logic, optimisation, optimization, program, smt, theorem-provers)2021-02-10MasahiroSakai
tptp240.0Parser and pretty printer for the TPTP language (formal-methods, gpl, language, library, parsing, pretty-printer, theorem-provers)2021-01-11EK
twee200.0An equational theorem prover (bsd3, program, theorem-provers)2021-07-11NickSmallbone
twee-lib500.0An equational theorem prover (bsd3, library, theorem-provers)2021-07-11NickSmallbone
what4982.25Solver-agnostic symbolic values support for issuing queries (bsd3, formal-methods, library, program, smt, symbolic-computation, theorem-provers)2021-06-16RobertDockins
yices-easy80.0Simple interface to the Yices SMT (SAT modulo theories) solver. (algorithms, bsd3, library, math, theorem-provers)2010-09-29KeeganMcAllister
yices-painless100.0An embedded language for programming the Yices SMT solver (bsd3, formal-methods, library, math, theorem-provers)2011-01-17DonaldStewart
z3442.25Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers)2020-08-29IagoAbal
zeno90.0An automated proof system for Haskell programs (mit, program, theorem-provers)2011-04-28WilliamSonnex
zsyntax60.0Automated theorem prover for the Zsyntax biochemical calculus (bioinformatics, bsd3, library, logic, theorem-provers)2018-12-15fsestini