The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. This method has been successfully applied to a variety of logics. Here we apply this method to derive the unprovability of a goal formula G in Intuitionistic Propositional Logic. To this aim we design a forward calculus FRJ(G) for Intuitionistic unprovability. From a derivation of G in FRJ(G) we can extract a Kripke countermodel for G. Since in forward methods sequents are not duplicated, the generated countermodels do not contain redundant worlds and are in general very concise.
A Forward Unprovability Calculus for Intuitionistic Propositional Logic / C. Fiorentini, M. Ferrari (LECTURE NOTES IN ARTIFICIAL INTELLIGENCE). - In: Automated Reasoning with Analytic Tableaux and Related Methods / [a cura di] R A. Schmidt, C. Nalon. - Prima edizione. - [s.l] : Springer International Publishing, 2017 Sep. - ISBN 9783319669014. - pp. 114-130 (( Intervento presentato al 26. convegno Tableaux tenutosi a Brasilia nel 2017.
A Forward Unprovability Calculus for Intuitionistic Propositional Logic
C. FiorentiniPrimo
;
2017
Abstract
The inverse method is a saturation based theorem proving technique; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. This method has been successfully applied to a variety of logics. Here we apply this method to derive the unprovability of a goal formula G in Intuitionistic Propositional Logic. To this aim we design a forward calculus FRJ(G) for Intuitionistic unprovability. From a derivation of G in FRJ(G) we can extract a Kripke countermodel for G. Since in forward methods sequents are not duplicated, the generated countermodels do not contain redundant worlds and are in general very concise.File | Dimensione | Formato | |
---|---|---|---|
2017_tableaux.pdf
accesso riservato
Tipologia:
Publisher's version/PDF
Dimensione
895.84 kB
Formato
Adobe PDF
|
895.84 kB | Adobe PDF | Visualizza/Apri Richiedi una copia |
Pubblicazioni consigliate
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.