21 results found Sort:
- Filter by Primary Language:
- TypeScript (4)
- C (2)
- Haskell (2)
- Python (2)
- Scala (2)
- Prolog (1)
- SMT (1)
- Rust (1)
- Common Lisp (1)
- C++ (1)
- OCaml (1)
- +
A modern proof language
Created
2018-07-13
279 commits to master branch, last one 4 months ago
The Yices SMT Solver
Created
2014-11-10
5,273 commits to master branch, last one 4 days ago
ACL2 System and Books as Maintained by the Community
Created
2014-09-01
45,454 commits to master branch, last one 12 hours ago
Links to tools by subject
Created
2013-09-24
1 commits to main branch, last one about a year ago
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Created
2021-04-10
291 commits to main branch, last one 7 days ago
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
Created
2017-12-12
88 commits to master branch, last one 3 years ago
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Created
2018-01-31
597 commits to coq8.20 branch, last one 5 months ago
My sandbox for experimenting with solver algorithms.
Created
2011-06-12
3,226 commits to master branch, last one 6 days ago
Cicada Language (solo version)
Created
2021-03-28
6,372 commits to master branch, last one 4 months ago
Large Scale Type Systems (programming language)
Created
2021-09-10
1,446 commits to main branch, last one 3 months ago
Tableau-based Theorem Prover for Natural Logic and Language
Created
2017-03-05
138 commits to master branch, last one 2 years ago
VSCode extension that is designed to help automate writing of Coq proofs.
Created
2023-09-04
787 commits to main branch, last one 2 months ago
Resolution theorem proving for predicate logic in pure Python.
Created
2017-03-04
96 commits to master branch, last one about a year ago
Cicada Language (PLCT little team)
Created
2022-08-07
1,874 commits to master branch, last one 4 months ago
KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
Created
2015-08-26
16,739 commits to master branch, last one 7 months ago
Datalog + Egg = Good
Created
2021-07-21
56 commits to main branch, last one about a year ago
GCLC is a mathematical software tool for producing high-quality mathematical illustrations, for teaching mathematics, and for automated proving of geometry theorems.
Created
2020-12-05
415 commits to master branch, last one about a month ago
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
Created
2018-08-08
5 commits to master branch, last one about a year ago
lapisla is a *battery-pluggable* theorem prover and ecosystem designed for everyone. Greetings! 👋
Created
2025-01-20
535 commits to main branch, last one about a month ago
A Lean tactic for Canonical, a search procedure for terms in dependent type theory.
Created
2025-04-10
4 commits to master branch, last one 13 days ago
Tiny theorem prover with syntax like Lean 4 in <1K LOC
Created
2025-01-26
155 commits to main branch, last one 11 days ago