#
theorem-prover
Here are 64 public repositories matching this topic...
Links to tools by subject
tools
static-analysis
theorem-proving
verification
proof-assistant
smtlib
synthesis
satisfiability-solver
binary-decision-diagrams
model-checking
satisfiability-modulo-theories
formal-methods
theorem-prover
-
Updated
Aug 12, 2021
The Yices SMT Solver
-
Updated
Aug 12, 2021 - SMT
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
scala
functional-programming
lambda-calculus
scala-macros
code-generation
automated-theorem-provers
theorem-prover
intuitionistic-logic
curry-howard-isomorphism
lambda-terms
-
Updated
Jul 19, 2021 - Scala
A repository to store Z3-python scripts you can use as examples, reminders, whatever.
-
Updated
Aug 22, 2020 - Python
ACL2 System and Books as Maintained by the Community
common-lisp
logic
theorem-proving
first-order-logic
formal-methods
formal-verification
theorem-prover
rewriting
acl2
-
Updated
Aug 13, 2021 - Common Lisp
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
-
Updated
Aug 1, 2021 - OCaml
My sandbox for experimenting with solver algorithms.
-
Updated
May 29, 2021 - Haskell
a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features
-
Updated
Sep 12, 2018 - Idris
-
Updated
Aug 10, 2021 - OCaml
Resolution theorem proving for predicate logic in pure Python.
-
Updated
Jun 26, 2021 - Python
KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
scala
proof
mathematica
tactics
dynamical-systems
differential-equations
hybrid-systems
theorem-prover
axiom
cyber-physical-systems
dynamic-logics
differential-dynamic-logic
keymaera
hybrid-games
-
Updated
Jul 22, 2021 - Scala
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
-
Updated
Jun 12, 2019 - Haskell
A Declarative Theorem Prover for First-Order Classical Logic
-
Updated
Aug 10, 2020 - Scheme
An automatic theorem prover for first order logic with equality
-
Updated
Jul 14, 2020 - Standard ML
Type inference algorithms and intuitionistic propositional theorem provers solving type inhabitation problems
prolog
type-inference
theorem-prover
beta-reduction
intuitionistic-logic
curry-howard-isomorphism
lambda-terms
random-binary-tree
random-set-partition
tautology-checking
de-bruijn-notation
all-binary-trees-generator
all-set-partitions-gnerator
remy-s-algorithm
knuth-s-algorithm-r
boltzmann-sampler
normal-forms
-
Updated
Aug 9, 2021 - Prolog
A language-generic implementation of equality saturation in Haskell
-
Updated
Dec 4, 2018 - Haskell
An SMT Solver for string constraints
-
Updated
Jul 15, 2021 - Scala
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
-
Updated
Aug 8, 2018 - C
Spacemacs layer for the Lean Theorem Prover.
-
Updated
Sep 6, 2019 - Emacs Lisp
Grail is a theorem prover for multimodal type-logical grammars
-
Updated
Feb 11, 2021 - Prolog
Older KeYmaera 3: A Hybrid Theorem Prover for Hybrid Systems
java
proof
mathematica
dynamical-systems
differential-equations
hybrid-systems
theorem-prover
cyber-physical-systems
dynamic-logics
differential-dynamic-logic
-
Updated
Dec 15, 2014 - Java
Propositional theorem prover using Wang's algorithm
-
Updated
Oct 17, 2016 - Prolog
Automated mathematical theorem formulation deduced from a provided set of axioms. Builds upon the HRL theorem generator.
theorem-proving
mathematical-logic
theorem-prover
hrl
theorem-generator
theorem-generation
lakatos
lakatos-methods
-
Updated
Aug 16, 2020 - Java
A simple theorem prover made for a university programming assignment
theorem-proving
propositional-logic
dimacs
theorem
reasoning
theorem-prover
dpll
clause-normal-form
resolution-calculus
propositional-resolution
-
Updated
Jul 28, 2017 - Java
Autonomous Theorem Prover for First Order Predicate Logic
ai
theorem-proving
first-order-logic
artificial-intelligence
tautology
theorem-prover
first-order-unification
subsumption
first-order-substitution
tautology-checking
most-general-unifier
subsumption-elimination
-
Updated
Jun 29, 2020 - Python
A simple theorem prover for Coq.
-
Updated
Jan 17, 2021 - Python
Improve this page
Add a description, image, and links to the theorem-prover topic page so that developers can more easily learn about it.
Add this topic to your repo
To associate your repository with the theorem-prover topic, visit your repo's landing page and select "manage topics."
Describe the bug
When installing the Kind toolchain the
kind-scmcommand is installed. When I read [THEOREMS.md][theorems] the command is namedkind.To Reproduce
Steps to reproduce the behavior:
THEOREMS.md][theorems]Expected behavior
I would expect