Ecosyste.ms: Repos
An open API service providing repository metadata for many open source software ecosystems.
GitHub topics: theorem-prover
msakai/toysolver
My sandbox for experimenting with solver algorithms.
Language: Haskell - Size: 7.22 MB - Last synced: 3 days ago - Pushed: 4 days ago - Stars: 152 - Forks: 11
uuverifiers/ostrich
An SMT Solver for string constraints
Language: Scala - Size: 207 MB - Last synced: 4 days ago - Pushed: 5 days ago - Stars: 30 - Forks: 9
ptarau/TypesAndProofs
Type inference algorithms and intuitionistic propositional theorem provers solving type inhabitation problems
Language: Prolog - Size: 3.91 MB - Last synced: 4 days ago - Pushed: 4 days ago - Stars: 29 - Forks: 3
lean-ja/fp-lean-ja
Functional Programming in Lean の日本語訳. 演習問題への解答を含みます（作業中 🚧）
Language: Lean - Size: 1.15 MB - Last synced: 7 days ago - Pushed: 7 days ago - Stars: 4 - Forks: 1
newca12/awesome-rust-formalized-reasoning
An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.
Size: 279 KB - Last synced: 7 days ago - Pushed: 7 days ago - Stars: 278 - Forks: 9
HigherOrderCO/Kind1
A next-gen functional language
Language: Rust - Size: 34.4 MB - Last synced: 7 days ago - Pushed: 9 days ago - Stars: 3,493 - Forks: 136
cicada-lang/cicada-plct
Cicada Language (PLCT little team)
Language: TypeScript - Size: 2.5 MB - Last synced: 8 days ago - Pushed: 9 days ago - Stars: 91 - Forks: 6
SRI-CSL/yices2
The Yices SMT Solver
Language: SMT - Size: 25.7 MB - Last synced: 9 days ago - Pushed: 10 days ago - Stars: 354 - Forks: 45
pitmonticone/carleson Fork of fpvandoorn/carleson
[WIP] A formalised proof of a generalised Carleson's Theorem in the Lean proof assistant.
Language: TeX - Size: 718 KB - Last synced: 13 days ago - Pushed: 13 days ago - Stars: 0 - Forks: 0
cicada-lang/cicada-solo
Cicada Language (solo version)
Language: TypeScript - Size: 6.83 MB - Last synced: 15 days ago - Pushed: 15 days ago - Stars: 126 - Forks: 5
cheuktingli/psitip
Python Symbolic Information Theoretic Inequality Prover
Language: Python - Size: 2.56 MB - Last synced: 16 days ago - Pushed: 4 months ago - Stars: 32 - Forks: 7
philzook58/pyeprover
A simple repackaging of the E automated theorem prover for ease of installation and execution from python
Language: Shell - Size: 1.65 MB - Last synced: 24 days ago - Pushed: 2 months ago - Stars: 1 - Forks: 0
konn/vscode-redtt-diagnostics 📦
Diagnostic extension for redtt prover
Language: TypeScript - Size: 120 KB - Last synced: 25 days ago - Pushed: about 2 years ago - Stars: 3 - Forks: 1
pitmonticone/FLT3 Fork of riccardobrasca/flt3
A formalised proof of Fermat's Last Theorem for exponent 3 in the Lean proof assistant.
Language: TeX - Size: 550 KB - Last synced: 25 days ago - Pushed: 25 days ago - Stars: 1 - Forks: 1
plazajan/Propositional-Resolution
Propositional theorem prover - resolution with pure literal elimination and subsumption elimination, implemented in ISO Prolog. Educational software.
Language: Prolog - Size: 110 KB - Last synced: 28 days ago - Pushed: 28 days ago - Stars: 0 - Forks: 0
phenax/ts-theorem-provinator
Experiment to use typescript's type system for theorem proving
Language: TypeScript - Size: 30.3 KB - Last synced: 24 days ago - Pushed: 5 months ago - Stars: 4 - Forks: 0
lukaszcz/coqhammer
CoqHammer: An Automated Reasoning Hammer Tool for Coq - Proof Automation for Dependent Type Theory
Language: OCaml - Size: 2.5 MB - Last synced: 23 days ago - Pushed: about 1 month ago - Stars: 205 - Forks: 29
0vercl0k/z3-playground 📦
A repository to store Z3-python scripts you can use as examples, reminders, whatever.
Language: Python - Size: 56.6 KB - Last synced: 6 days ago - Pushed: almost 4 years ago - Stars: 273 - Forks: 33
uuverifiers/princess
The Princess Theorem Prover
Language: Scala - Size: 52.1 MB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 18 - Forks: 5
evhub/pyprover
Resolution theorem proving for predicate logic in pure Python.
Language: Python - Size: 344 KB - Last synced: 24 days ago - Pushed: 6 months ago - Stars: 88 - Forks: 8
veracruz-project/supervisionary
The Supervisionary proof-checking kernel for higher-order logic
Language: Rust - Size: 827 KB - Last synced: about 1 month ago - Pushed: about 2 years ago - Stars: 3 - Forks: 0
righ1113/IshiiSan_Galois_Idris
『ガロア理論の頂を踏む』読書ノート
Language: Idris - Size: 40 KB - Last synced: about 1 month ago - Pushed: over 4 years ago - Stars: 1 - Forks: 0
jubnzv/folderol
A toy theorem prover
Language: OCaml - Size: 21.5 KB - Last synced: about 1 month ago - Pushed: about 1 year ago - Stars: 4 - Forks: 0
edoput/lcf-prover
silly automated prover for minimal propositional logic
Language: OCaml - Size: 2.93 KB - Last synced: about 1 month ago - Pushed: almost 5 years ago - Stars: 3 - Forks: 0
acl2/acl2
ACL2 System and Books as Maintained by the Community
Language: Common Lisp - Size: 1.2 GB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 336 - Forks: 96
lambduli/resin
A toy Automated Theorem Prover for First Order Classical Logic built on Resolution.
Language: Haskell - Size: 264 KB - Last synced: about 1 month ago - Pushed: about 1 month ago - Stars: 1 - Forks: 0
johnyf/tool_lists
Links to tools by subject
Size: 63.5 KB - Last synced: 10 days ago - Pushed: 2 months ago - Stars: 360 - Forks: 81
groupoid/anders
🧊 Модальний гомотопічний верифікатор математики
Language: OCaml - Size: 11.5 MB - Last synced: about 1 month ago - Pushed: about 2 months ago - Stars: 17 - Forks: 3
RiccardoBiosas/LeanGPT
Experiments with interactive theorem provers, LLMs and formal systems
Language: Coq - Size: 7.81 KB - Last synced: about 1 month ago - Pushed: 11 months ago - Stars: 12 - Forks: 2
philzook58/pyvampire
A simple repackaging of the Vampire automated theorem prover
Language: Shell - Size: 20.8 MB - Last synced: 24 days ago - Pushed: 2 months ago - Stars: 1 - Forks: 0
dominique-unruh/qrhl-tool
Proof assistant for qRHL
Language: Scala - Size: 90.1 MB - Last synced: 15 days ago - Pushed: 15 days ago - Stars: 17 - Forks: 3
hengxin/tlaps-examples
Examples for TLAPS (TLA+ Proof System)
Language: TeX - Size: 4.76 MB - Last synced: about 1 month ago - Pushed: about 4 years ago - Stars: 9 - Forks: 6
theoremprover-museum/egal
Chad Brown’s Egal, a theorem prover for higher-order Tarski–Grothendieck set theory
Language: OCaml - Size: 1.32 MB - Last synced: about 2 months ago - Pushed: almost 3 years ago - Stars: 2 - Forks: 0
philzook58/egglog0
Datalog + Egg = Good
Language: Rust - Size: 481 KB - Last synced: 24 days ago - Pushed: 12 months ago - Stars: 65 - Forks: 3
jchenche/theorem-prover
Implementation of a theorem prover for first-order logic
Language: Rust - Size: 278 KB - Last synced: about 1 month ago - Pushed: 6 months ago - Stars: 1 - Forks: 0
andrew-johnson-4/LSTS
Large Scale Type Systems (programming language)
Language: Rust - Size: 1.16 MB - Last synced: 4 days ago - Pushed: 3 months ago - Stars: 99 - Forks: 3
joom/hezarfen 📦
a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features
Language: Idris - Size: 48.8 KB - Last synced: 3 months ago - Pushed: over 5 years ago - Stars: 118 - Forks: 3
nomaanakhan/Theorem-Prover-for-Clause-Logic
Theorem prover for a clause logic using the resolution principle.
Language: Python - Size: 223 KB - Last synced: 17 days ago - Pushed: about 5 years ago - Stars: 4 - Forks: 0
tani/acl2-kernel
Jupyter Kernel for ACL2
Language: Jupyter Notebook - Size: 145 KB - Last synced: 9 days ago - Pushed: about 1 month ago - Stars: 4 - Forks: 1
righ1113/divseq2
割数列を用いたコラッツ予想の証明Ⅱ
Language: Lean - Size: 34.2 KB - Last synced: about 1 month ago - Pushed: 9 months ago - Stars: 1 - Forks: 0
RAIRLab/lazyslate
An open source graphical proof construction assistant for the creation of Natural Deduction proofs. Started as a Hack RPI 2022 Project
Language: TypeScript - Size: 175 KB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 1 - Forks: 0
Chymyst/curryhoward
Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism
Language: Scala - Size: 413 KB - Last synced: 3 months ago - Pushed: over 2 years ago - Stars: 254 - Forks: 14
LS-Lab/KeYmaera-release
Older KeYmaera 3: A Hybrid Theorem Prover for Hybrid Systems
Language: Java - Size: 19.5 MB - Last synced: 2 months ago - Pushed: over 9 years ago - Stars: 8 - Forks: 4
LS-Lab/KeYmaeraX-release
KeYmaera X: An aXiomatic Tactical Theorem Prover for Hybrid Systems (release)
Language: Scala - Size: 256 MB - Last synced: 2 months ago - Pushed: 2 months ago - Stars: 71 - Forks: 36
ai4reason/Prover9
Prover9 is an automated theorem prover for first-order and equational logic, and Mace4 searches for finite models and counterexamples.
Language: C - Size: 1.81 MB - Last synced: 4 months ago - Pushed: 4 months ago - Stars: 27 - Forks: 8
martinberger/hol-c
A proof-of-concept LCF-style interactive theorem prover for HOL(C)
Language: Scala - Size: 136 KB - Last synced: 3 months ago - Pushed: 3 months ago - Stars: 4 - Forks: 1
shilangyu/cs550-labs
Solutions to labs from the formal verification course at EPFL
Language: Scala - Size: 1.03 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 0 - Forks: 0
lambduli/plover
An implementation of Minilog (my other) toy language with a complete search strategy making it a simple, naive, toy theorem prover with Prolog syntax.
Language: Haskell - Size: 2.72 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 3 - Forks: 0
RAIRLab/ShadowProver
The definitive DCEC theorem prover built on SNARK.
Language: Java - Size: 35.5 MB - Last synced: 6 months ago - Pushed: 6 months ago - Stars: 1 - Forks: 0
kovvalsky/prove_SICK_NL
Prove Ducth NLI problems of SICK-NL with LangPro
Language: Prolog - Size: 66.4 MB - Last synced: 7 months ago - Pushed: 7 months ago - Stars: 3 - Forks: 0
catseye/Philomath
MIRROR of https://codeberg.org/catseye/Philomath : An LCF-style theorem prover written in C89 (a.k.a ANSI C)
Language: C - Size: 51.8 KB - Last synced: 5 months ago - Pushed: 5 months ago - Stars: 12 - Forks: 1
forked-from-1kasper/anders
Anders: Cubical Type Checker
Language: OCaml - Size: 4.02 MB - Last synced: 7 months ago - Pushed: 7 months ago - Stars: 13 - Forks: 1
DaniRuizPerez/AutomaticReasoning-IntelligentSystems
Collection of projets that I developed like an ASP music composer, a Sokoban, Hitory and 8puzzle puzzle solvers, Probabilistic Reasoning with Answer Sets and a project on Automatic Theorem Provers
Language: C - Size: 155 KB - Last synced: 7 months ago - Pushed: over 6 years ago - Stars: 0 - Forks: 1
pro465/nnoq
not noq
Language: Rust - Size: 94.7 KB - Last synced: 4 days ago - Pushed: 7 months ago - Stars: 4 - Forks: 1
benhuds/wangs-algorithm
Propositional theorem prover using Wang's algorithm
Language: Prolog - Size: 7.81 KB - Last synced: about 1 month ago - Pushed: over 7 years ago - Stars: 7 - Forks: 2
Seasawher/mathematics_in_lean Fork of leanprover-community/mathematics_in_lean
「Mathematics in Lean」の読書メモ
Language: Lean - Size: 17.2 MB - Last synced: 9 months ago - Pushed: 9 months ago - Stars: 0 - Forks: 0
Seasawher/lean-math-workshop-my-solutions
https://github.com/yuma-mizuno/lean-math-workshop のクローン．自分で問題を解いていくために使う．
Language: Lean - Size: 295 KB - Last synced: 9 months ago - Pushed: 9 months ago - Stars: 0 - Forks: 0
Seasawher/lean-quiz-template
Lean でクイズを出題するためのテンプレート. lean_grader を使用して自動採点を行います．
Language: Lean - Size: 5.86 KB - Last synced: 9 months ago - Pushed: 9 months ago - Stars: 0 - Forks: 0
joom/WangsAlgorithm
A classical propositional theorem prover in Haskell, using Wang's Algorithm.
Language: Haskell - Size: 17.6 KB - Last synced: 10 months ago - Pushed: almost 5 years ago - Stars: 35 - Forks: 4
chrisjpm/holbert Fork of liamoc/holbert
A graphical interactive proof assistant designed for education. My contributions: applying rules by elimination, proofs by induction, proofs by cases, multi-axiom element and misc css styling. Honours report grade: 76% :tada:
Language: Haskell - Size: 13.3 MB - Last synced: 10 months ago - Pushed: almost 2 years ago - Stars: 0 - Forks: 0
Seasawher/math2001 Fork of hrmacbeth/math2001
Lean4 による数学の定理証明のチュートリアル
Language: Lean - Size: 4.64 MB - Last synced: 10 months ago - Pushed: 10 months ago - Stars: 0 - Forks: 0
domasin/nholz
An F# porting of HOL Zero
Language: F# - Size: 27.6 MB - Last synced: 9 months ago - Pushed: 9 months ago - Stars: 0 - Forks: 0
namin/leanTAP
A Declarative Theorem Prover for First-Order Classical Logic
Language: Scheme - Size: 20.5 KB - Last synced: 7 months ago - Pushed: almost 4 years ago - Stars: 25 - Forks: 2
nclarius/pyPL
Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions
Language: Python - Size: 5.83 MB - Last synced: 25 days ago - Pushed: over 1 year ago - Stars: 18 - Forks: 2
benjishults/bitnots
Tableau Theorem Prover
Language: Kotlin - Size: 1.04 MB - Last synced: 11 months ago - Pushed: 11 months ago - Stars: 3 - Forks: 1
kovvalsky/LangPro
Tableau-based Theorem Prover for Natural Logic and Language
Language: Prolog - Size: 26.3 MB - Last synced: 7 months ago - Pushed: 7 months ago - Stars: 107 - Forks: 9
Seasawher/docker-lean4
Ubuntu base docker images and devcontainer feature of lean4 theorem prover
Language: Dockerfile - Size: 34.2 KB - Last synced: 11 months ago - Pushed: 11 months ago - Stars: 0 - Forks: 0
forked-from-1kasper/bravo
Castle Bravo: Experimental HoTT Implementation
Language: OCaml - Size: 381 KB - Last synced: 12 months ago - Pushed: 12 months ago - Stars: 6 - Forks: 1
georgejkaye/theorem-prover
A simple theorem prover made for a university programming assignment
Language: Java - Size: 163 KB - Last synced: about 1 month ago - Pushed: almost 7 years ago - Stars: 4 - Forks: 1
moratori/clover
A experimental prover written in Common Lisp, based on clause resolution and Knuth-Bendix completion algorithm.
Language: Common Lisp - Size: 443 KB - Last synced: 11 months ago - Pushed: almost 2 years ago - Stars: 1 - Forks: 0
uncomputable/natural-number-game
Reimplementation of Natural Number Game in Coq
Language: Coq - Size: 14.6 KB - Last synced: about 1 month ago - Pushed: over 1 year ago - Stars: 6 - Forks: 0
James-Oswald/EminenceProver
A theorem prover for proof-theoretic higher order modal logic
Language: C++ - Size: 515 KB - Last synced: about 1 year ago - Pushed: about 1 year ago - Stars: 0 - Forks: 0
rasheedja/LPPaver
An automated prover targeting problems that involve nonlinear real arithmetic.
Language: JavaScript - Size: 1.62 MB - Last synced: 6 days ago - Pushed: 6 months ago - Stars: 5 - Forks: 0
adyavanapalli/natural-number-game-solutions
Solutions to Imperial College London's Natural Number Game, a gamified formal mathematics course on the Peano axioms using an interactive + automated theorem prover developed by Microsoft Research called Lean.
Size: 23.4 KB - Last synced: about 1 year ago - Pushed: over 2 years ago - Stars: 8 - Forks: 6
ncfavier/muri
A theorem prover for intuitionistic propositional logic
Language: Haskell - Size: 28.3 KB - Last synced: about 1 year ago - Pushed: over 3 years ago - Stars: 4 - Forks: 0
o7q/InfiniteMonkeySimulator
Simulate an immortal monkey typing on a typewriter.
Language: C++ - Size: 725 KB - Last synced: about 1 year ago - Pushed: about 1 year ago - Stars: 0 - Forks: 0
gilith/metis
An automatic theorem prover for first order logic with equality
Language: Standard ML - Size: 609 KB - Last synced: about 1 year ago - Pushed: almost 4 years ago - Stars: 27 - Forks: 1
nbice1/First-Order-Logic
This project is aimed at developing a program to evaluate the truth-value of sentences in First-Order Logic and construct proofs.
Language: Python - Size: 225 KB - Last synced: about 1 year ago - Pushed: over 2 years ago - Stars: 4 - Forks: 0
taktoa/eqsat
A language-generic implementation of equality saturation in Haskell
Language: Haskell - Size: 451 KB - Last synced: 7 months ago - Pushed: over 5 years ago - Stars: 19 - Forks: 3
chaudhuri/sympli 📦
A propositional linear inverse method theorem prover (written in 2003-2004, very lightly maintained)
Language: Standard ML - Size: 106 KB - Last synced: about 1 year ago - Pushed: almost 6 years ago - Stars: 2 - Forks: 0
dannypsnl/k 📦
k theorem prover
Language: Racket - Size: 280 KB - Last synced: 4 days ago - Pushed: almost 2 years ago - Stars: 11 - Forks: 1
rasheedja/PropaFP
Auto-active verification of floating-point programs.
Language: Haskell - Size: 1.54 MB - Last synced: 15 days ago - Pushed: 7 months ago - Stars: 6 - Forks: 0
samuelbarrett1234/atp
An automated conjecturer / theorem prover in C++
Language: C++ - Size: 181 MB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 0 - Forks: 0
5HT/bertrand
🧊 Metamath система
Language: OCaml - Size: 157 KB - Last synced: about 1 year ago - Pushed: about 2 years ago - Stars: 1 - Forks: 0
bor0/budge
Budge - a programming language and a theorem prover
Language: Jupyter Notebook - Size: 907 KB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 8 - Forks: 0
yakuza8/first-order-predicate-logic-theorem-prover
Autonomous Theorem Prover for First Order Predicate Logic
Language: Python - Size: 104 KB - Last synced: about 1 year ago - Pushed: almost 4 years ago - Stars: 8 - Forks: 3
DominicPM/supervisionary
Supervisionary: a proof-checking system for HOL
Language: Rust - Size: 4.84 MB - Last synced: 4 days ago - Pushed: about 1 year ago - Stars: 0 - Forks: 0
tani/solv
IPC/CPC theorem prover in Prolog
Language: Prolog - Size: 48.8 KB - Last synced: 10 days ago - Pushed: 3 months ago - Stars: 1 - Forks: 0
cpressey/LCF-style-ND
Exposition of an LCF-style theorem prover for propositional logic in a Natural Deduction system
Size: 123 KB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 2 - Forks: 0
sramakrishnan247/ProveMe
A Theorem Prover for Propositional Logic
Language: Java - Size: 50.8 KB - Last synced: about 1 year ago - Pushed: over 1 year ago - Stars: 2 - Forks: 1
forked-from-1kasper/principia
Principia: Metamath-like Logician Language
Language: OCaml - Size: 126 KB - Last synced: about 1 year ago - Pushed: about 2 years ago - Stars: 1 - Forks: 0
forked-from-1kasper/romeo
Castle Romeo: Experimental Theorem Prover for Category Theory
Language: OCaml - Size: 122 KB - Last synced: about 1 year ago - Pushed: almost 2 years ago - Stars: 2 - Forks: 0
jdevuyst/tableaux
Tableau-based theorem prover for public announcement logic
Language: Clojure - Size: 211 KB - Last synced: 10 months ago - Pushed: over 9 years ago - Stars: 6 - Forks: 1
BelegCuthalion/hilbert
Simple Hilbert-style prover for implicational fragment.
Language: Python - Size: 5.86 KB - Last synced: about 1 year ago - Pushed: almost 2 years ago - Stars: 0 - Forks: 0
SjVer/MQS
Math Question Solver
Language: Rust - Size: 1.37 MB - Last synced: about 1 year ago - Pushed: almost 2 years ago - Stars: 4 - Forks: 0
flijnzaad/natural-natural-deduction
"Natural" Natural Deduction: a Theorem Prover for Propositional Logic
Language: Python - Size: 571 KB - Last synced: about 1 year ago - Pushed: almost 3 years ago - Stars: 1 - Forks: 0
forked-from-1kasper/hurricane
Hurricane: HoTT-I Type System
Language: OCaml - Size: 44.9 KB - Last synced: about 1 year ago - Pushed: about 2 years ago - Stars: 0 - Forks: 0
arckt/go-stp
Golang bindings to the STP API
Language: Go - Size: 4.88 KB - Last synced: about 1 month ago - Pushed: over 2 years ago - Stars: 0 - Forks: 0
righ1113/collatzProof_DivSeq
割数列を用いたコラッツ予想の証明
Language: Idris - Size: 357 KB - Last synced: about 1 month ago - Pushed: 6 months ago - Stars: 0 - Forks: 0
righ1113/godel
Mathematical Girls
Language: Idris - Size: 85 KB - Last synced: about 1 month ago - Pushed: 5 months ago - Stars: 0 - Forks: 0