{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T08:10:37Z","timestamp":1726042237437},"publisher-location":"Cham","reference-count":33,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030290252"},{"type":"electronic","value":"9783030290269"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-29026-9_13","type":"book-chapter","created":{"date-parts":[[2019,8,21]],"date-time":"2019-08-21T23:10:06Z","timestamp":1566429006000},"page":"223-240","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["On Combinatorial Proofs for Modal Logic"],"prefix":"10.1007","author":[{"given":"Matteo","family":"Acclavio","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Lutz","family":"Stra\u00dfburger","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2019,8,14]]},"reference":[{"key":"13_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"481","DOI":"10.1007\/978-3-319-94205-6_32","volume-title":"Automated Reasoning","author":"M Acclavio","year":"2018","unstructured":"Acclavio, M., Stra\u00dfburger, L.: From syntactic proofs to combinatorial proofs. In: Galmiche, D., Schulz, S., Sebastiani, R. (eds.) IJCAR 2018. LNCS (LNAI), vol. 10900, pp. 481\u2013497. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-94205-6_32"},{"key":"13_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/978-3-662-59533-6_1","volume-title":"Logic, Language, Information, and Computation","author":"M Acclavio","year":"2019","unstructured":"Acclavio, M., Stra\u00dfburger, L.: On combinatorial proofs for logics of relevance and entailment. In: Iemhoff, R., Moortgat, M., de Queiroz, R. (eds.) WoLLIC 2019. LNCS, vol. 11541, pp. 1\u201316. Springer, Heidelberg (2019). https:\/\/doi.org\/10.1007\/978-3-662-59533-6_1"},{"key":"13_CR3","doi-asserted-by":"crossref","unstructured":"Avron, A.: The method of hypersequents in the proof theory of propositional non-classical logics. In: Logic: From Foundations to Applications, European Logic Colloquium, pp. 1\u201332. Oxford University Press (1994)","DOI":"10.1093\/oso\/9780198538622.003.0001"},{"key":"13_CR4","doi-asserted-by":"crossref","unstructured":"Benjamin, R., Stra\u00dfburger, L.: Towards a combinatorial proof theory. In: Cerrito, S., Popescu, A., (eds.) TABLEAUX 2019. LNAI, vol. 11714, pp. 259\u2013276 (2019)","DOI":"10.1007\/978-3-030-29026-9_15"},{"issue":"6","key":"13_CR5","doi-asserted-by":"publisher","first-page":"551","DOI":"10.1007\/s00153-009-0137-3","volume":"48","author":"K Br\u00fcnnler","year":"2009","unstructured":"Br\u00fcnnler, K.: Deep sequent systems for modal logic. Arch. Math. Log. 48(6), 551\u2013577 (2009)","journal-title":"Arch. Math. Log."},{"key":"13_CR6","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1007\/3-540-45653-8_24","volume-title":"Logic for Programming, Artificial Intelligence, and Reasoning","author":"K Br\u00fcnnler","year":"2001","unstructured":"Br\u00fcnnler, K., Tiu, A.F.: A local system for classical logic. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 347\u2013361. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-45653-8_24"},{"key":"13_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"390","DOI":"10.1007\/978-3-662-49630-5_23","volume-title":"Foundations of Software Science and Computation Structures","author":"K Chaudhuri","year":"2016","unstructured":"Chaudhuri, K., Marin, S., Stra\u00dfburger, L.: Focused and synthetic nested sequents. In: Jacobs, B., L\u00f6ding, C. (eds.) FoSSaCS 2016. LNCS, vol. 9634, pp. 390\u2013407. Springer, Heidelberg (2016). https:\/\/doi.org\/10.1007\/978-3-662-49630-5_23"},{"key":"13_CR8","unstructured":"Chaudhuri, K., Marin, S., Stra\u00dfburger, L.: Modular focused proof systems for intuitionistic modal logics. In: Kesner, D., Pientka, B. (eds.) FSCD 2016. LIPIcs, vol. 52, pp. 16:1\u201316:18. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik (2016)"},{"issue":"1","key":"13_CR9","doi-asserted-by":"publisher","first-page":"36","DOI":"10.2307\/2273702","volume":"44","author":"SA Cook","year":"1979","unstructured":"Cook, S.A., Reckhow, R.A.: The relative efficiency of propositional proof systems. J. Symb. Logic 44(1), 36\u201350 (1979)","journal-title":"J. Symb. Logic"},{"issue":"2","key":"13_CR10","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-7(2:8)2011","volume":"7","author":"R Gor\u00e9","year":"2011","unstructured":"Gor\u00e9, R., Postniece, L., Tiu, A.: On the correspondence between display postulates and deep inference in nested sequent calculi for tense logics. Log. Methods Comput. Sci. 7(2), 1\u201338 (2011)","journal-title":"Log. Methods Comput. Sci."},{"key":"13_CR11","first-page":"279","volume":"9","author":"R Gor\u00e9","year":"2012","unstructured":"Gor\u00e9, R., Ramanayake, R., et al.: Labelled tree sequents, tree hypersequents and nested (deep) sequents. Adv. Modal Log. 9, 279\u2013299 (2012)","journal-title":"Adv. Modal Log."},{"issue":"1","key":"13_CR12","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/1182613.1182614","volume":"8","author":"A Guglielmi","year":"2007","unstructured":"Guglielmi, A.: A system of interaction and structure. ACM Trans. Comput. Log. 8(1), 1\u201364 (2007)","journal-title":"ACM Trans. Comput. Log."},{"key":"13_CR13","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"54","DOI":"10.1007\/3-540-44802-0_5","volume-title":"Computer Science Logic","author":"A Guglielmi","year":"2001","unstructured":"Guglielmi, A., Stra\u00dfburger, L.: Non-commutativity and MELL in the calculus of structures. In: Fribourg, L. (ed.) CSL 2001. LNCS, vol. 2142, pp. 54\u201368. Springer, Heidelberg (2001). https:\/\/doi.org\/10.1007\/3-540-44802-0_5"},{"key":"13_CR14","unstructured":"Hein, R., Stewart, C.: Purity through unravelling. In: Structures and Deduction, pp. 126\u2013143 (2005)"},{"issue":"3","key":"13_CR15","doi-asserted-by":"publisher","first-page":"1065","DOI":"10.4007\/annals.2006.164.1065","volume":"164","author":"D Hughes","year":"2006","unstructured":"Hughes, D.: Proofs without syntax. Ann. Math. 164(3), 1065\u20131076 (2006)","journal-title":"Ann. Math."},{"key":"13_CR16","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1016\/j.entcs.2006.05.036","volume":"165","author":"D Hughes","year":"2006","unstructured":"Hughes, D.: Towards Hilbert\u2019s 24 $${}^{\\text{ th }}$$ problem: combinatorial proof invariants: (preliminary version). Electr. Notes Theor. Comput. Sci. 165, 37\u201363 (2006)","journal-title":"Electr. Notes Theor. Comput. Sci."},{"key":"13_CR17","unstructured":"Hughes, D.J.D.: First-order proofs without syntax, June 2019"},{"key":"13_CR18","doi-asserted-by":"publisher","first-page":"76","DOI":"10.1016\/j.tcs.2016.10.004","volume":"656","author":"B Lellmann","year":"2016","unstructured":"Lellmann, B.: Hypersequent rules with restricted contexts for propositional modal logics. Theor. Comput. Sci. 656, 76\u2013105 (2016)","journal-title":"Theor. Comput. Sci."},{"issue":"2","key":"13_CR19","first-page":"7","volume":"20","author":"B Lellmann","year":"2019","unstructured":"Lellmann, B., Pimentel, E.: Modularisation of sequent calculi for normal and non-normal modalities. ACM Trans. Comput. Log. (TOCL) 20(2), 7 (2019)","journal-title":"ACM Trans. Comput. Log. (TOCL)"},{"key":"13_CR20","unstructured":"Marin, S., Stra\u00dfburger, L.: Label-free modular systems for classical and intuitionistic modal logics. In: Advances in Modal Logic 10 (2014)"},{"key":"13_CR21","doi-asserted-by":"publisher","first-page":"105","DOI":"10.1007\/978-94-009-2639-4_4","volume-title":"Algorithms and Order","author":"RH M\u00f6hring","year":"1989","unstructured":"M\u00f6hring, R.H.: Computationally tractable classes of ordered sets. In: Rival, I. (ed.) Algorithms and Order, pp. 105\u2013194. Kluwer, Dordrecht (1989)"},{"issue":"5\u20136","key":"13_CR22","doi-asserted-by":"publisher","first-page":"507","DOI":"10.1007\/s10992-005-2267-3","volume":"34","author":"S Negri","year":"2005","unstructured":"Negri, S.: Proof analysis in modal logic. J. Philos. Log. 34(5\u20136), 507 (2005)","journal-title":"J. Philos. Log."},{"key":"13_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"300","DOI":"10.1007\/3-540-62688-3_43","volume-title":"Typed Lambda Calculi and Applications","author":"C Retor\u00e9","year":"1997","unstructured":"Retor\u00e9, C.: Pomset logic: a non-commutative extension of classical linear logic. In: de Groote, P., Roger Hindley, J. (eds.) TLCA 1997. LNCS, vol. 1210, pp. 300\u2013318. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/3-540-62688-3_43"},{"issue":"3","key":"13_CR24","doi-asserted-by":"publisher","first-page":"473","DOI":"10.1016\/S0304-3975(01)00175-X","volume":"294","author":"C Retor\u00e9","year":"2003","unstructured":"Retor\u00e9, C.: Handsome proof-nets: perfect matchings and cographs. Theor. Comput. Sci. 294(3), 473\u2013488 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"13_CR25","unstructured":"Simpson, A.K.: The proof theory and semantics of intuitionistic modal logic. Ph.D. thesis, University of Edinburgh. College of Science and Engineering (1994)"},{"key":"13_CR26","first-page":"309","volume":"5","author":"C Stewart","year":"2004","unstructured":"Stewart, C., Stouppa, P.: A systematic proof theory for several modal logics. Adv. Modal Log. 5, 309\u2013333 (2004)","journal-title":"Adv. Modal Log."},{"key":"13_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"344","DOI":"10.1007\/978-3-540-73449-9_26","volume-title":"Term Rewriting and Applications","author":"L Stra\u00dfburger","year":"2007","unstructured":"Stra\u00dfburger, L.: A characterization of medial as rewriting rule. In: Baader, F. (ed.) RTA 2007. LNCS, vol. 4533, pp. 344\u2013358. Springer, Heidelberg (2007). https:\/\/doi.org\/10.1007\/978-3-540-73449-9_26"},{"key":"13_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"209","DOI":"10.1007\/978-3-642-37075-5_14","volume-title":"Foundations of Software Science and Computation Structures","author":"L Stra\u00dfburger","year":"2013","unstructured":"Stra\u00dfburger, L.: Cut elimination in nested sequents for intuitionistic modal logics. In: Pfenning, F. (ed.) FoSSaCS 2013. LNCS, vol. 7794, pp. 209\u2013224. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-37075-5_14"},{"key":"13_CR29","unstructured":"Stra\u00dfburger, L.: Combinatorial flows and their normalisation. In: Miller, D. (ed.) FSCD 2017. LIPIcs, vol. 84, pp. 31:1\u201331:17. Schloss Dagstuhl (2017)"},{"issue":"2140","key":"13_CR30","doi-asserted-by":"publisher","first-page":"20180038","DOI":"10.1098\/rsta.2018.0038","volume":"377","author":"L Stra\u00dfburger","year":"2019","unstructured":"Stra\u00dfburger, L.: The problem of proof identity, and why computer scientists should care about Hilbert\u2019s 24th problem. Philos. Trans. R. Soc. A 377(2140), 20180038 (2019)","journal-title":"Philos. Trans. R. Soc. A"},{"key":"13_CR31","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1080\/00029890.2003.11919933","volume":"110","author":"R Thiele","year":"2003","unstructured":"Thiele, R.: Hilbert\u2019s twenty-fourth problem. Am. Math. Mon. 110, 1\u201324 (2003)","journal-title":"Am. Math. Mon."},{"issue":"2","key":"13_CR32","doi-asserted-by":"publisher","first-page":"125","DOI":"10.1093\/logcom\/4.2.125","volume":"4","author":"H Wansing","year":"1994","unstructured":"Wansing, H.: Sequent calculi for normal modal propositional logics. J. Log. Comput. 4(2), 125\u2013142 (1994)","journal-title":"J. Log. Comput."},{"key":"13_CR33","series-title":"Handbook of Philosophical Logic","doi-asserted-by":"publisher","first-page":"61","DOI":"10.1007\/978-94-010-0387-2_2","volume-title":"Handbook of Philosophical Logic","author":"H Wansing","year":"2002","unstructured":"Wansing, H.: Sequent systems for modal logics. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic. Handbook of Philosophical Logic, vol. 8, pp. 61\u2013145. Springer, Dordrecht (2002)"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning with Analytic Tableaux and Related Methods"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-29026-9_13","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,22]],"date-time":"2024-07-22T10:55:37Z","timestamp":1721645737000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-29026-9_13"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030290252","9783030290269"],"references-count":33,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-29026-9_13","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"14 August 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"TABLEAUX","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Automated Reasoning with Analytic Tableaux and Related Methods","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3 September 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"5 September 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"tableaux2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/tableaux2019.org\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"43","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"25","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"58% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3.2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}