Forward proof-search and Countermodel Construction in Intuitionistic Propositional Logic?

Abstract

In this extended abstract we review some recent work about the application of the inverse method to refute formulas in Intuitionistic Propositional Logic. The inverse method, introduced in the 1960s by Maslov [21], is a saturation based theorem proving technique closely related to (hyper)resolution [7]; 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). As pointed out by Vladimir Lifschitz [20], \the role of the inverse method in the Soviet work on proof procedures for predicate logic can be compared to the role of resolution method in theorem proving projects in the West". But, he regrets, \for a number of reasons, this work has not been duly appreciated outside a small circle of Maslov's associates". The method has been popularized by Degtyarev and Voronkov [7], who provide the general recipe to design forward calculi, with applications to Classical Predicate Logic and some non-classical logics. Further extensions can be found in [2,8,19]. A signi cant investigation is presented in [4,5], where focused calculi and polarization of formulas are exploited to reduce the search space in forward proof-search for Intuitionistic Logic. These techniques are at the heart of the design of the prover Imogen [22]. In all the mentioned papers, the inverse method has been exploited to prove the validity of a goal in a speci c logic. In [15,16] we follow the dual approach, namely: we design a forward calculus to derive refutations asserting the unprovability of a goal formula in Intuitionistic Propositional Logic (IPL). Our motivation is twofold. Firstly, we aim to de ne a refutation calculus which constructively ascertains the unprovability of a formula by providing a concise coun? Copyright c 2020 for this paper by its authors. Use permitted under Creative Commons License Attribution 4.0 International (CC BY 4.0). This extended abstract is a summary of [16].

-

termodel for it3. The second motivation is to clarify the role of the saturated database obtained when the search for a refutation (refutation-search) fails. 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" [ 22 ]. However, as far as we know, no method has been proposed to e ectively extract it. Actually, the main problem comes from the high level of non-determinism involved in the construction of countermodels. Here, assuming the dual approach, the saturated database generated by a failed refutation-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 formula to be proved (the goal formula) determines the instances of the rules of the forward calculus. The calculus we de ne is parametrized by the goal formula G (where the goal is to prove that G is not valid in IPL). We call the related calculus FRJ(G) (Forward Refutation calculus for IPL parametrized by G); formulas occurring in the sequents of FRJ(G) are suitable subformulas of G. In [ 16 ] we de ne a forward refutation-search procedure to build an FRJ(G)refutation of a goal formula G, namely an FRJ(G)-refutation of a sequent of the form ; G, meaning that G is not derivable in IPL from assumptions . This is a standard saturation procedure where the derivable sequents of FRJ(G) are collected step-by-step in a database DG. To avoid redundancies and maintain DG compact, we introduce a subsumption relation between sequents; for instance, if at some step is proved and is subsumed by a sequent already in DG, then is discarded and not added to DG (forward subsumption).

If the formula G is valid in IPL, refutation-search for G fails (indeed, no FRJ(G)-refutation of G can be built) and we eventually get a saturated database DG for G. This means that for every sequent derivable in FRJ(G), DG contains a sequent 0 which subsumes ; thus DG is in some sense representative of all the sequents derivable in FRJ(G). We can exploit DG to build a derivation of G in a sequent calculus for IPL. To this aim, we introduce the sequent calculus Gbu(G), a variant of the well-known sequent calculus G3i [ 25 ]. From a Gbu(G)derivation of G, we can immediately obtain a G3i-derivation of G. Di erently from G3i, backward proof-search in Gbu(G) always terminates; indeed, we can de ne a weight function on sequents such that, after the backward application of a rule of Gbu(G) to a sequent, the weight of the sequents decreases. Nonetheless, backward-proof search in Gbu(G) might present several backtrack points, in correspondence of the applications of rules for left implication and right disjunction. The crucial point is that we can remove backtracking by exploiting the database DG: in presence of multiple non-deterministic choices, we query DG as an oracle to select the right way so to successfully continue proof-search. Thus, we can consider DG as a proof-certi cate of the validity of G, in the sense that it contains enough information to reconstruct a derivation of G in the sequent calculus G3i. In general DG is not unique; however, if we eliminate all the re3 Note that our use of the term refutation is di erent from the one in the context of resolution, where it is about establishing that False is entailed in all models. dundancies from DG (if belongs to DG, then remove from DG all the sequents subsumed by ), then we get a saturated database DG which is the minimum among the saturated databases of G, hence we can consider DG as the canonical proof-certi cate of the validity of G. To get the minimum saturated database, we have to enhance the refutation-search procedure by implementing backward subsumption. We have experimented that the backtracking-free proof-search in Gbu(G) driven by a saturated database can be more e cient than the usual backward proof-search procedure in G3i.

The rules of FRJ(G) are inspired by Kripke semantics. We show that, from a refutation of G, we can extract a countermodel for G, namely a Kripke model such that, at its root, the formula G is not forced, witnessing that G is not valid in IPL [ 3 ]. Actually, there is a close correspondence between a refutation and the related Kripke model. Thus, our forward refutation-search procedure can be understood as a top-down method to build a countermodel for G, starting from the nal worlds down to the root. This original approach is dual to the standard one, where countermodels are built bottom-up, mimicking the backward application of rules (see, e.g., [ 1,6,9,10,11,17,18,23,24 ]). This di erent viewpoint has a signi cant impact on the outcome. Indeed, the countermodels generated by a backward procedure are always trees, which might contain some redundancies. Instead, forward methods re-use sequents and do not replicate them; thus the generated models are DAGs (Direct Acyclic Graphs) not containing duplications and are in general very concise. As a signi cant example, let us consider the one-variable formulas Ni of the Nishimura family [ 3 ], which are not valid in IPL:

N1 = p N2 = :p

N2n+3 = N2n+1 _ N2n+2 N2n+4 = N2n+3

N2n+1 n 0 For formulas Nj our approach generates the standard \tower-like" minimum countermodel [ 3 ]; e.g. in Fig. 1 we display the countermodel for N17.

We also investigate the relationship between a non-valid formula G and the height of the countermodel extracted from an FRJ(G)-refutation of G. We show that, given a countermodel for G of height h, we can build an FRJ(G)-refutation of G having height at most h. By this fact, we conclude that, if G is not valid in IPL, we can build an FRJ(G)-refutation of G such that the height h of the extracted countermodel is minimal (namely, there exists no countermodel for G having height less than h). Actually, we can tweak the refutation-search procedure so that, if G is not valid, it yields an FRJ(G)-refutation of G such that the extracted countermodel has minimal height. However, in general the obtained models are not minimal in the number of worlds, and the de nition of a calculus devoted to the construction of minimal models (in the number of worlds) seems to be challenging. A di erent approach to generate minimal models, exploiting Answer Set Programming, is presented in [ 14 ].

To evaluate the potential of our approach we have implemented frj, a Java prototype of our refutation-search procedure based on the JTabWb framework [ 12 ]4. frj implements term-indexing, forward and backward subsumption 4 frj is available at http://github.com/ferram/jtabwb_provers/. and it allows the user to generate the rendering of proofs and of the extracted countermodels. We point out that the minimal countermodel in Fig. 1 has been generated by frj; the other provers we have tested fail to get such a concise countermodel.

As a future work we plan to investigate the applicability of our method to other logics, in particular to modal logics (see [ 13 ] for a preliminary work) and intermediate logics such as Godel-Dummett logic characterized by linear Kripke models.

Acknowledgments This work has been partially funded by the INdAM-GNCS project 2019 \METALLIC #2: METodi di prova per il ragionamento Automatico per Logiche noncLassIChe #2".

References

1. A. Avellone , C. Fiorentini , and A. Momigliano . A semantical analysis of focusing and contraction in intuitionistic logic . Fundamenta Informaticae , 140 ( 3-4 ): 247 { 262 , 2015 .

2. T. Brock-Nannestad and K. Chaudhuri . Disproving using the inverse method by iterative re nement of nite approximations . In H. De Nivelle, editor, TABLEAUX 2015 , volume 9323 of LNCS , pages 153 { 168 . Springer, 2015 .

3. A. Chagrov and M. Zakharyaschev . Modal Logic . Oxford University Press, 1997 .

4. K. Chaudhuri and F. Pfenning . A focusing inverse method theorem prover for rstorder linear logic . In R. Nieuwenhuis, editor, CADE-20 , volume 3632 of LNCS , pages 69 { 83 . Springer, 2005 .

5. 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 .

6. K. Claessen and D. Rosen . SAT modulo intuitionistic implications . In M. Davis, A. Fehnker , A. McIver, and A . Voronkov, editors, Logic for Programming , Arti cial Intelligence, and Reasoning - 20th International Conference , LPAR-20 2015 , Suva, Fiji, November 24-28 , 2015 , Proceedings, volume 9450 , pages 622 { 637 . Springer, 2015 .

7. 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 .

8. 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 .

9. M. Ferrari , C. Fiorentini , and G. Fiorino. FCube : An e cient prover for intuitionistic propositional logic . In C. G. Fermuller et al., editor, LPAR 2010 , volume 6397 of LNCS , pages 294 { 301 . Springer, 2010 .

10. M. Ferrari , C. Fiorentini , and G. Fiorino . Contraction-free linear depth sequent calculi for intuitionistic propositional logic with the subformula property and minimal depth counter-models . Journal of Automated Reasoning , 51 ( 2 ): 129 { 149 , 2013 .

11. M. Ferrari , C. Fiorentini , and G. Fiorino. An evaluation-driven decision procedure for G3i . ACM Transactions on Computational Logic (TOCL) , 16 ( 1 ):8: 1 {8: 37 , 2015 .

12. M. Ferrari , C. Fiorentini , and G. Fiorino. JTabWb: a Java framework for implementing terminating sequent and tableau calculi . Fundamenta Informaticae , 150 : 119 { 142 , 2017 .

13. M. Ferrari , C. Fiorentini , and Fiorino G. Forward countermodel construction in modal logic K . In P. Felli and Montali M, editors, Proceedings of the 33rd Italian Conference on Computational Logic , Bolzano, Italy, September 20-22 , 2018 , volume 2214 of CEUR Workshop Proceedings , pages 75 { 81 . CEUR-WS.org, 2018 .

14. C. Fiorentini . An ASP approach to generate minimal countermodels in intuitionistic propositional logic . In Sarit Kraus, editor, Proceedings of the Twenty-Eighth International Joint Conference on Arti cial Intelligence , IJCAI 2019 , Macao, China, August 10-16 , 2019 , pages 1675 { 1681. ijcai.org, 2019 .

15. 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 .

16. C. Fiorentini and M. Ferrari . Duality between unprovability and provability in forward refutation-search for intuitionistic propositional logic . ACM Trans. Comput. Logic , 21 ( 3 ), March 2020 .

17. C. Fiorentini , R. Gore , and S. Graham-Lengrand . A proof-theoretic perspective on SMT-solving for intuitionistic propositional logic . In S. Cerrito and A . Popescu, editors, TABLEAUX 2019 , volume 11714 of LNCS , pages 111 { 129 . Springer, 2019 .

18. R. Gore and L. Postniece . Combining derivations and refutations for cut-free completeness in bi-intuitionistic logic . Journal of Logic and Computation , 20 ( 1 ): 233 { 260 , 2010 .

19. L. Kovacs , 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 .

20. V. Lifschitz . What is the inverse method ? J. Automat . Reason., 5 ( 1 ):1{ 23 , 1989 .

21. S. Ju. Maslov. An invertible sequential version of the constructive predicate calculus . Zap. Naucn. Sem. Leningrad. Otdel. Mat. Inst. Steklov. (LOMI) , 4 : 96 { 111 , 1967 .

22. 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 .

23. S. Negri . Proofs and countermodels in non-classical logics . Logica Universalis , 8 ( 1 ): 25 { 60 , 2014 .

24. L. Pinto and R. Dyckho . Loop-free construction of counter-models for intuitionistic propositional logic . In Behara et al., editor, Symposia Gaussiana, Conference A , pages 225 { 232 . Walter de Gruyter, Berlin, 1995 .

25. A.S. Troelstra and H. Schwichtenberg . Basic Proof Theory , volume 43 of Cambridge Tracts in Theoretical Computer Science. Camb. Univ. Press, 2ed edition , 2000 .