{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T05:54:25Z","timestamp":1743141265247,"version":"3.40.3"},"publisher-location":"Cham","reference-count":26,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030658397"},{"type":"electronic","value":"9783030658403"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"vor","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":[[2020]]},"DOI":"10.1007\/978-3-030-65840-3_14","type":"book-chapter","created":{"date-parts":[[2020,12,21]],"date-time":"2020-12-21T09:04:02Z","timestamp":1608541442000},"page":"222-238","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Public Announcement Logic in HOL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2555-999X","authenticated-orcid":false,"given":"Sebastian","family":"Reiche","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3392-3093","authenticated-orcid":false,"given":"Christoph","family":"Benzm\u00fcller","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,12,22]]},"reference":[{"unstructured":"Baldoni, M.: Normal multimodal logics: automatic deduction and logic programming extension. Ph.D. thesis, Universit\u00e0 degli Studi di Torino, Dipartimento di Informatica (1998)","key":"14_CR1"},{"unstructured":"Baltag, A., Renne, B.: Dynamic epistemic logic. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy. Metaphysics Research Lab, Stanford University, winter 2016 edition (2016)","key":"14_CR2"},{"issue":"3","key":"14_CR3","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/s10992-016-9403-0","volume":"46","author":"C Benzm\u00fcller","year":"2017","unstructured":"Benzm\u00fcller, C.: Cut-elimination for quantified conditional logic. J. Philos. Logic 46(3), 333\u2013353 (2017). https:\/\/doi.org\/10.1007\/s10992-016-9403-0","journal-title":"J. Philos. Logic"},{"key":"14_CR4","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1016\/j.scico.2018.10.008","volume":"172","author":"C Benzm\u00fcller","year":"2019","unstructured":"Benzm\u00fcller, C.: Universal (meta-) logical reasoning: recent successes. Sci. Comput. Program. 172, 48\u201362 (2019)","journal-title":"Sci. Comput. Program."},{"issue":"103823","key":"14_CR5","first-page":"1","volume":"24","author":"C Benzm\u00fcller","year":"2019","unstructured":"Benzm\u00fcller, C.: Universal (meta-) logical reasoning: the wise men puzzle (Isabelle\/HOL Dataset). Data Brief 24(103823), 1\u20135 (2019)","journal-title":"Data Brief"},{"unstructured":"Benzm\u00fcller, C., Andrews, P.: Church\u2019s type theory. In: Zalta, E.N. (ed.) The Stanford Encyclopedia of Philosophy, (in pdf version). Metaphysics Research Lab, Stanford University, summer 2019 edition, pp. 1\u201362 (2019)","key":"14_CR6"},{"issue":"4","key":"14_CR7","doi-asserted-by":"publisher","first-page":"1027","DOI":"10.2178\/jsl\/1102022211","volume":"69","author":"C Benzm\u00fcller","year":"2004","unstructured":"Benzm\u00fcller, C., Brown, C., Kohlhase, M.: Higher-order semantics and extensionality. J. Symb. Logic 69(4), 1027\u20131088 (2004)","journal-title":"J. Symb. Logic"},{"key":"14_CR8","series-title":"Computational Logic","first-page":"215","volume-title":"Handbook of the History of Logic","author":"C Benzm\u00fcller","year":"2014","unstructured":"Benzm\u00fcller, C., Miller, D.: Automation of higher-order logic. In: Gabbay, D.M., Siekmann, J.H., Woods, J. (eds.) Handbook of the History of Logic. Computational Logic, vol. 9, pp. 215\u2013254. Elsevier, North Holland (2014)"},{"key":"14_CR9","first-page":"116","volume":"51","author":"J Blanchette","year":"2011","unstructured":"Blanchette, J., B\u00f6hme, S., Paulson, L.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51, 116\u2013130 (2011)","journal-title":"J. Autom. Reason."},{"issue":"2","key":"14_CR10","doi-asserted-by":"publisher","first-page":"56","DOI":"10.2307\/2266170","volume":"5","author":"A Church","year":"1940","unstructured":"Church, A.: A formulation of the simple theory of types. J. Symb. Logic 5(2), 56\u201368 (1940)","journal-title":"J. Symb. Logic"},{"key":"14_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"479","DOI":"10.1007\/978-3-540-27813-9_41","volume-title":"Computer Aided Verification","author":"P Gammie","year":"2004","unstructured":"Gammie, P., van der Meyden, R.: MCK: model checking the logic of knowledge. In: Alur, R., Peled, D.A. (eds.) CAV 2004. LNCS, vol. 3114, pp. 479\u2013483. Springer, Heidelberg (2004). https:\/\/doi.org\/10.1007\/978-3-540-27813-9_41"},{"unstructured":"Glei\u00dfner, T., Steen, A., Benzm\u00fcller, C.: Theorem provers for every normal modal logic. In: Eiter, T., Sands, D. (eds.) LPAR-21. 21st International Conference on Logic for Programming, Artificial Intelligence and Reasoning, volume 46 of EPiC Series in Computing, pp. 14\u201330. EasyChair, Maun (2017)","key":"14_CR12"},{"issue":"1","key":"14_CR13","doi-asserted-by":"publisher","first-page":"173","DOI":"10.1007\/BF01700692","volume":"38","author":"K G\u00f6del","year":"1931","unstructured":"G\u00f6del, K.: \u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I. Monatshefte f\u00fcr Mathematik und Physik 38(1), 173\u2013198 (1931). https:\/\/doi.org\/10.1007\/BF01700692","journal-title":"Monatshefte f\u00fcr Mathematik und Physik"},{"issue":"2","key":"14_CR14","doi-asserted-by":"publisher","first-page":"81","DOI":"10.2307\/2266967","volume":"15","author":"L Henkin","year":"1950","unstructured":"Henkin, L.: Completeness in the theory of types. J. Symb. Logic 15(2), 81\u201391 (1950)","journal-title":"J. Symb. Logic"},{"issue":"1","key":"14_CR15","doi-asserted-by":"publisher","first-page":"31","DOI":"10.1007\/s11229-013-0278-0","volume":"190","author":"WH Holliday","year":"2013","unstructured":"Holliday, W.H., Hoshi, T., Icard, T.F.: Information dynamics and uniform substitution. Synthese 190(1), 31\u201355 (2013). https:\/\/doi.org\/10.1007\/s11229-013-0278-0","journal-title":"Synthese"},{"issue":"9","key":"14_CR16","doi-asserted-by":"publisher","first-page":"798","DOI":"10.1111\/phc3.12059","volume":"8","author":"E Pacuit","year":"2013","unstructured":"Pacuit, E.: Dynamic epistemic logic i: modeling knowledge and belief. Philos. Comp. 8(9), 798\u2013814 (2013)","journal-title":"Philos. Comp."},{"doi-asserted-by":"crossref","unstructured":"Pfenning, F., Elliott, C.: Higher-order abstract syntax. In: Proceedings of the ACM SIGPLAN 1988 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, 22\u201324 June 1988, pp. 199\u2013208. ACM (1988)","key":"14_CR17","DOI":"10.1145\/960116.54010"},{"unstructured":"Plaza, J.: Logics of public communications. In: Proceedings of the 4th International Symposium on Methodologies for Intelligent Systems (1989)","key":"14_CR18"},{"unstructured":"Raimondi, F., Lomuscio, A.: Verification of multiagent systems via ordered binary decision diagrams: an algorithm and its implementation. In: Proceedings of the Third International Joint Conference on Autonomous Agents and Multiagent Systems, AAMAS 2004, pp. 630\u2013637. IEEE (2004)","key":"14_CR19"},{"key":"14_CR20","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"MW Tobias Nipkow","year":"2002","unstructured":"Tobias Nipkow, M.W., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9"},{"issue":"2","key":"14_CR21","doi-asserted-by":"publisher","first-page":"367","DOI":"10.1093\/logcom\/exx038","volume":"28","author":"J van Benthem","year":"2018","unstructured":"van Benthem, J., van Eijck, J., Gattinger, M., Su, K.: Symbolic model checking for dynamic epistemic logic - S5 and beyond. J. Log. Comp. 28(2), 367\u2013402 (2018)","journal-title":"J. Log. Comp."},{"issue":"11","key":"14_CR22","doi-asserted-by":"publisher","first-page":"1620","DOI":"10.1016\/j.ic.2006.04.006","volume":"204","author":"J van Benthem","year":"2006","unstructured":"van Benthem, J., van Eijck, J., Kooi, B.: Logics of communication and change. Inf. Comput. 204(11), 1620\u20131662 (2006)","journal-title":"Inf. Comput."},{"unstructured":"van Ditmarsch, H., Halpern, J.Y., van Der Hoek, W., Kooi, B.: An introduction to logics of knowledge and belief. In: Handbook of Epistemic Logic, pp. 1\u201351 (2015)","key":"14_CR23"},{"issue":"2","key":"14_CR24","first-page":"105","volume":"149","author":"H van Ditmarsch","year":"2006","unstructured":"van Ditmarsch, H., van der Hoek, W., van der Meyden, R., Ruan, J.: Model checking Russian cards. ENTCS 149(2), 105\u2013123 (2006)","journal-title":"ENTCS"},{"unstructured":"van Eijck, J.: Demo-a demo of epistemic modelling. In: Interactive Logic. Selected Papers from the 7th Augustus de Morgan Workshop, London (2007). http:\/\/homepages.cwi.nl\/~jve\/papers\/07\/pdfs\/DEMO_IL.pdf","key":"14_CR25"},{"unstructured":"van Eijck, J.: Demo-s5. Technical report, CWI (2014). http:\/\/homepages.cwi.nl\/~jve\/software\/demo_s5","key":"14_CR26"}],"container-title":["Lecture Notes in Computer Science","Dynamic Logic. New Trends and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-65840-3_14","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,21]],"date-time":"2020-12-21T09:16:55Z","timestamp":1608542215000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-65840-3_14"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030658397","9783030658403"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-65840-3_14","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2020]]},"assertion":[{"value":"22 December 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"DaLi","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Dynamic Logic","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2020","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"9 October 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10 October 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"3","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"DaLi2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/www.cs.cas.cz\/dali2020\/","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":"31","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":"17","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":"6","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":"55% - 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":"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":"2","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)"}}]}}