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 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 / C. Fiorentini, M. Ferrari. - In: ACM TRANSACTIONS ON COMPUTATIONAL LOGIC. - ISSN 1529-3785. - 21:3(2020), pp. 22.1-22.47. [10.1145/3372299]

Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic

C. Fiorentini;M. Ferrari
2020

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 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.
Proof-search procedures; intuitionistic propositional logic; sequent calculi
Settore INF/01 - Informatica
Settore MAT/01 - Logica Matematica
2020
Article (author)
File in questo prodotto:
File Dimensione Formato  
2020_TOCL_DualityUnprovabilityProvabilityForwardRefSearchIPL.pdf

accesso riservato

Tipologia: Publisher's version/PDF
Dimensione 2.08 MB
Formato Adobe PDF
2.08 MB 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.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/2434/717904
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 3
  • ???jsp.display-item.citation.isi??? 2
social impact