{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,12,31]],"date-time":"2025-12-31T01:01:26Z","timestamp":1767142886207,"version":"build-2238731810"},"reference-count":46,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2022,4,7]],"date-time":"2022-04-07T00:00:00Z","timestamp":1649289600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2022,4,7]],"date-time":"2022-04-07T00:00:00Z","timestamp":1649289600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2022,8]]},"abstract":"<jats:title>Abstract<\/jats:title>\n                  <jats:p>Classical propositional logic plays a prominent role in industrial applications, and yet the complexity of this logic is presumed to be non-feasible. Tractable systems such as depth-bounded boolean logics approximate classical logic and can be seen as a model for resource-bounded agents whose reasoning style is nonetheless classical. In this paper we first study a hierarchy of tractable logics that is not defined by depth. Then we extend it into a modal logic where modalities make explicit the assumptions discharged in propositional proofs, thereby expressing blueprints for proofs. A natural deduction system is provided that permits to reason about and manage such proof blueprints.<\/jats:p>","DOI":"10.1007\/s11225-022-09984-3","type":"journal-article","created":{"date-parts":[[2022,4,7]],"date-time":"2022-04-07T07:08:58Z","timestamp":1649315338000},"page":"1035-1080","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Modal View on Resource-Bounded Propositional Logics"],"prefix":"10.1007","volume":"110","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-0181-4658","authenticated-orcid":false,"given":"Pere","family":"Pardo","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2022,4,7]]},"reference":[{"key":"9984_CR1","doi-asserted-by":"crossref","unstructured":"\u00c5gotnes, T., and M. Walicki, A logic of reasoning, communication and cooperation with syntactic knowledge, in 4th International Conference on Autonomous Agents and Multiagent Systems (AAMAS 2005), Association for Computing Machinery, New York, 2005, pp. 1135\u20131136.","DOI":"10.1145\/1082473.1082660"},{"key":"9984_CR2","unstructured":"Alechina, N., B. Logan, and M. Whitsey, A complete and decidable logic for resourcebounded agents, in Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems: Volume 2 (AAMAS 2004), IEEE Computer Society, New York, 2004, pp. 606\u2013613."},{"issue":"6","key":"9984_CR3","doi-asserted-by":"publisher","first-page":"1059","DOI":"10.1093\/logcom\/exi053","volume":"15","author":"SN Artemov","year":"2005","unstructured":"Artemov, S.N., and E. Nogina, Introducing justification into epistemic logic, Journal of Logic and Computation 15(6):1059\u20131073, 2005.","journal-title":"Journal of Logic and Computation"},{"issue":"1","key":"9984_CR4","doi-asserted-by":"publisher","first-page":"245","DOI":"10.1007\/BF00245930","volume":"7","author":"K Bendall","year":"1978","unstructured":"Bendall, K., Natural deduction, separation and the meaning of logical operators, Journal of Philosophical Logic 7(1):245\u2013276, 1978.","journal-title":"Journal of Philosophical Logic"},{"issue":"3","key":"9984_CR5","doi-asserted-by":"publisher","first-page":"501","DOI":"10.1007\/s10992-018-9473-2","volume":"48","author":"JCh Bjerring","year":"2019","unstructured":"Bjerring, J.Ch., and M. Skipper, A dynamic solution to the problem of logical omniscience, Journal of Philosophical Logic 48(3):501\u2013521, 2019.","journal-title":"Journal of Philosophical Logic"},{"issue":"4","key":"9984_CR6","doi-asserted-by":"publisher","first-page":"916","DOI":"10.2307\/2273826","volume":"52","author":"SR Buss","year":"1987","unstructured":"Buss, S. R., Polynomial size proofs of the propositional pigeonhole principle, Journal of Symbolic Logic 52(4):916\u2013927, 1987.","journal-title":"Journal of Symbolic Logic"},{"key":"9984_CR7","doi-asserted-by":"crossref","unstructured":"Cignarale, G., and G. Primiero, A multi-agent depth bounded boolean logic, in L. Cleophas, and M. Massink, (eds.), Software Engineering and Formal Methods. SEFM 2020 Collocated Workshops, Springer, 2021, pp 176\u2013191.","DOI":"10.1007\/978-3-030-67220-1_14"},{"key":"9984_CR8","doi-asserted-by":"crossref","unstructured":"Cook, S.A., The complexity of theorem-proving procedures, in M.A. Harrison, N.B. Banerji, and J.D. Ullman, (eds.), Proceedings of the 3rd Annual ACM Symposium on Theory of Computing, Association for Computing Machinery, New York, 1971, pp. 151\u2013158.","DOI":"10.1145\/800157.805047"},{"issue":"1","key":"9984_CR9","doi-asserted-by":"publisher","first-page":"33","DOI":"10.3390\/info4010033","volume":"4","author":"M D\u2019Agostino","year":"2013","unstructured":"D\u2019Agostino, M., Semantic information and the trivialization of logic: Floridi on the scandal of deduction, Information 4(1):33\u201359, 2013.","journal-title":"Information"},{"key":"9984_CR10","doi-asserted-by":"publisher","first-page":"79","DOI":"10.1016\/j.tcs.2015.06.057","volume":"606","author":"M D\u2019Agostino","year":"2015","unstructured":"D\u2019Agostino, M., An informational view of classical logic, Theoretical Computer Science 606: 79\u201397, 2015.","journal-title":"Theoretical Computer Science"},{"key":"9984_CR11","doi-asserted-by":"publisher","first-page":"43","DOI":"10.1016\/j.tcs.2013.02.014","volume":"480","author":"M D\u2019Agostino","year":"2013","unstructured":"D\u2019Agostino, M., M. Finger, and D.M. Gabbay, Semantics and proof-theory of depth bounded boolean logics, Theoretical Computer Science 480:43\u201368, 2013.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"9984_CR12","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1007\/s11229-008-9409-4","volume":"167","author":"M D\u2019Agostino","year":"2009","unstructured":"D\u2019Agostino, M., and L. Floridi, The enduring scandal of deduction, Synthese 167(2):271\u2013315, 2009.","journal-title":"Synthese"},{"issue":"2","key":"9984_CR13","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/s11225-019-09847-4","volume":"108","author":"M D\u2019Agostino","year":"2020","unstructured":"D\u2019Agostino, M., D.M. Gabbay, and S. Modgil, Normality, non-contamination and logical depth in classical natural deduction, Studia Logica 108(2):291\u2013357, 2020.","journal-title":"Studia Logica"},{"key":"9984_CR14","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1016\/j.artint.2018.05.003","volume":"262","author":"M D\u2019Agostino","year":"2018","unstructured":"D\u2019Agostino, M., and S. Modgil, Classical logic, argument and dialectic, Artificial Intelligence 262: 15\u201351, 2018.","journal-title":"Artificial Intelligence"},{"issue":"3\u20134","key":"9984_CR15","doi-asserted-by":"publisher","first-page":"297","DOI":"10.1023\/A:1018947704302","volume":"22","author":"M Dalal","year":"1998","unstructured":"Dalal, M., Anytime clausal reasoning, Annals of Mathematics and Artificial Intelligence 22(3-4):297\u2013318, 1998.","journal-title":"Annals of Mathematics and Artificial Intelligence"},{"key":"9984_CR16","doi-asserted-by":"crossref","unstructured":"Davey, B.A., and H.A. Priestley, Introduction to Lattices and Order, 2nd edition, Cambridge University Press, 2002.","DOI":"10.1017\/CBO9780511809088"},{"key":"9984_CR17","doi-asserted-by":"publisher","first-page":"171","DOI":"10.1016\/j.entcs.2005.04.040","volume":"143","author":"G de Souza Rabello","year":"2006","unstructured":"de Souza Rabello, G., and M. Finger, Approximations of modal logic K, Electronic Notes in Theoretical Computer Science 143:171\u2013184, 2006.","journal-title":"Finger, Approximations of modal logic K, Electronic Notes in Theoretical Computer Science"},{"issue":"3","key":"9984_CR18","doi-asserted-by":"publisher","first-page":"195","DOI":"10.1007\/s10849-005-9001-y","volume":"15","author":"M Finger","year":"2006","unstructured":"Finger, M., and D.M. Gabbay, Cut and pay, Journal of Logic, Language and Information 15(3):195\u2013218, 2006.","journal-title":"Journal of Logic, Language and Information"},{"issue":"2","key":"9984_CR19","doi-asserted-by":"publisher","first-page":"153","DOI":"10.1016\/j.tcs.2006.01.007","volume":"355","author":"M Finger","year":"2006","unstructured":"Finger, M., and R. Wassermann, The universe of propositional approximations, Theoretical Computer Science 355(2):153\u2013166, 2006.","journal-title":"Theoretical Computer Science"},{"issue":"2","key":"9984_CR20","doi-asserted-by":"publisher","first-page":"194","DOI":"10.1016\/0022-0000(79)90046-1","volume":"18","author":"MJ Fischer","year":"1979","unstructured":"Fischer, M.J., and R.E. Ladner, Propositional dynamic logic of regular programs, Journal of Computer and System Sciences 18(2):194\u2013211, 1979.","journal-title":"Journal of Computer and System Sciences"},{"key":"9984_CR21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511617737","volume-title":"Modal Logic for Philosophers","author":"JW Garson","year":"2006","unstructured":"Garson, J.W., Modal Logic for Philosophers, Cambridge University Press, Cambridge, 2006."},{"key":"9984_CR22","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/j.artint.2017.08.008","volume":"253","author":"Ch Ghidini","year":"2017","unstructured":"Ghidini, Ch., and L. Serafini, Distributed first order logic, Artificial Intelligence 253:1\u201339, 2017.","journal-title":"Artificial Intelligence"},{"key":"9984_CR23","doi-asserted-by":"crossref","unstructured":"Goubault, J., The complexity of resource-bounded first-order classical logic, in P. Enjalbert, E.W. Mayr, and K.W. Wagner, (eds.), STACS 94, 11th Annual Symposium on Theoretical Aspects of Computer Science, vol. 775 of LNCS, Springer, 1994, pp. 59\u201370.","DOI":"10.1007\/3-540-57785-8_131"},{"key":"9984_CR24","doi-asserted-by":"crossref","unstructured":"Gr\u00e4tzer, G., Lattice Theory: Foundation, Birkh\u00e4user Basel, 2011.","DOI":"10.1007\/978-3-0348-0018-1"},{"key":"9984_CR25","doi-asserted-by":"crossref","unstructured":"Grossi, D., and F.R. Vel\u00e1zquez-Quesada, Twelve Angry Men: A study on the finegrain of announcements, in X. He, J. Horty, and E. Pacuit, (eds.), Proceedings of the 2nd international conference on logic, rationality and interaction, vol. 5834 of LNCS, Springer, 2009, pp. 147\u2013160.","DOI":"10.1007\/978-3-642-04893-7_12"},{"key":"9984_CR26","doi-asserted-by":"crossref","unstructured":"Hakli, R., and S. Negri, Proof theory for distributed knowledge, in F. Sadri, and K. Satoh, (eds.), Computational Logic in Multi-Agent Systems, CLIMA VIII, vol. 5056 of LNCS, Springer, 2007, pp. 100\u2013116.","DOI":"10.1007\/978-3-540-88833-8_6"},{"issue":"3","key":"9984_CR27","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/s10009-004-0152-y","volume":"7","author":"J Hammarberg","year":"2005","unstructured":"Hammarberg, J., and S. Nadjm-Tehrani, Formal verification of fault tolerance in safetycritical reconfigurable modules, International Journal on Software Tools for Technology Transfer volume 7(3):268\u2013279, 2005.","journal-title":"International Journal on Software Tools for Technology Transfer"},{"issue":"4","key":"9984_CR28","doi-asserted-by":"publisher","first-page":"727","DOI":"10.1007\/s10992-019-09536-6","volume":"49","author":"P Hawke","year":"2020","unstructured":"Hawke, P., A. \u00d6zg\u00fcn, and F. Berto, The fundamental problem of logical omniscience, Journal of Philosophical Logic 49(4):727\u2013766, 2020.","journal-title":"Journal of Philosophical Logic"},{"key":"9984_CR29","volume-title":"Natural Deduction","author":"A Indrzejczak","year":"2010","unstructured":"Indrzejczak, A., Natural Deduction, Hybrid Systems and Modal Logics, Springer, 2010."},{"key":"9984_CR30","doi-asserted-by":"publisher","first-page":"131","DOI":"10.1007\/s10849-008-9071-8","volume":"18","author":"M Jago","year":"2009","unstructured":"Jago, M., Epistemic logic for rule-based agents, Journal of Logic, Language and Information 18:131\u2013158, 2009.","journal-title":"Journal of Logic, Language and Information"},{"key":"9984_CR31","volume-title":"Towards tractable inference for resource-bounded agents, in 2015 AAAI Spring Symposia","author":"TQ Klassen","year":"2015","unstructured":"Klassen, T.Q., S.A. McIlraith, and H.J. Levesque, Towards tractable inference for resource-bounded agents, in 2015 AAAI Spring Symposia, Stanford University, Palo Alto, CA, USA, AAAI Press, 2015."},{"key":"9984_CR32","volume-title":"Introduction to Metamathematics","author":"SC Kleene","year":"1952","unstructured":"Kleene, S.C., Introduction to Metamathematics, North-Holland, Amsterdam, 1952."},{"key":"9984_CR33","unstructured":"Larese, C., The Principle of Analyticity of Logic A Philosophical and Formal Perspective, M.S. thesis, Scuola Normale Superiore, Pisa, Italy, 2019."},{"key":"9984_CR34","doi-asserted-by":"crossref","unstructured":"Marques-Silva, J., and S. Malik, Propositional SAT solving, in E.M. Clarke, T.A. Henzinger, H. Veith, and R. Bloem, (eds.), Handbook of Model Checking, Springer, 2018, pp. 247\u2013275.","DOI":"10.1007\/978-3-319-10575-8_9"},{"key":"9984_CR35","doi-asserted-by":"crossref","unstructured":"Marx, M., Complexity of modal logic, in P. Blackburn, J. van Benthem, and F. Wolter, (eds.), Handbook of Modal Logic, vol. 3 of Studies in logic and practical reasoning, North-Holland, 2007, pp. 139\u2013179.","DOI":"10.1016\/S1570-2464(07)80006-1"},{"issue":"1","key":"9984_CR36","first-page":"167","volume":"107","author":"GK Olkhovikov","year":"2019","unstructured":"Olkhovikov, G.K., and H. Wansing, Inference as doxastic agency. Part I: The basics of justification stit logic, Studia Logica 107(1):167\u2013194, 2019.","journal-title":"Part I: The basics of justification stit logic, Studia Logica"},{"key":"9984_CR37","volume-title":"Natural Deduction","author":"D Prawitz","year":"1965","unstructured":"Prawitz, D., Natural Deduction. A Proof-Theoretical Study, Almqvist & Wilksell, Uppsala, 1965."},{"key":"9984_CR38","unstructured":"Quine, W.V.O., The Roots of Reference, Open Court, 1973."},{"issue":"2","key":"9984_CR39","doi-asserted-by":"publisher","first-page":"249","DOI":"10.1016\/0004-3702(94)00009-P","volume":"74","author":"M Schaerf","year":"1995","unstructured":"Schaerf, M., and M. Cadoli, Tractable reasoning via approximation, Artificial Intelligence 74(2):249\u2013310, 1995.","journal-title":"Artificial Intelligence"},{"issue":"1","key":"9984_CR40","doi-asserted-by":"publisher","first-page":"23","DOI":"10.1023\/A:1008725524946","volume":"16","author":"M Sheeran","year":"2000","unstructured":"Sheeran, M., and G. St\u00e5lmarck, A tutorial on St\u00e5lmarck\u2019s proof procedure for propositional logic, Formal Methods in System Design 16(1):23\u201358, 2000.","journal-title":"Formal Methods in System Design"},{"key":"9984_CR41","unstructured":"Sipser, M., Introduction to the theory of computation, PWS Publishing Company, 1997."},{"key":"9984_CR42","doi-asserted-by":"crossref","unstructured":"Solaki, A., Rule-based reasoners in epistemic logic, in J. Sikos, and E. Pacuit, (eds.), At the Intersection of Language, Logic, and Information - ESSLLI 2018 Student Session, vol. 11667 of LNCS, Springer, 2018, pp. 144\u2013156.","DOI":"10.1007\/978-3-662-59620-3_9"},{"issue":"2","key":"9984_CR43","first-page":"169","volume":"23","author":"H van Ditmarsch","year":"2014","unstructured":"van Ditmarsch, H., and T. French, Semantics for knowledge and change of awareness, Journal of Logic, Language, and Information 23(2):169\u2013195, 2014.","journal-title":"Journal of Logic, Language, and Information"},{"key":"9984_CR44","doi-asserted-by":"crossref","unstructured":"van Ditmarsch, H., W. van der Hoek, and B. Kooi, Dynamic Epistemic Logic, vol. 337 of Synthese Library, Springer, 2008.","DOI":"10.1007\/978-1-4020-5839-4"},{"key":"9984_CR45","doi-asserted-by":"crossref","unstructured":"Vel\u00e1zquez-Quesada, F., Dynamic epistemic logic for implicit and explicit beliefs, Journal of Logic, Language and Information 23(2):107\u2013140, 2014.","DOI":"10.1007\/s10849-014-9193-0"},{"key":"9984_CR46","volume-title":"Logical omniscience: A survey, Technical Report NOTTCS-WP-2003-2","author":"M Whitsey","year":"2003","unstructured":"Whitsey, M., Logical omniscience: A survey, Technical Report NOTTCS-WP-2003-2, School of Computer Science and IT, University of Nottingham, 2003."}],"updated-by":[{"DOI":"10.1007\/s11225-022-10006-5","type":"correction","label":"Correction","source":"publisher","updated":{"date-parts":[[2022,5,25]],"date-time":"2022-05-25T00:00:00Z","timestamp":1653436800000}}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-09984-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-022-09984-3\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-022-09984-3.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,30]],"date-time":"2022-07-30T03:17:15Z","timestamp":1659151035000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-022-09984-3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,7]]},"references-count":46,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2022,8]]}},"alternative-id":["9984"],"URL":"https:\/\/doi.org\/10.1007\/s11225-022-09984-3","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"value":"0039-3215","type":"print"},{"value":"1572-8730","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,7]]},"assertion":[{"value":"30 November 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"7 April 2022","order":2,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"31 July 2022","order":3,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Update","order":4,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Missing Open Access funding information has been added in the Funding Note","order":5,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"25 May 2022","order":6,"name":"change_date","label":"Change Date","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"Correction","order":7,"name":"change_type","label":"Change Type","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"A Correction to this paper has been published:","order":8,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"https:\/\/doi.org\/10.1007\/s11225-022-10006-5","URL":"https:\/\/doi.org\/10.1007\/s11225-022-10006-5","order":9,"name":"change_details","label":"Change Details","group":{"name":"ArticleHistory","label":"Article History"}}]}}