Packages tagged theorem-provers

41 packages have this tag.

[Merge tag] (trustees only)

Related tags: library (30), bsd3 (20), gpl (18), program (17), formal-methods (11), smt (8), symbolic-computation (7), math (6), deprecated (5), logic (4), algorithms (2), bit-vectors (2), compilers-interpreters (2), game (2), benchmark (1), codec (1), constraints (1), ...

Name
DLs
Rating
Description
Tags
Maintainer
Folly170.0A first order logic library in Haskell (bsd3, library, program, theorem-provers)dillonhuff
HTab120.0Tableau based theorem prover for hybrid logics (gpl, program, theorem-provers)GuillaumeHoffmann
atp-haskell100.0Translation from Ocaml to Haskell of John Harrison's ATP code (bsd3, library, logic, theorem-provers)DavidFox
bindings-yices90.0Bindings to the Yices theorem prover (ffi, foreign, library, public-domain, theorem-provers)PepeIborra
dedukti190.0A type-checker for the λΠ-modulo calculus. (compilers-interpreters, gpl, library, program, theorem-provers)MathieuBoespflug
haskhol-core40.0The core logical system of HaskHOL, an EDSL for HOL theorem proving. (bsd3, library, theorem-provers)EvanAustin
hgen40.0Random generation of modal and hybrid logic formulas (gpl, program, theorem-provers)GuillaumeHoffmann
htaut40.0Tautology Proving Logic in Haskell (bsd3, library, theorem-provers)Ailrun
hylolib140.0Tools for hybrid logics related programs (gpl, library, theorem-provers)GuillaumeHoffmann
hylotab30.0Tableau based theorem prover for hybrid logics (gpl, program, theorem-provers)GuillaumeHoffmann
hyloutils10.0Very small programs for hybrid logics (gpl, program, theorem-provers)GuillaumeHoffmann
ivor (deprecated in favor of idris)180.0Theorem proving library based on dependent type theory (bsd3, dependent-types, deprecated, library, theorem-provers)EdwinBrady, GwernBranwen
logic-TPTP1370.0Import, export etc. for TPTP, a syntax for first-order logic (codec, gpl, library, math, theorem-provers)DanielSchuessler, KiYungAhn
logic-classes210.0Framework for propositional and first order logic, theorem proving (bsd3, library, logic, theorem-provers)DavidFox
mprover20.0Simple equational reasoning for a Haskell-ish language (bsd3, program, theorem-provers)AdamProcter
pesca60.0Proof Editor for Sequent Calculus (compilers-interpreters, gpl, program, theorem-provers)GwernBranwen
qed20.0Simple prover (bsd3, library, theorem-provers)NeilMitchell
sbv1942.5SMT Based Verification: Symbolic Haskell theorem prover using SMT solving. (bit-vectors, bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)LeventErkok
sbvPlugin180.0Formally prove properties of Haskell programs using SBV/SMT (bsd3, formal-methods, library, math, smt, symbolic-computation, theorem-provers)LeventErkok
scyther-proof130.0Automatic generation of Isabelle/HOL correctness proofs for security protocols. (gpl, program, security, theorem-provers)SimonMeier, lochbihl
smtlib2112.0A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)HenningGuenther
smtlib2-debug30.0Dump the communication with an SMT solver for debugging purposes. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)HenningGuenther
smtlib2-pipe30.0A type-safe interface to communicate with an SMT solver. (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)HenningGuenther
smtlib2-quickcheck40.0Helper functions to create SMTLib expressions in QuickCheck (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)HenningGuenther
smtlib2-timing40.0Get timing informations for SMT queries (formal-methods, gpl, library, smt, symbolic-computation, theorem-provers)HenningGuenther
structural-induction100.0Instantiate structural induction schemas for algebraic data types (lgpl, library, logic, theorem-provers)DanRosen
tableaux80.0An interactive theorem prover based on semantic tableaux (bsd3, program, theorem-provers)PedroVasconcelos
tamarin-prover (deprecated)200.0The Tamarin prover for security protocol analysis. (deprecated, gpl, program, theorem-provers)BenediktSchmidt, SimonMeier
tamarin-prover-term (deprecated)100.0Term manipulation library for the tamarin prover. (deprecated, gpl, library, theorem-provers)BenediktSchmidt, SimonMeier
tamarin-prover-theory (deprecated)60.0Term manipulation library for the tamarin prover. (deprecated, gpl, library, theorem-provers)BenediktSchmidt, SimonMeier
tamarin-prover-utils (deprecated)120.0Utility library for the tamarin prover. (deprecated, gpl, library, theorem-provers)BenediktSchmidt, SimonMeier
theoremquest20.0A common library for TheoremQuest, a theorem proving game. (bsd3, formal-methods, game, library, theorem-provers)TomHawkins
theoremquest-client30.0A simple client for the TheoremQuest theorem proving game. (bsd3, formal-methods, game, program, theorem-provers)TomHawkins
tip-haskell-frontend30.0Convert from Haskell to Tip (bsd3, library, program, theorem-provers)DanRosen
tip-lib90.0tons of inductive problems - support library and tools (bsd3, library, program, theorem-provers)DanRosen
toysolver160.0Assorted decision procedures for SAT, Max-SAT, PB, MIP, etc (algorithms, benchmark, bsd3, constraints, library, logic, optimisation, optimization, program, theorem-provers)MasahiroSakai
twee210.0An equational theorem prover (bsd3, library, program, theorem-provers)NickSmallbone
yices-easy30.0Simple interface to the Yices SMT (SAT modulo theories) solver. (algorithms, bsd3, library, math, theorem-provers)KeeganMcAllister
yices-painless70.0An embedded language for programming the Yices SMT solver (bsd3, formal-methods, library, math, theorem-provers)DonaldStewart
z3352.0Bindings for the Z3 Theorem Prover (bit-vectors, bsd3, formal-methods, library, math, smt, theorem-provers)IagoAbal
zeno50.0An automated proof system for Haskell programs (mit, program, theorem-provers)WilliamSonnex