An open API service providing repository metadata for many open source software ecosystems.

GitHub topics: proof-checking

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: 4 days ago - Pushed at: over 1 year ago - Stars: 2 - 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: 2 months ago - Pushed at: over 1 year ago - Stars: 6 - Forks: 0

lukaszcz/hcpl

A prototypical proof checker and programming language based on illative combinatory logic

Language: OCaml - Size: 350 KB - Last synced at: 20 days ago - Pushed at: 8 months ago - Stars: 3 - Forks: 0

surajx/proof-assistant

Online platform to enable Logic students to write, verify, and store System L style Natural Deduction proofs with real-time proof-checking

Language: JavaScript - Size: 1.24 MB - Last synced at: about 1 month ago - Pushed at: almost 7 years ago - Stars: 11 - Forks: 3

pro465/nnoq

not noq

Language: Rust - Size: 94.7 KB - Last synced at: 4 days ago - Pushed at: over 1 year ago - Stars: 3 - Forks: 1

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: about 1 month ago - Pushed at: over 1 year ago - Stars: 14 - Forks: 2

catseye/Maxixe

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

Language: Python - Size: 53.7 KB - Last synced at: about 1 month ago - Pushed at: over 1 year ago - Stars: 10 - 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: about 1 month ago - Pushed at: over 1 year ago - Stars: 4 - Forks: 1

milesrout/minimal-logic

a proof checker and model checker for minimal propositional logic

Language: Haskell - Size: 19.5 KB - Last synced at: almost 2 years ago - Pushed at: almost 7 years ago - Stars: 2 - Forks: 0

sacerdot/Minimalist-Type-Theory-In-Lambda-Prolog

An implementation in Lambda-Prolog of the Minimalist Type Theory

Language: Prolog - Size: 9.43 MB - Last synced at: about 1 month ago - Pushed at: over 6 years ago - Stars: 4 - Forks: 3

hacker-DOM/provio-2019

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

Language: TypeScript - Size: 1.16 MB - Last synced at: 7 days ago - Pushed at: over 2 years ago - Stars: 0 - Forks: 0