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 [ABM99].
|Data di pubblicazione:||2001|
|Titolo:||How to Avoid the Formal Verification of a Theorem Prover|
|Rivista:||LOGIC JOURNAL OF THE IGPL|
|Appare nelle tipologie:||Articolo su Rivista|