Topic: "proof-checker"
Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
Language: OCaml - Size: 39 MB - Last synced at: 8 days ago - Pushed at: 9 days ago - Stars: 320 - Forks: 36
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 at: 17 days ago - Pushed at: over 1 year ago - Stars: 14 - Forks: 2
c-cube/quip 📦
[wip] Proof format and checker for first-order and higher-order theorem provers
Language: OCaml - Size: 1.51 MB - Last synced at: 7 days ago - Pushed at: about 2 years ago - Stars: 12 - Forks: 1
c-cube/trustee
[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.
Language: OCaml - Size: 3.45 MB - Last synced at: 7 days ago - Pushed at: over 1 year ago - Stars: 11 - Forks: 2
catseye/Maxixe
MIRROR of https://codeberg.org/catseye/Maxixe : A simple proof checker
Language: Python - Size: 53.7 KB - Last synced at: 15 days ago - Pushed at: over 1 year ago - Stars: 10 - Forks: 0
krobelus/rate
DRAT/DPR proof checker
Language: Rust - Size: 5.67 MB - Last synced at: 11 months ago - Pushed at: about 3 years ago - Stars: 9 - Forks: 1
math-o-matic/math-o-matic
Computerized proof system on the web
Language: TypeScript - Size: 5.62 MB - Last synced at: 9 months ago - Pushed at: over 1 year ago - Stars: 6 - 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 at: about 2 months ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 0
catseye/Eqthy
MIRROR of https://codeberg.org/catseye/Eqthy : A simple formalized language for equational proofs
Language: Python - Size: 104 KB - Last synced at: 15 days ago - Pushed at: over 1 year ago - Stars: 4 - Forks: 1
pro465/nnoq
not noq
Language: Rust - Size: 94.7 KB - Last synced at: 11 months ago - Pushed at: over 1 year ago - Stars: 4 - Forks: 1
andrew222651/semkon
LLM-based proof checker for codebases
Language: Python - Size: 73.2 KB - Last synced at: 15 days ago - Pushed at: 3 months ago - Stars: 3 - Forks: 0
skius/imp
Big-step, small-step and axiomatic semantics for the IMP language (unofficial)
Language: Rust - Size: 146 KB - Last synced at: about 1 month ago - Pushed at: over 3 years ago - Stars: 3 - Forks: 0
MDeiml/attomath
A system for formalizing and proving mathematical theorems inspired by Metamath
Language: Objective-C++ - Size: 15.3 MB - Last synced at: 20 days ago - Pushed at: almost 3 years ago - Stars: 2 - Forks: 0
pro465/nyaya
proof language based on https://en.wikipedia.org/wiki/Sequent_calculus and https://us.metamath.org/.
Language: Rust - Size: 46.9 KB - Last synced at: 5 months ago - Pushed at: over 1 year ago - Stars: 1 - Forks: 0
vefthym/dr-prolog-proof-checker
Automatically exported from code.google.com/p/dr-prolog-proof-checker
Language: OpenEdge ABL - Size: 230 KB - Last synced at: about 2 years ago - Pushed at: about 10 years ago - Stars: 1 - Forks: 0
andreiarusoaie/certifying-unification-in-aml
This repo contains a series of Maude scripts for generating and checking proof certificates for syntactic unification in (Applicative) Matching Logic.
Language: Python - Size: 1.33 MB - Last synced at: over 1 year ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
hacker-DOM/provio-2019
Provio will be a step-by-step math proof checker
Language: TypeScript - Size: 1.16 MB - Last synced at: 1 day ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0
Realiserad/beviskoll
Validation of proof in natural deduction.
Language: Prolog - Size: 15.6 KB - Last synced at: 5 days ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
Realiserad/ctl-tester
Program for testing CTL formulas.
Language: Prolog - Size: 110 KB - Last synced at: 5 days ago - Pushed at: over 3 years ago - Stars: 0 - Forks: 0
BendeguzToth/Xcuuuse
Proof checker for natural deduction.
Language: Haskell - Size: 91.8 KB - Last synced at: over 1 year ago - Pushed at: over 5 years ago - Stars: 0 - Forks: 0
wfica/proof_checker
Proof checker implementation in OCaml.
Language: OCaml - Size: 74.2 KB - Last synced at: about 2 years ago - Pushed at: almost 7 years ago - Stars: 0 - Forks: 0
