Applying the inverse method to refutation calculi
The inverse method, introduced in the 1960s by Maslov , is a saturation based theorem proving technique closely related to (hyper)resolution ; it relies on a forward proof-search strategy and can be applied to cut-free calculi enjoying the subformula property. Given a goal, a set of instances of the rules of the calculus at hand is selected; such specialized rules are repeatedly applied in the forward direction, starting from the axioms (i.e., the rules without premises). Proof-search terminates if either the goal is obtained or the database of proved facts saturates (no new fact can be added). The inverse method has been originally applied to Classical Logic and successively extended to some non-classical logics, see, e.g., [1,3,4,5,6,9].
In all the mentioned papers, the inverse method has been exploited to prove the validity of a goal in a specific logic. We propose the dual approach, where the inverse method is applied to disprove the validity of a formula. We focus on
Intuitionistic Propositional Logic (IPL) and we present a forward refutation calculus to derive the unprovability of a formula in IPL. Our motivation is twofold. Firstly, we aim to define a calculus which is prone to constructively ascertain the unprovability of a formula by providing a concise countermodel for it. Differently from backward proof-search methods, where rules are applied bottom-up, in forward proof-search the proved sequents need not be duplicated; accordingly, the obtained derivations contain few edundancies and the extracted countermodels are in general small. Actually, we can build a derivation of an unprovable formula so that the obtained countermodel has minimal height.
We also aim at clarifying the role of the saturated database yielded by a failed proof-search. In the case of the usual forward calculi for Intuitionistic provability, if proof-search fails, a saturated database is generated which “may be considered a kind of countermodel for the goal sequent” . However, as far as we know, no method has been proposed to effectively extract it. The saturated database obtained by a failed proof-search can be considered as a kind of proof of the goal; we give evidence of this by showing how to extract from such a database a derivation witnessing the Intuitionistic validity of the goal.
The preliminary results of this research have been introduced in , where the forward calculus for IPL and the proof-search procedure are presented. An in-depth discussion of the method and new results (minimality of generated countermodels, extraction of derivations from saturated databases) can be found in . To evaluate the potential of our approach, we have implemented the proof-search procedures in the prover frj, available at http://github.com/ferram/jtabwb_provers/.
We are investigating the applicability of the method to other non-classical propositional logics; so far we have considered the modal logic S4 .
1. T. Brock-Nannestad and K. Chaudhuri. Disproving using the inverse method by iterative refinement of finite approximations. In H. De Nivelle, editor, TABLEAUX 2015, volume 9323 of LNCS, pages 153–168. Springer, 2015.2. A. Chagrov and M. Zakharyaschev. Modal Logic. Oxford University Press, 1997.
3. K. Chaudhuri and F. Pfenning. A focusing inverse method theorem prover for first-order linear logic. In R. Nieuwenhuis, editor, CADE-20, volume 3632 of LNCS, pages 69–83. Springer, 2005.
4. K. Chaudhuri, F. Pfenning, and G. Price. A logical characterization of forward and backward chaining in the inverse method. In U. Furbach et al., editor, IJCAR 2006, volume 4130 of LNCS, pages 97–111. Springer, 2006.
5. A. Degtyarev and A. Voronkov. The inverse method. In J.A. Robinson et al., editor, Handbook of Automated Reasoning, pages 179–272. Elsevier and MIT Press, 2001.
6. K. Donnelly, T. Gibson, N. Krishnaswami, S. Magill, and S. Park. The inverse method for the logic of bunched implications. In F. Baader et al., editor, LPAR 2004, volume 3452 of LNCS, pages 466–480. Springer, 2004.
7. C. Fiorentini and M. Ferrari. A forward unprovability calculus for intuitionistic propositional logic. In R. A. Schmidt and C. Nalon, editors, TABLEAUX 2017, volume 10501 of LNCS, pages 114–130. Springer, 2017.
8. C. Fiorentini and M. Ferrari. Duality between unprovability and provability in forward proof-search for intuitionistic propositional logic. CoRR, arXiv:1804.06689, 2018.
9. L. Kovács, A. Mantsivoda, and A. Voronkov. The inverse method for many-valued logics. In F. Castro-Espinoza et al., editor, MICAI 2013, volume 8265 of LNCS, pages 12–23. Springer, 2013.
10. S. Ju. Maslov. An invertible sequential version of the constructive predicate calculus. Zap. Naučn. Sem. Leningrad. Otdel. Mat. Inst. Steklov. (LOMI), 4:96–111, 1967.
11. S. McLaughlin and F. Pfenning. Imogen: Focusing the polarized inverse method for intuitionistic propositional logic. In I. Cervesato et al., editor, LPAR 2008, volume 5330 of LNCS, pages 174–181. Springer, 2008