Top

Published in:

2018 | OriginalPaper | Chapter

Constructive Decision via Redundancy-Free Proof-Search

Author : Dominique Larchey-Wendling

Published in: Automated Reasoning

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter A FOOLish Encoding of the Next State Relations of Imperative Programs

next chapter Deciding the First-Order Theory of an Algebra of Feature Trees with Updates

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

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

Unrestricted contraction would generate infinitely branching proof-search.

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

The braces around

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_28/464406_1_En_28_IEq189_HTML.gif

specify an implicit argument.

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_28/464406_1_En_28_IEq196_HTML.gif

and _

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_28/464406_1_En_28_IEq197_HTML.gif

_ are shorthand notations for the two list constructors.

The notation

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_28/464406_1_En_28_IEq208_HTML.gif

is a shortcut for

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_28/464406_1_En_28_IEq209_HTML.gif

, the (finitary) membership predicate.

Typically, systems which include a cut-rule do not satisfy the

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_28/464406_1_En_28_IEq233_HTML.gif

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.

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

Branches are read from the root to leaves, hence the use of

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94205-6_28/464406_1_En_28_IEq283_HTML.gif

to reverse lists.

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

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

Coquand, T.: A direct proof of the intuitionistic Ramsey theorem. In: Pitt, D.H., Curien, P.-L., Abramsky, S., Pitts, A.M., Poigné, A., Rydeheard, D.E. (eds.) CTCS 1991. LNCS, vol. 530, pp. 164–172. Springer, Heidelberg (1991). https://doi.org/10.1007/BFb0013465CrossRef

Coquand, T.: Constructive topology and combinatorics. In: Myers, J.P., O’Donnell, M.J. (eds.) Constructivity in CS 1991. LNCS, vol. 613, pp. 159–164. Springer, Heidelberg (1992). https://doi.org/10.1007/BFb0021089CrossRef

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

Dawson, J.E., Goré, R.: Issues in machine-checking the decidability of implicational ticket entailment. In: Schmidt, R.A., Nalon, C. (eds.) TABLEAUX 2017. LNCS, vol. 10501, pp. 347–363. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-66902-1_21CrossRef

Demri, S., Jurdziński, M., Lachish, O., Lazić, R.: The covering and boundedness problems for branching vector addition systems. J. Comput. System Sci. 79(1), 23–38 (2012)MathSciNetCrossRef

Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermannian and primitive-recursive bounds with Dickson’s lemma. In: LICS 2011, pp. 269–278 (2011)

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)

10.

Fridlender, D.: An interpretation of the fan theorem in type theory. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 93–105. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48167-2_7CrossRef

11.

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

12.

Kripke, S.: The problem of entailment (abstract). J. Symb. Log. 24, 324 (1959)CrossRef

13.

Larchey-Wendling, D.: A mechanized inductive proof of Kruskal’s tree theorem (2015). http://www.loria.fr/~larchey/Kruskal

14.

Larchey-Wendling, D.: A constructive mechanization of Kripke-Curry’s method for the decidability of implicational relevance logic (2018). https://github.com/DmxLarchey/Relevant-decidability

15.

Meyer, R.K.: Improved decision procedures for pure relevant logic. In: Anderson, C.A., Zelëny, M. (eds.) Logic, Meaning and Computation. Synthese Library (Studies in Epistemology, Logic, Methodology, and Philosophy of Science), pp. 191–217. Springer, Dordrecht (2001). https://doi.org/10.1007/978-94-010-0526-5_9CrossRef

16.

Padovani, V.: Ticket entailment is decidable. Math. Struct. Comput. Sci. 23(3), 568–607 (2013)MathSciNetCrossRef

17.

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

18.

Riche, J., Meyer, R.K.: Kripke, Belnap, Urquhart and relevant decidability and complexity. In: Gottlob, G., Grandjean, E., Seyr, K. (eds.) CSL 1998. LNCS, vol. 1584, pp. 224–240. Springer, Heidelberg (1999). https://doi.org/10.1007/10703163_16CrossRef

19.

Schmitz, S.: Implicational relevance logic is 2-ExpTime-complete. J. Symb. Log. 81(2), 641–661 (2016)MathSciNetCrossRef

20.

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

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)MathSciNetMATH

22.

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

23.

Veldman, W., Bezem, M.: Ramsey’s theorem and the pigeonhole principle in intuitionistic mathematics. J. Lond. Math. Soc. s2–47(2), 193–211 (1993)MathSciNetCrossRef

24.

Vytiniotis, D., Coquand, T., Wahlstedt, D.: Stop when you are almost-full. In: Beringer, L., Felty, A. (eds.) ITP 2012. LNCS, vol. 7406, pp. 250–265. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-32347-8_17CrossRef

Title: Constructive Decision via Redundancy-Free Proof-Search
Author: Dominique Larchey-Wendling
Publisher: Springer International Publishing
Book: Automated Reasoning
Print ISBN: 978-3-319-94204-9

Electronic ISBN: 978-3-319-94205-6

Copyright Year: 2018
DOI: https://doi.org/10.1007/978-3-319-94205-6_28

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner