Proof assistant based on the λΠ-calculus modulo rewriting

• UpdatedMar 14, 2025
• OCaml

MIRROR ofhttps://codeberg.org/catseye/Philomath : An LCF-style theorem prover written in C89 (a.k.a ANSI C)

• UpdatedDec 19, 2023
• C

[wip] Proof format and checker for first-order and higher-order theorem provers

• UpdatedMar 29, 2023
• OCaml

[wip] A LCF-style kernel of trust intended for certified ATP and proof checking for FOL/HOL.

• UpdatedJan 25, 2024
• OCaml

MIRROR ofhttps://codeberg.org/catseye/Maxixe : A simple proof checker

• UpdatedNov 10, 2023
• Python

DRAT/DPR proof checker

• UpdatedFeb 12, 2022
• Rust

Computerized proof system on the web

• UpdatedJan 10, 2024
• TypeScript

Exposition of an LCF-style theorem prover for propositional logic in a Natural Deduction system

• UpdatedOct 31, 2023

MIRROR ofhttps://codeberg.org/catseye/Eqthy : A simple formalized language for equational proofs

• UpdatedNov 10, 2023
• Python

LLM-based proof checker for codebases

• UpdatedFeb 4, 2025
• Python

not noq

• UpdatedOct 23, 2023
• Rust

Big-step, small-step and axiomatic semantics for the IMP language (unofficial)

• UpdatedOct 25, 2021
• Rust

proof language based onhttps://en.wikipedia.org/wiki/Sequent_calculus andhttps://us.metamath.org/.

• UpdatedJan 23, 2024
• Rust

A system for formalizing and proving mathematical theorems inspired by Metamath

• UpdatedJun 13, 2022
• Objective-C++

Automatically exported from code.google.com/p/dr-prolog-proof-checker

• UpdatedMar 28, 2015
• OpenEdge ABL

Proof checker for natural deduction.

• UpdatedDec 31, 2019
• Haskell

Provio will be a step-by-step math proof checker

• UpdatedJan 4, 2023
• TypeScript

This repo contains a series of Maude scripts for generating and checking proof certificates for syntactic unification in (Applicative) Matching Logic.

• UpdatedJan 12, 2023
• Python

Program for testing CTL formulas.

• UpdatedNov 12, 2021
• Prolog

Proof checker implementation in OCaml.

• UpdatedJun 22, 2018
• OCaml