On the Length of Medial-Switch-Mix Derivations | SpringerLink
Skip to main content
Springer Nature Link
Log in

On the Length of Medial-Switch-Mix Derivations

  • Conference paper
  • First Online:
Logic, Language, Information, and Computation (WoLLIC 2017)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10388))

Abstract

Switch and medial are two inference rules that play a central role in many deep inference proof systems. In specific proof systems, the mix rule may also be present. In this paper we show that the maximal length of a derivation using only the inference rules for switch, medial, and mix, modulo associativity and commutativity of the two binary connectives involved, is quadratic in the size of the formula at the conclusion of the derivation. This shows, at the same time, the termination of the rewrite system.

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

Access this chapter

Log in via an institution

Subscribe and save

Springer+ Basic
¥17,985 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Chapter
JPY 3498
Price includes VAT (Japan)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
JPY 5719
Price includes VAT (Japan)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
JPY 7149
Price includes VAT (Japan)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    The relation web of a formula provides a graph-based representation of a formula in deep inference contextual rewriting, as in [12]. An equivalent definition of the relweb-or-number is the number of edges in the cograph for .

References

  1. Bechet, D., Groote, P., Retoré, C.: A complete axiomatisation for the inclusion of series-parallel partial orders. In: Comon, H. (ed.) RTA 1997. LNCS, vol. 1232, pp. 230–240. Springer, Heidelberg (1997). doi:10.1007/3-540-62950-5_74

    Chapter  Google Scholar 

  2. Blute, R., Cockett, R., Seely, R., Trimble, T.: Natural deduction and coherence for weakly distributive categories. J. Pure Appl. Algebra 113, 229–296 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  3. Brünnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 347–361. Springer, Heidelberg (2001). doi:10.1007/3-540-45653-8_24

    Chapter  Google Scholar 

  4. Bruscoli, P.: A purely logical account of sequentiality in proof search. In: Stuckey, P.J. (ed.) ICLP 2002. LNCS, vol. 2401, pp. 302–316. Springer, Heidelberg (2002). doi:10.1007/3-540-45619-8_21

    Chapter  Google Scholar 

  5. Bruscoli, P., Guglielmi, A.: On the proof complexity of deep inference. ACM Trans. Comput. Logic 10(2), 1–34 (2009). Article 14

    Article  MathSciNet  MATH  Google Scholar 

  6. Bruscoli, P., Guglielmi, A., Gundersen, T., Parigot, M.: A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In: Clarke, E.M., Voronkov, A. (eds.) LPAR 2010. LNCS (LNAI), vol. 6355, pp. 136–153. Springer, Heidelberg (2010). doi:10.1007/978-3-642-17511-4_9

    Chapter  Google Scholar 

  7. Bruscoli, P., Guglielmi, A., Gundersen, T., Parigot, M.: A quasipolynomial normalisation in deep inference via atomic flows and threshold formulae. Log. Methods Comput. Sci. 12(1:5), 1–30 (2016)

    MathSciNet  MATH  Google Scholar 

  8. Das, A.: Complexity of deep inference via atomic flows. In: Cooper, S.B., Dawar, A., Löwe, B. (eds.) CiE 2012. LNCS, vol. 7318, pp. 139–150. Springer, Heidelberg (2012). doi:10.1007/978-3-642-30870-3_15

    Chapter  Google Scholar 

  9. Das, A.: Rewriting with linear inferences in propositional logic. In: van Raamsdonk, F. (ed) 24th International Conference on Rewriting Techniques and Applications (RTA). Leibniz International Proceedings in Informatics (LIPIcs), vol. 21, pp. 158–173. Schloss Dagstuhl-Leibniz-Zentrum für Informatik (2013)

    Google Scholar 

  10. Das, A., Straßburger, L.: No complete linear term rewriting system for propositional logic. In: Fernandez, M. (ed) 26th International Conference on Rewriting Techniques and Applications, RTA 2015. LIPIcs, Warsaw, Poland, 29 June to 1 July 2015, vol. 36, pp. 127–142 (2015)

    Google Scholar 

  11. Das, A., Straßburger, L.: On linear rewriting systems for boolean logic and some applications to proof theory. Log. Methods Comput. Sci. 12(4) (2016)

    Google Scholar 

  12. Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Logic 8(1), 1–64 (2007)

    Article  MathSciNet  Google Scholar 

  13. Guglielmi, A., Gundersen, T.: Normalisation control in deep inference via atomic flows. Log. Methods Comput. Sci. 4(1:9), 1–36 (2008)

    MathSciNet  MATH  Google Scholar 

  14. Guglielmi, A., Gundersen, T., Straßburger, L.: Breaking paths in atomic flows for classical logic. In: LICS 2010 (2010)

    Google Scholar 

  15. Guglielmi, A., Straßburger, L.: Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 54–68. Springer, Heidelberg (2001). doi:10.1007/3-540-44802-0_5

    Chapter  Google Scholar 

  16. Gundersen, T., Heijltjes, W., Parigot, M.: Atomic lambda calculus: a typed lambda-calculus with explicit sharing. In: 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, USA, 25–28 June 2013, pp. 311–320. IEEE Computer Society (2013)

    Google Scholar 

  17. Kahramanogullari, O.: Interaction and depth against nondeterminism in proof search. Log. Methods Comput. Sci. 10(2) (2014)

    Google Scholar 

  18. Lamarche, F.: Exploring the gap between linear and classical logic. Theory Appl. Categ. 18(18), 473–535 (2007)

    MathSciNet  MATH  Google Scholar 

  19. Straßburger, L.: A local system for linear logic. In: Baaz, M., Voronkov, A. (eds.) LPAR 2002. LNCS (LNAI), vol. 2514, pp. 388–402. Springer, Heidelberg (2002). doi:10.1007/3-540-36078-6_26

    Chapter  Google Scholar 

  20. Straßburger, L.: A characterization of medial as rewriting rule. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 344–358. Springer, Heidelberg (2007). doi:10.1007/978-3-540-73449-9_26

    Chapter  Google Scholar 

  21. Straßburger, L.: On the axiomatisation of Boolean categories with and without medial. Theory Appl. Categ. 18(18), 536–601 (2007)

    MathSciNet  MATH  Google Scholar 

  22. Aler Tubella, A.: A study of normalisation through subatomic logic. PhD thesis, University of Bath (2016)

    Google Scholar 

Download references

Acknowledgements

We are grateful to Alessio Guglielmi and Tom Gundersen, for their encouragements and checks, and to the anonymous referees. Paola Bruscoli was funded by EPSRC Project EP/K018868/1 “Efficient and Natural Proof Systems”. This research is also supported by ANR Project FISP – “The Fine Structure of Formal Proof Systems and their Computational Interpretations.”

Author information

Authors and Affiliations

  1. University of Bath, Bath, UK

    Paola Bruscoli

  2. Inria, Palaiseau, France

    Lutz Straßburger

Authors
  1. Paola Bruscoli
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lutz Straßburger
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Paola Bruscoli .

Editor information

Editors and Affiliations

  1. Department of Mathematics and Statistics, University of Helsinki, Helsinki, Finland

    Juliette Kennedy

  2. Centro de Informática, Recife, Pernambuco, Brazil

    Ruy J.G.B. de Queiroz

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer-Verlag GmbH Germany

About this paper

Cite this paper

Bruscoli, P., Straßburger, L. (2017). On the Length of Medial-Switch-Mix Derivations. In: Kennedy, J., de Queiroz, R. (eds) Logic, Language, Information, and Computation. WoLLIC 2017. Lecture Notes in Computer Science(), vol 10388. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-55386-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-55386-2_5

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-55385-5

  • Online ISBN: 978-3-662-55386-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation