Constructive Decision via Redundancy-Free Proof-Search

Abstract

We give a constructive account of Kripke–Curry’s method which was used to establish the decidability of implicational relevance logic (\(\mathbf{R}_{{\rightarrow }}\)). To sustain our approach, we mechanize this method in axiom-free Coq, abstracting away from the specific features of \(\mathbf{R}_{{\rightarrow }}\) to keep only the essential ingredients of the technique. In particular we show how to replace Kripke/Dickson’s lemma by a constructive form of Ramsey’s theorem based on the notion of almost full relation. We also explain how to replace König’s lemma with an inductive form of Brouwer’s Fan theorem. We instantiate our abstract proof to get a constructive decision procedure for \(\mathbf{R}_{{\rightarrow }}\) and discuss potential applications to other logical decidability problems.

This is a preview of subscription content, log in to check access.

Fig. 1
Fig. 2
Fig. 3

Notes

  1. 1.

    https://coq.inria.fr.

  2. 2.

    As for coverability in BVASS, it seems that the arguments developed in [7] cannot easily be converted to constructive ones (private communication with S. Demri).

  3. 3.

    i.e. they are identical when ignoring repetitions and permutations.

  4. 4.

    Dickson’s lemma states that under product order, \(\mathbb {N}^k\) is a WQO for any \(k\in \mathbb {N}\).

  5. 5.

    Moreover, in type theory, the function type subsumes logical implication via the BHK interpretation where proofs of \(A\mathbin {\rightarrow }B\) are viewed as functions mapping proofs of A to proofs of B.

  6. 6.

    Unrestricted contraction would generate infinitely branching proof-search.

  7. 7.

    This result is known as Dickson’s lemma when restricted to \(\mathbb {N}^k\) with the point-wise product order. The inclusion relation between multisets built from the finite set \(\mathcal S\) is a particular case of the product order \(\mathbb {N}^k\) where k is the cardinal of \(\mathcal S\).

  8. 8.

    The Coq standard library is documented at https://coq.inria.fr/library.

  9. 9.

    We temporarily use letters like R or S to represent binary redundancy relations because some of the next results involve several of such relations.

  10. 10.

    see Corollary  below.

  11. 11.

    Typically, systems which include a cut-rule do not satisfy the property which is why cut-elimination is viewed as a critical requisite to design sequent-based decision procedures. The same remark holds for the modus-ponens rule of Hilbert systems, usually making them unsuited for decision procedures.

  12. 12.

    For this, we need a notion of sub-statement that is reflexive, transitive and such that valid rules instances possess the sub-statement property.

  13. 13.

    See http://www.loria.fr/~larchey/Kruskal.

References

  1. 1.

    Bimbó, K.: The decidability of the intensional fragment of classical linear logic. Theor. Comput. Sci. 597, 1–17 (2015)

    MathSciNet  Article  Google Scholar 

  2. 2.

    Bimbó, K., Dunn, J.M.: On the decidability of implicational ticket entailment. J. Symb. Log. 78(1), 214–236 (2013)

    MathSciNet  Article  Google Scholar 

  3. 3.

    Coquand, T.: A direct proof of the intuitionistic Ramsey Theorem. In: Pitt D.H., Curien PL., Abramsky S., Pitts A.M., Poigné A., Rydeheard D.E. (eds) Category Theory and Computer Science. CTCS 1991. Lecture Notes in Computer Science, vol 530, pp. 164–172. Springer (1991)

  4. 4.

    Coquand, T.: Constructive topology and combinatorics. In: Myers J.P., O’Donnell M.J. (eds) Constructivity in Computer Science. Constructivity in CS 1991. Lecture Notes in Computer Science, vol 613, pp. 159–164. Springer (1992)

  5. 5.

    Curry, H.B.: A Theory of Formal Deductibility. Notre Dame mathematical lectures. University of Notre Dame, Notre Dame (1957)

    Google Scholar 

  6. 6.

    Dawson, J.E., Goré, R.: Issues in Machine-Checking the Decidability of Implicational Ticket Entailment. In: TABLEAUX 2017, LNAI, vol. 10501, pp. 347–363. Springer International Publishing, Berlin (2017)

  7. 7.

    Demri, S., Jurdziński, M., Lachish, O., Lazić, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. Syst. Sci. 79(1), 23–38 (2012). https://doi.org/10.1016/j.jcss.2012.04.002

    MathSciNet  Article  MATH  Google Scholar 

  8. 8.

    Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and Primitive-Recursive Bounds with Dickson’s Lemma. LICS 2011, 269–278 (2011). https://doi.org/10.1109/LICS.2011.39

    MathSciNet  Article  Google Scholar 

  9. 9.

    Figueira, D., Lazic, R., Leroux, J., Mazowiecki, F., Sutre, G.: Polynomial-Space Completeness of Reachability for Succinct Branching VASS in Dimension One. In: ICALP 2017, LIPIcs, vol. 80, pp. 119:1–14. Schloss Dagstuhl (2017). https://doi.org/10.4230/LIPIcs.ICALP.2017.119

  10. 10.

    Fridlender, D.: An Interpretation of the Fan Theorem in Type Theory. In: TYPES’98 Selected Papers, LNCS, vol. 1657, pp. 93–105. Springer, Berlin (1999)

  11. 11.

    Galmiche, D., Méry, D., Pym, D.: The semantics of BI and resource tableaux. Math. Struct. Comput. Sci. 15(6), 1033–1088 (2005). https://doi.org/10.1017/S0960129505004858

    MathSciNet  Article  MATH  Google Scholar 

  12. 12.

    Kripke, S.: The Problem of Entailment (abstract). J. Symb. Log. 24, 324 (1959)

    Article  Google Scholar 

  13. 13.

    Larchey-Wendling, D.: Constructive decision via redundancy-free proof-search. In: Automated Reasoning—9th International Joint Conference, IJCAR 2018, Lecture Notes in Computer Science, vol. 10900, pp. 422–438. Springer, Berlin (2018)

  14. 14.

    Meyer, R.K.: Improved Decision Procedures for Pure Relevant Logic, pp. 191–217. Springer, Dordrecht (2001)

    Google Scholar 

  15. 15.

    Okada, M.: A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theor. Comput. Sci. 281(1–2), 471–498 (2002)

    MathSciNet  Article  Google Scholar 

  16. 16.

    Padovani, V.: Ticket Entailment is decidable. Math. Struct. Comput. Sci. 23(3), 568–607 (2013). https://doi.org/10.1017/S0960129512000412

    MathSciNet  Article  MATH  Google Scholar 

  17. 17.

    Riche, J.: Decision procedure of some relevant logics: a constructive perspective. J. Appl. Non-Class. Log. 15(1), 9–23 (2005)

    MathSciNet  Article  Google Scholar 

  18. 18.

    Riche, J., Meyer, R.K.: Kripke, Belnap, Urquhart and Relevant Decidability & Complexity. In: CSL’99, pp. 224–240. Springer (1999)

  19. 19.

    Schmitz, S.: Implicational Relevance Logic is 2-EXPTIME-Complete. J. Symb. Log. 81(2), 641–661 (2016)

    MathSciNet  Article  Google Scholar 

  20. 20.

    Schmitz, S.: The complexity of reachability in vector addition systems. ACM SIGLOG News 3(1), 4–21 (2016). https://doi.org/10.1145/2893582.2893585

    Article  Google Scholar 

  21. 21.

    Schwichtenberg, H.: A direct proof of the equivalence between Brouwer’s Fan Theorem and König’s Lemma with a uniqueness hypothesis. J. UCS 11(12), 2086–2095 (2005)

    MathSciNet  MATH  Google Scholar 

  22. 22.

    Straßburger, L.: On the decision problem for MELL. Theor. Comput. Sci. 768, 91–98 (2019)

    MathSciNet  Article  Google Scholar 

  23. 23.

    Urquhart, A.: The undecidability of entailment and relevant implication. J. Symb. Log. 49(4), 1059–1073 (1984)

    MathSciNet  Article  Google Scholar 

  24. 24.

    Veldman, W., Bezem, M.: Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. J. Lond. Math. Soc. s2–47(2), 193–211 (1993). https://doi.org/10.1112/jlms/s2-47.2.193

    MathSciNet  Article  MATH  Google Scholar 

  25. 25.

    Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full—adventures in constructive termination. In: ITP 2012, LNCS, vol. 7406, pp. 250–265 (2012)

Download references

Author information

Affiliations

Authors

Corresponding author

Correspondence to Dominique Larchey-Wendling.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Work partially supported by the joint project ANR-FWF TICAMORE (No. ANR-16-CE91-0002).

Rights and permissions

Reprints and Permissions

About this article

Verify currency and authenticity via CrossMark

Cite this article

Larchey-Wendling, D. Constructive Decision via Redundancy-Free Proof-Search. J Autom Reasoning (2020). https://doi.org/10.1007/s10817-020-09555-y

Download citation

Keywords

  • Constructive decidability
  • Relevance logic
  • Sequent calculi
  • Contraction rule
  • Redundancy-free search
  • Almost full relations
  • Mechanization in Coq

Mathematics Subject Classification

  • 03F03
  • 03B35
  • 03B47