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].
How to Avoid the Formal Verification of a Theorem Prover
BENINI, MARCO;
2001-01-01
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 [ABM99].
File in questo prodotto:
| File | Dimensione | Formato | |
|---|---|---|---|
|
main.pdf
non disponibili
Tipologia:
Documento in Pre-print
Licenza:
DRM non definito
Dimensione
292.48 kB
Formato
Adobe PDF
|
292.48 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.
