Duality between Unprovability and Provability in Forward Refutation-search for Intuitionistic Propositional Logic
Camillo Fiorentini, Mauro Ferrari · ACM Transactions on Computational Logic · 2020
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 formulaGin Intuitionistic Propositional Logic. To this aim we design a forward calculusFRJ(G) for Intuitionistic unprovability, which is appropriate for constructively ascertaining the unprovability of a formulaGby 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 inFRJ(G) by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.