Proof in first order logic by resolution

, par Michel Lévy

Given a list of clauses, as well as limits on the time of proof and the size of the clauses, the software tries to build a proof of the empty clause within the imposed limits.

Voir en ligne : http://teachinglogic.liglab.fr/ResBinSc/