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.

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

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

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

Intuitionistic and classical propositional logic library

Algorithmic Truth Table Method for Proving Validity of Argument Forms