proof-checker
There are 21 repositories under proof-checker topic.
Deducteam/lambdapi
Proof assistant based on the λΠ-calculus modulo rewriting
catseye/Philomath
MIRROR of https://codeberg.org/catseye/Philomath : An LCF-style theorem prover written in C89 (a.k.a ANSI C)
c-cube/quip
[wip] Proof format and checker for first-order and higher-order theorem provers
c-cube/trustee
[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.
catseye/Maxixe
MIRROR of https://codeberg.org/catseye/Maxixe : A simple proof checker
krobelus/rate
DRAT/DPR proof checker
math-o-matic/math-o-matic
Computerized proof system on the web
cpressey/LCF-style-ND
Exposition of an LCF-style theorem prover for propositional logic in a Natural Deduction system
catseye/Eqthy
MIRROR of https://codeberg.org/catseye/Eqthy : A simple formalized language for equational proofs
pro465/nnoq
not noq
skius/imp
Big-step, small-step and axiomatic semantics for the IMP language (unofficial)
MDeiml/attomath
A system for formalizing and proving mathematical theorems inspired by Metamath
BendeguzToth/Xcuuuse
Proof checker for natural deduction.
pro465/nyaya
proof language based on https://en.wikipedia.org/wiki/Sequent_calculus and https://us.metamath.org/.
vefthym/dr-prolog-proof-checker
Automatically exported from code.google.com/p/dr-prolog-proof-checker
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.
ChinmayMittal/COL703-Logic-For-CS
Logic for Computer Science, Course Repository, IITD 7th Semester 2023-24
hacker-DOM/provio-2019
Provio will be a step-by-step math proof checker
Realiserad/beviskoll
Validation of proof in natural deduction.
Realiserad/ctl-tester
Program for testing CTL formulas.
wfica/proof_checker
Proof checker implementation in OCaml.