hackage.haskell.org "theorem-provers" keyword
View the packages on the hackage.haskell.org package registry that are tagged with the "theorem-provers" keyword.
smtlib2-quickcheck 1.0
1 version - Latest release: over 8 years ago - 1 thousand downloads total - 1 maintainergrisette-monad-coroutine 0.2.0.0
Orphan instances and wrappers for monad-coroutine package with Grisette.2 versions - Latest release: over 1 year ago - 1 dependent repositories - 157 downloads total - 0 stars on GitHub - 1 maintainer
toysolver 0.9.0
Toy-level solver implementation of various problems including SAT, SMT, Max-SAT, PBSPBO (Pseudo B...16 versions - Latest release: 5 months ago - 2 dependent repositories - 15.7 thousand downloads total - 157 stars on GitHub - 1 maintainer
logic-TPTP 0.2.0
21 versions - Latest release: about 16 years ago - 3 dependent repositories - 15.1 thousand downloads total - 3 maintainerslogic-classes 1.7.1
Framework for propositional and first order logic, theorem proving20 versions - Latest release: almost 9 years ago - 1 dependent package - 13.6 thousand downloads total - 7 stars on GitHub - 1 maintainer
Top 4.0% on hackage.haskell.org
128 versions - Latest release: over 13 years ago - 8 dependent packages - 162 dependent repositories - 82 thousand downloads total - 240 stars on GitHub - 1 maintainer
sbv 0.9.24
Express properties about Haskell programs and automatically prove them using SMT (Satisfiability ...128 versions - Latest release: over 13 years ago - 8 dependent packages - 162 dependent repositories - 82 thousand downloads total - 240 stars on GitHub - 1 maintainer
hz3 96.0.0.0 💰
Fork of z3 with future-proof version-numbering scheme Bindings for the Z3 4.x Theorem Prover (ht...1 version - Latest release: almost 6 years ago - 682 downloads total - 0 stars on GitHub
mprover 0.0.0.0
MProver is a proof checker for equational reasoning in a Haskell-like language. This is an extrem...1 version - Latest release: over 13 years ago - 1.02 thousand downloads total - 1 maintainer
tptp 0.1.3.0
Parser and pretty printer for the TPTP language7 versions - Latest release: over 4 years ago - 1 dependent repositories - 2.52 thousand downloads total - 7 stars on GitHub - 1 maintainer
tamarin-prover 0.8.6.3
17 versions - Latest release: almost 10 years ago - 11.7 thousand downloads total - 2 maintainerswhat4 1.6.3
What4 is a generic library for representing values as symbolic formulae which may contain referen...13 versions - Latest release: 5 months ago - 9 dependent packages - 18 dependent repositories - 4.84 thousand downloads total - 165 stars on GitHub - 5 maintainers
theoremquest-client 0.0.0
1 version - Latest release: over 14 years ago - 1.16 thousand downloads total - 1 maintaineryices-painless 0.1.2
3 versions - Latest release: over 14 years ago - 2.55 thousand downloads total - 1 maintainerhtaut 0.1.1.0
Haskell integrated Tautology prover2 versions - Latest release: almost 9 years ago - 1.48 thousand downloads total - 2 stars on GitHub - 1 maintainer
grisette 0.13.0.1
Grisette is a reusable symbolic evaluation library for Haskell. By translating programs into cons...18 versions - Latest release: 11 days ago - 1 dependent package - 2 dependent repositories - 844 downloads total - 67 stars on GitHub - 1 maintainer
tamarin-prover-utils 0.8.5.1
11 versions - Latest release: over 11 years ago - 9 dependent repositories - 7.83 thousand downloads total - 2 maintainerspesca 4.0.1
Pesca is a program that helps in the construction of proofs in sequent calculus. It works both as...2 versions - Latest release: about 17 years ago - 2.24 thousand downloads total - 3 maintainers
hylolib 1.5.4
10 versions - Latest release: over 6 years ago - 1 dependent repositories - 7.01 thousand downloads total - 1 maintainerbindings-yices 0.3.0.2
5 versions - Latest release: almost 10 years ago - 1 dependent repositories - 4.06 thousand downloads total - 1 maintainerqed 0.0
A prototype proof system.1 version - Latest release: over 9 years ago - 900 downloads total - 3 stars on GitHub - 1 maintainer
theoremquest 0.0.0
1 version - Latest release: over 14 years ago - 1 dependent repositories - 1.2 thousand downloads total - 1 maintainersmtlib2 0.3.1
5 versions - Latest release: about 9 years ago - 1 dependent package - 4 dependent repositories - 4.46 thousand downloads total - 1 maintainerLPPaver 0.0.5.0
Please see the README on GitHub at https://github.com/rasheedja/LPPaver#readme2 versions - Latest release: over 2 years ago - 1 dependent package - 1 dependent repositories - 166 downloads total - 5 stars on GitHub - 1 maintainer
HTab 1.7.3
9 versions - Latest release: about 5 years ago - 7.15 thousand downloads total - 1 maintainersmtlib2-timing 1.0
1 version - Latest release: over 8 years ago - 1.02 thousand downloads total - 1 maintainertip-lib 0.2.2
6 versions - Latest release: over 9 years ago - 3 dependent repositories - 3.97 thousand downloads total - 1 maintainerhylotab 1.2.1
2 versions - Latest release: about 13 years ago - 1.77 thousand downloads total - 1 maintainerhaskhol-core 1.1.0
2 versions - Latest release: over 10 years ago - 2 dependent repositories - 1.81 thousand downloads total - 1 maintainersmtlib2-pipe 1.0
1 version - Latest release: over 8 years ago - 1 dependent repositories - 1.08 thousand downloads total - 1 maintainertwee 2.4.2
Twee is an experimental equational theorem prover based on Knuth-Bendix completion. Given a set ...15 versions - Latest release: almost 3 years ago - 5.62 thousand downloads total - 52 stars on GitHub - 1 maintainer
twee-lib 2.4.2
An equational theorem prover based on Knuth-Bendix completion13 versions - Latest release: almost 3 years ago - 1 dependent package - 2 dependent repositories - 5.56 thousand downloads total - 49 stars on GitHub - 1 maintainer
tamarin-prover-term 0.8.5.1
10 versions - Latest release: over 11 years ago - 9 dependent repositories - 7.24 thousand downloads total - 2 maintainerstamarin-prover-theory 0.8.6.0
5 versions - Latest release: over 11 years ago - 8 dependent repositories - 3.76 thousand downloads total - 2 maintainersatp-haskell 1.14.3
Haskell version of the code from "Handbook of Practical Logic and Automated Reasoning"9 versions - Latest release: over 1 year ago - 3 dependent repositories - 4.38 thousand downloads total - 16 stars on GitHub - 1 maintainer
hyloutils 1.0
1 version - Latest release: about 13 years ago - 1.04 thousand downloads total - 1 maintainertip-haskell-frontend 0.1.1
3 versions - Latest release: about 10 years ago - 1 dependent repositories - 1.99 thousand downloads total - 1 maintainerPropaFP 0.1.2.0
Please see the README on GitHub at https://github.com/rasheedja/PropaFP#readme3 versions - Latest release: over 2 years ago - 2 dependent packages - 2 dependent repositories - 238 downloads total - 8 stars on GitHub - 1 maintainer
zsyntax 0.2.0.0
An automated theorem prover for Zsyntax, a logical calculus for molecular biology inspired by lin...1 version - Latest release: over 6 years ago - 1 dependent repositories - 553 downloads total - 12 stars on GitHub - 1 maintainer
sbvPlugin 9.12.1
GHC plugin for proving properties over Haskell functions using SMT solvers, based on the SBV pack...20 versions - Latest release: 5 months ago - 1 dependent repositories - 6.68 thousand downloads total - 45 stars on GitHub - 1 maintainer
scyther-proof 0.4.0
scyther-proof is a security protocol verification tool based on an algorithm similar to the Scyth...9 versions - Latest release: about 13 years ago - 6.69 thousand downloads total - 2 maintainers
dedukti 1.1.4
9 versions - Latest release: over 14 years ago - 7.37 thousand downloads total - 1 maintainerstructural-induction 0.1.2
SII: Structural Induction Instantiator over any strictly-positive algebraic data type.6 versions - Latest release: over 10 years ago - 3 dependent repositories - 4.6 thousand downloads total - 4 stars on GitHub - 1 maintainer
zeno 0.2.0.1
2 versions - Latest release: about 14 years ago - 1.89 thousand downloads total - 1 maintainertableaux 0.3
This is a simple web-based interactive theorem prover using semantic tableaux for propositional a...3 versions - Latest release: about 2 years ago - 2.1 thousand downloads total - 1 maintainer
atp 0.1.0.0
Haskell interface to automated theorem provers1 version - Latest release: over 4 years ago - 1 dependent repositories - 223 downloads total - 9 stars on GitHub - 1 maintainer
boolector 0.0.0.13
Haskell bindings for the Boolector SMT solver13 versions - Latest release: almost 5 years ago - 2 dependent repositories - 6.16 thousand downloads total - 5 stars on GitHub - 1 maintainer
ivor 0.1.14
9 versions - Latest release: over 14 years ago - 1 dependent repositories - 8.61 thousand downloads total - 2 maintainersz3 4.3.1
Bindings for the Z3 4.x Theorem Prover (https://github.com/Z3Prover/z3). Z3.Base.C provides the ...15 versions - Latest release: about 7 years ago - 16 dependent repositories - 11.2 thousand downloads total - 58 stars on GitHub - 1 maintainer
smtlib2-debug 1.0
1 version - Latest release: over 8 years ago - 1 dependent repositories - 1.02 thousand downloads total - 1 maintainerhgen 1.4.0
2 versions - Latest release: about 13 years ago - 1.69 thousand downloads total - 1 maintaineryices-easy 0.1
1 version - Latest release: almost 15 years ago - 1.23 thousand downloads total - 1 maintainerFolly 0.2.0.1
First order logic in Haskell15 versions - Latest release: almost 10 years ago - 11.2 thousand downloads total - 10 stars on GitHub - 1 maintainer
Related Keywords
Propose Tags
52
library
40
bsd3
27
formal-methods
21
program
20
smt
14
math
11
symbolic-computation
10
haskell
8
gpl
7
logic
7
deprecated
6
theorem-proving
4
verification
4
bit-vectors
4
theorem-prover
3
mathematics
2
maths
2
mpl
2
compilers-interpreters
2
mit
2
game
2
automated-theorem-provers
2
tptp
2
algorithms
2
automatic-theorem-proving
1
floating-point
1
floating-point-arithmetic
1
formal-verification
1
bioinformatics
1
automated-deduction
1
linear-logic
1
molecular-biology
1
sbv
1
security
1
lgpl
1
atp
1
first-order-logic
1
prover
1
dependent-types
1
api
1
z3
1
smt-solver
1
codec
1
sat-solver
1
mathematical-programming
1
optimization
1
optimisation
1
constraints
1
language
1
parsing
1
pretty-printer
1
eprover
1
haskell-library
1
parsing-library
1
pretty-print
1
vampire
1
symbolic-evaluation
1
symbolic-execution
1
synthesis
1
ffi
1
foreign
1
public-domain
1