Analytic tableau based minimal model generator, model checker and theorem prover for first-order logic with modal extensions

New version of the PML language and (classical) proof assistant

A propositional logic library.

An Agda formalization of "division by 2" in classical ZF without choice.

Propositional theorem prover - resolution with pure literal elimination and subsumption elimination, implemented in ISO Prolog. Educational software.

Algorithmic Truth Table Method for Proving Validity of Argument Forms

Trying to build logic & proof system library on TypeScript.

Présentation de l'article Focalisation and Classical Realizability de Guillaume Munch-Maccagnoni.

Intuitionistic and classical propositional logic library