Proof assistant based on the λΠ-calculus modulo rewriting

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

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

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

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

DRAT/DPR proof checker

Computerized proof system on the web

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

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

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

not noq

A system for formalizing and proving mathematical theorems inspired by Metamath

proof language based on https://en.wikipedia.org/wiki/Sequent_calculus and https://us.metamath.org/.

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

Proof checker for natural deduction.

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

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

Program for testing CTL formulas.

Proof checker implementation in OCaml.

Validation of proof in natural deduction.