Automatic code generation for Scala functions and expressions via the Curry-Howard isomorphism

An exhaustive list of all Rust resources regarding automated or semi-automated formalization efforts in any area, constructive mathematics, formal algorithms, and program verification.

a theorem prover for intuitionistic propositional logic in Idris, with metaprogramming features

Parser and pretty printer for the TPTP language

クヌース・ベンディックス完備化アルゴリズムの OCaml 実装

A Language for the Specification and Efficient Implementation of Type Systems

Towards an Automated Geometer

Automated theorem prover for Reasoning @ UoB

This is a repository for my Master's thesis LaTeX source.

Work-in-progress. Small helper Python functions I made while working for LaiTeP in NOVA (Laboratory for Augmented Intelligence in Theorem Proving). ProverX is an extension of Prover9 and is automated theorem prover available at http://proverx.com

Resolution-based theorem proving for propositional logic in Haskell

Graphical Tableaux Prover for Propositional-, First Order Predicate-, Intuitionistic Propositional- and Intuitionistic First Order Predicate Logic

Extract TPTP problems from a TSTP trace and reconstruct the proof in lambdapi (λΠ-calculus modulo theory).

Haskell interface to automated theorem provers

Basic tableau prover written in ocaml