-
-
-
-
-
Megalodon Public
The Megalodon interactive theorem prover and proof checker
-
Prover9 Public
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
-
-
-
-
mm-atp-benchmark Public
Metamath ATP Benchmark created from set.mm
-
oeis-atp-benchmark Public
The OEIS Benchmark for Inductive Theorem Proving
-
cvc5ml Public
Forked from ajreynol/CVC4CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems.
-
-
public Public
Public space for AI4REASON permanent links (like conference paper materials).
1 UpdatedOct 20, 2022 -
isa_enigma_paper Public
Data and information for the "Isabelle ENIGMA" ITP'22 paper
-
-
-
-
enigma-gpu-server Public
Tensorflow GPU server for fast evaluation with ENIGMA E Prover
-
aimleap Public
AIMLEAP is an environment designed for proving equational theorems by interacting with a (typically learning-based) advisors.
-
Proofgold Public
Proofgold is a cryptocurrency that allows bounties on formal proofs.
OCaml MIT License UpdatedNov 9, 2020 -
GRUNGE-full Public
Forked from JUrban/GRUNGE-fullThe full GRUNGE repo
Common Lisp UpdatedAug 18, 2020 -
-
-
enigma Public
ENIGMA: Inference Guiding Machine
-
-
BliStrTune Public
Hierarchical invention of targeted E prover strategies
-
EmpireTune Public
Invention of Targeted Theorem Proving Strategies for E and Vampire
Ruby GNU General Public License v3.0 UpdatedJul 19, 2017