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. 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, which is appropriate for constructively ascertaining the unprovability of a formula G by providing a concise countermodel for it; in particular, we prove that the generated countermodels have minimal height. Moreover, we clarify the role of the saturated database obtained as a result of a failed proof search in FRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.
Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic
Fiorentini, Camillo
;Ferrari, Mauro
2020-01-01
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. 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, which is appropriate for constructively ascertaining the unprovability of a formula G by providing a concise countermodel for it; in particular, we prove that the generated countermodels have minimal height. Moreover, we clarify the role of the saturated database obtained as a result of a failed proof search in FRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.File | Dimensione | Formato | |
---|---|---|---|
2020-fiofer-DualityBetweenUnprovabilityAndProvabilityInForwardRefutation-searchForIPL-tocl.pdf
non disponibili
Tipologia:
Versione Editoriale (PDF)
Licenza:
Copyright dell'editore
Dimensione
2.1 MB
Formato
Adobe PDF
|
2.1 MB | Adobe PDF | Visualizza/Apri Richiedi una copia |
I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.