{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:52:04Z","timestamp":1750308724272,"version":"3.41.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/F042728\/1"],"award-info":[{"award-number":["EP\/F042728\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:p>We develop a cut-free nested sequent calculus as basis for a proof search procedure for an intuitionistic modal logic of actions and propositions. The actions act on propositions via a dynamic modality (the<jats:italic>weakest precondition<\/jats:italic>of program logics), whose left adjoint we refer to as \u201cupdate\u201d (the<jats:italic>strongest postcondition<\/jats:italic>). The logic has agent-indexed adjoint pairs of epistemic modalities: the left adjoints encode agents' uncertainties and the right adjoints encode their beliefs. The rules for the \u201cupdate\u201d modality encode learning as a result of discarding uncertainty. We prove admissibility of<jats:italic>Cut<\/jats:italic>, and hence the soundness and completeness of the logic with respect to an algebraic semantics. We interpret the logic on epistemic scenarios that consist of honest and dishonest communication actions, add assumption rules to encode them, and prove that the calculus with the assumption rules still has the admissibility results. We apply the calculus to encode (and allow reasoning about) the classic epistemic puzzles of<jats:italic>dirty children<\/jats:italic>(a.k.a. \u201cmuddy children\u201d) and<jats:italic>drinking logicians<\/jats:italic>and some versions with dishonesty or noise; we also give an application where the actions are movements of a robot rather than announcements.<\/jats:p>","DOI":"10.1145\/2536740.2536742","type":"journal-article","created":{"date-parts":[[2013,12,4]],"date-time":"2013-12-04T14:04:47Z","timestamp":1386165887000},"page":"1-37","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Algebra, proof theory and applications for an intuitionistic logic of propositions, actions and adjoint modal operators"],"prefix":"10.1145","volume":"14","author":[{"given":"Roy","family":"Dyckhoff","sequence":"first","affiliation":[{"name":"University of St Andrews, Scotland, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mehrnoosh","family":"Sadrzadeh","sequence":"additional","affiliation":[{"name":"University of Oxford, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Julien","family":"Truffaut","sequence":"additional","affiliation":[{"name":"University of Oxford, London, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,11,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000189"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exn060"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exm015"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1023\/B:SYNT.0000024912.56773.5e"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-009-0137-3"},{"key":"e_1_2_1_6_1","unstructured":"Brunnler K. and Guglielmi A. 2004. A first order system with finite choice of premises. In First-Order Logic Revisited Logos Verlag London 59--74. Brunnler K. and Guglielmi A. 2004. A first order system with finite choice of premises. In First-Order Logic Revisited Logos Verlag London 59--74."},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Cirstea C. and Sadrzadeh M . 2007 . Coalgebraic epistemic update without change of model. In Proceedings of the 2nd International Conference on Algebra and Coalgebra in Computer Science (CALCO'07). T. Mossakowski U. Montanari and M. Haveraaen Eds. Lecture Notes in Computer Science Series vol. 4624 Springer 158--172. Cirstea C. and Sadrzadeh M. 2007. Coalgebraic epistemic update without change of model. In Proceedings of the 2 nd International Conference on Algebra and Coalgebra in Computer Science (CALCO'07). T. Mossakowski U. Montanari and M. Haveraaen Eds. Lecture Notes in Computer Science Series vol. 4624 Springer 158--172.","DOI":"10.1007\/978-3-540-73859-6_11"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2012.08.011"},{"key":"e_1_2_1_9_1","doi-asserted-by":"crossref","unstructured":"Fagin R. Halpern J. Y. Moses Y. and Vardi M. Y. 1995. Reasoning About Knowledge. MIT Press. Fagin R. Halpern J. Y. Moses Y. and Vardi M. Y. 1995. Reasoning About Knowledge. MIT Press.","DOI":"10.7551\/mitpress\/5803.001.0001"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2011.09.004"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1090\/S0002-9947-2012-05573-5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:8)2011"},{"key":"e_1_2_1_13_1","unstructured":"Huth M. and Ryan M. 2000. Logic in Computer Science. Cambridge University Press. Huth M. and Ryan M. 2000. Logic in Computer Science. Cambridge University Press."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01053026"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/3.2-3.371"},{"key":"e_1_2_1_16_1","first-page":"49","article-title":"A proof theoretical perspective on public announcement logic","volume":"9","author":"Negri S.","year":"2011","unstructured":"Negri , S. and Maffezioli , P. 2011 . A proof theoretical perspective on public announcement logic . Logic Philos. Sci. 9 , 49 -- 59 . Negri, S. and Maffezioli, P. 2011. A proof theoretical perspective on public announcement logic. Logic Philos. Sci. 9, 49--59.","journal-title":"Logic Philos. Sci."},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.2307\/420956"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11229-007-9168-7"},{"volume-title":"Gentzen Calculi for Modal Propositional Logic","author":"Poggiolesi F.","key":"e_1_2_1_19_1","unstructured":"Poggiolesi , F. 2010. Gentzen Calculi for Modal Propositional Logic . Springer . Poggiolesi, F. 2010. Gentzen Calculi for Modal Propositional Logic. Springer."},{"volume-title":"An Introduction to Substructural Logics","author":"Restall G.","key":"e_1_2_1_20_1","unstructured":"Restall , G. 2000. An Introduction to Substructural Logics . Routledge , London . Restall, G. 2000. An Introduction to Substructural Logics. Routledge, London."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1755020310000134"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37075-5_14"},{"volume-title":"Implementation and Improvements of a Cut-Free Sequent Calculus for Dynamic Epistemic Logic. Department of Computer Science","author":"Truffaut J.","key":"e_1_2_1_24_1","unstructured":"Truffaut , J. 2011. Implementation and Improvements of a Cut-Free Sequent Calculus for Dynamic Epistemic Logic. Department of Computer Science , University of Oxford , Oxford. Truffaut, J. 2011. Implementation and Improvements of a Cut-Free Sequent Calculus for Dynamic Epistemic Logic. Department of Computer Science, University of Oxford, Oxford."},{"key":"e_1_2_1_25_1","volume-title":"W.","author":"Van Ditmarsch H.","year":"2007","unstructured":"Van Ditmarsch , H. , Van Der Hoek , W. , and Kooi, B. 2007 . Dynamic Epistemic Logic. Springer . Van Ditmarsch, H., Van Der Hoek, W., and Kooi, B. 2007. Dynamic Epistemic Logic. Springer."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2536740.2536742","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2536740.2536742","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T20:14:42Z","timestamp":1750277682000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2536740.2536742"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":24,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1145\/2536740.2536742"],"URL":"https:\/\/doi.org\/10.1145\/2536740.2536742","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2013,11]]},"assertion":[{"value":"2012-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}