hackage.haskell.org "theorem-provers" keyword
View the packages on the hackage.haskell.org package registry that are tagged with the "theorem-provers" keyword.
dedukti 1.1.4
9 versions - Latest release: over 14 years ago - 7.39 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 - 254 downloads total - 8 stars on GitHub - 1 maintainer
LPPaver 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 - 172 downloads total - 5 stars on GitHub - 1 maintainer
Folly 0.2.0.1
First order logic in Haskell15 versions - Latest release: almost 10 years ago - 11.3 thousand downloads total - 10 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: 6 months ago - 1 dependent repositories - 6.73 thousand downloads total - 45 stars on GitHub - 1 maintainer
hgen 1.4.0
2 versions - Latest release: about 13 years ago - 1.69 thousand downloads total - 1 maintainersmtlib2-debug 1.0
1 version - Latest release: over 8 years ago - 1 dependent repositories - 1.03 thousand downloads total - 1 maintainer
Top 4.0% on hackage.haskell.org
129 versions - Latest release: over 13 years ago - 8 dependent packages - 162 dependent repositories - 82.5 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 ...129 versions - Latest release: over 13 years ago - 8 dependent packages - 162 dependent repositories - 82.5 thousand downloads total - 240 stars on GitHub - 1 maintainer
grisette-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 - 159 downloads total - 0 stars on GitHub - 1 maintainer
smtlib2-quickcheck 1.0
1 version - Latest release: over 8 years ago - 1.01 thousand downloads total - 1 maintaineryices-easy 0.1
1 version - Latest release: almost 15 years ago - 1.24 thousand downloads total - 1 maintainerhz3 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 - 684 downloads total - 0 stars on GitHub
what4 1.6.3
What4 is a generic library for representing values as symbolic formulae which may contain referen...13 versions - Latest release: 6 months ago - 9 dependent packages - 18 dependent repositories - 4.88 thousand downloads total - 168 stars on GitHub - 5 maintainers
toysolver 0.9.0
Toy-level solver implementation of various problems including SAT, SMT, Max-SAT, PBSPBO (Pseudo B...16 versions - Latest release: 7 months ago - 2 dependent repositories - 15.7 thousand downloads total - 158 stars on GitHub - 1 maintainer
z3 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: over 7 years ago - 16 dependent repositories - 11.3 thousand downloads total - 60 stars on GitHub - 1 maintainer
ivor 0.1.14
9 versions - Latest release: over 14 years ago - 1 dependent repositories - 8.64 thousand downloads total - 2 maintainersHTab 1.7.3
9 versions - Latest release: over 5 years ago - 7.16 thousand downloads total - 1 maintaineryices-painless 0.1.2
3 versions - Latest release: over 14 years ago - 2.55 thousand downloads total - 1 maintainertamarin-prover 0.8.6.3
17 versions - Latest release: about 10 years ago - 11.7 thousand downloads total - 2 maintainerslogic-TPTP 0.2.0
21 versions - Latest release: over 16 years ago - 3 dependent repositories - 15.2 thousand downloads total - 3 maintainerstptp 0.1.3.0
Parser and pretty printer for the TPTP language7 versions - Latest release: over 4 years ago - 1 dependent repositories - 2.54 thousand downloads total - 7 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 maintainermprover 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.03 thousand downloads total - 1 maintainer
theoremquest-client 0.0.0
1 version - Latest release: over 14 years ago - 1.16 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 maintainertamarin-prover-utils 0.8.5.1
11 versions - Latest release: over 11 years ago - 9 dependent repositories - 7.85 thousand downloads total - 2 maintainershyloutils 1.0
1 version - Latest release: about 13 years ago - 1.04 thousand downloads total - 1 maintainertamarin-prover-theory 0.8.6.0
5 versions - Latest release: over 11 years ago - 8 dependent repositories - 3.77 thousand downloads total - 2 maintainershtaut 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
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 - 557 downloads total - 12 stars on GitHub - 1 maintainer
haskhol-core 1.1.0
2 versions - Latest release: over 10 years ago - 2 dependent repositories - 1.82 thousand downloads total - 1 maintainergrisette 0.13.0.1
Grisette is a reusable symbolic evaluation library for Haskell. By translating programs into cons...18 versions - Latest release: about 2 months ago - 1 dependent package - 2 dependent repositories - 877 downloads total - 67 stars on GitHub - 1 maintainer
smtlib2 0.3.1
5 versions - Latest release: about 9 years ago - 1 dependent package - 4 dependent repositories - 4.47 thousand downloads total - 1 maintainertip-haskell-frontend 0.1.1
3 versions - Latest release: about 10 years ago - 1 dependent repositories - 2 thousand downloads total - 1 maintainerpesca 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: over 17 years ago - 2.25 thousand downloads total - 3 maintainers
smtlib2-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.98 thousand downloads total - 1 maintainerhylotab 1.2.1
2 versions - Latest release: about 13 years ago - 1.77 thousand downloads total - 1 maintainerqed 0.0
A prototype proof system.1 version - Latest release: almost 10 years ago - 903 downloads total - 3 stars on GitHub - 1 maintainer
hylolib 1.5.4
10 versions - Latest release: over 6 years ago - 1 dependent repositories - 7.03 thousand downloads total - 1 maintainertamarin-prover-term 0.8.5.1
10 versions - Latest release: over 11 years ago - 9 dependent repositories - 7.26 thousand downloads total - 2 maintainersbindings-yices 0.3.0.2
5 versions - Latest release: about 10 years ago - 1 dependent repositories - 4.06 thousand downloads total - 1 maintaineratp 0.1.0.0
Haskell interface to automated theorem provers1 version - Latest release: over 4 years ago - 1 dependent repositories - 226 downloads total - 9 stars on GitHub - 1 maintainer
tableaux 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.11 thousand downloads total - 1 maintainer
boolector 0.0.0.13
Haskell bindings for the Boolector SMT solver13 versions - Latest release: about 5 years ago - 2 dependent repositories - 6.18 thousand downloads total - 5 stars on GitHub - 1 maintainer
atp-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.4 thousand downloads total - 16 stars on GitHub - 1 maintainer
twee 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.64 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.58 thousand downloads total - 49 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: over 13 years ago - 6.7 thousand downloads total - 2 maintainers
structural-induction 0.1.2
SII: Structural Induction Instantiator over any strictly-positive algebraic data type.6 versions - Latest release: almost 11 years ago - 3 dependent repositories - 4.61 thousand downloads total - 4 stars on GitHub - 1 maintainer
zeno 0.2.0.1
2 versions - Latest release: over 14 years ago - 1.89 thousand downloads total - 1 maintainerlogic-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
Related Keywords
Propose Tags
52
library
40
bsd3
27
formal-methods
21
program
20
smt
14
math
11
symbolic-computation
10
haskell
8
logic
7
gpl
7
deprecated
6
theorem-proving
4
bit-vectors
4
verification
4
theorem-prover
3
algorithms
2
game
2
automated-theorem-provers
2
tptp
2
mit
2
compilers-interpreters
2
mathematics
2
mpl
2
maths
2
floating-point
1
pretty-print
1
vampire
1
bioinformatics
1
automated-deduction
1
linear-logic
1
molecular-biology
1
symbolic-evaluation
1
symbolic-execution
1
synthesis
1
ffi
1
foreign
1
public-domain
1
atp
1
lgpl
1
security
1
prover
1
first-order-logic
1
floating-point-arithmetic
1
formal-verification
1
automatic-theorem-proving
1
sbv
1
constraints
1
optimisation
1
optimization
1
mathematical-programming
1
sat-solver
1
smt-solver
1
api
1
z3
1
dependent-types
1
codec
1
language
1
parsing
1
pretty-printer
1
eprover
1
haskell-library
1
parsing-library
1