Abstract

The purpose of this papers to show a technique to automatically certify answers coming from a non-trustable theorem prover. As an extreme consequence, the development of non-sound theorem provers has been considered and investigated, in order to evaluate their relative efficiency on particular classes of difficult theorems.The presentation will consider as a case study, a tableau-based theorem prover for first-order intuitionistic logic without equality