{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,11]],"date-time":"2024-09-11T14:29:05Z","timestamp":1726064945395},"publisher-location":"Cham","reference-count":39,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030388072"},{"type":"electronic","value":"9783030388089"}],"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"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2020]]},"DOI":"10.1007\/978-3-030-38808-9_1","type":"book-chapter","created":{"date-parts":[[2020,1,13]],"date-time":"2020-01-13T17:03:25Z","timestamp":1578935005000},"page":"3-18","update-policy":"http:\/\/dx.doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Mechanizing Bisimulation Theorems for Relation-Changing Logics in Coq"],"prefix":"10.1007","author":[{"given":"Raul","family":"Fervari","sequence":"first","affiliation":[]},{"given":"Francisco","family":"Trucco","sequence":"additional","affiliation":[]},{"given":"Beta","family":"Ziliani","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2020,1,14]]},"reference":[{"key":"1_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"142","DOI":"10.1007\/978-3-642-32621-9_11","volume-title":"Logic, Language, Information and Computation","author":"C Areces","year":"2012","unstructured":"Areces, C., Fervari, R., Hoffmann, G.: Moving arrows and four model checking results. In: Ong, L., de Queiroz, R. (eds.) WoLLIC 2012. LNCS, vol. 7456, pp. 142\u2013153. Springer, Heidelberg (2012). \nhttps:\/\/doi.org\/10.1007\/978-3-642-32621-9_11"},{"issue":"2","key":"1_CR2","doi-asserted-by":"publisher","first-page":"309","DOI":"10.1093\/jigpal\/jzt030","volume":"22","author":"C Areces","year":"2014","unstructured":"Areces, C., Fervari, R., Hoffmann, G.: Swap logic. Log. J. IGPL 22(2), 309\u2013332 (2014)","journal-title":"Log. J. IGPL"},{"issue":"4","key":"1_CR3","doi-asserted-by":"publisher","first-page":"601","DOI":"10.1093\/jigpal\/jzv020","volume":"23","author":"C Areces","year":"2015","unstructured":"Areces, C., Fervari, R., Hoffmann, G.: Relation-changing modal operators. Log. J. IGPL 23(4), 601\u2013627 (2015)","journal-title":"Log. J. IGPL"},{"issue":"7","key":"1_CR4","doi-asserted-by":"publisher","first-page":"1443","DOI":"10.1093\/logcom\/exy022","volume":"28","author":"C Areces","year":"2018","unstructured":"Areces, C., Fervari, R., Hoffmann, G., Martel, M.: Satisfiability for relation-changing logics. J. Log. Comput. 28(7), 1443\u20131470 (2018)","journal-title":"J. Log. Comput."},{"issue":"2","key":"1_CR5","doi-asserted-by":"publisher","first-page":"290","DOI":"10.1017\/S1755020310000389","volume":"4","author":"C Areces","year":"2011","unstructured":"Areces, C., Figueira, D., Figueira, S., Mera, S.: The expressive power of memory logics. Rev. Symb. Log. 4(2), 290\u2013318 (2011)","journal-title":"Rev. Symb. Log."},{"key":"1_CR6","doi-asserted-by":"publisher","first-page":"821","DOI":"10.1016\/S1570-2464(07)80017-6","volume-title":"Handbook of Modal Logic","author":"C Areces","year":"2007","unstructured":"Areces, C., ten Cate, B.: Hybrid logics. In: Blackburn, P., Wolter, F., van Benthem, J. (eds.) Handbook of Modal Logic, pp. 821\u2013868. Elsevier, Amsterdam (2007)"},{"key":"1_CR7","first-page":"293","volume":"231","author":"G Aucher","year":"2009","unstructured":"Aucher, G., Balbiani, P., Fari\u00f1as del Cerro, L., Herzig, A.: Global and local graph modifiers. ENTCS 231, 293\u2013307 (2009)","journal-title":"ENTCS"},{"issue":"2","key":"1_CR8","first-page":"269","volume":"28","author":"G Aucher","year":"2018","unstructured":"Aucher, G., van Benthem, J., Grossi, D.: Modal logics of sabotage revisited. JLC 28(2), 269\u2013303 (2018)","journal-title":"JLC"},{"key":"1_CR9","volume-title":"Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions","author":"Y Bertot","year":"2010","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development: Coq\u2019Art The Calculus of Inductive Constructions, 1st edn. Springer, Heidelberg (2010)","edition":"1"},{"key":"1_CR10","series-title":"Cambridge Tracts in Theoretical Computer Science","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884","volume-title":"Modal Logic","author":"P Blackburn","year":"2001","unstructured":"Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2001)"},{"key":"1_CR11","doi-asserted-by":"crossref","unstructured":"Blackburn, P., van Benthem, J.: Modal logic: a semantic perspective. In: Handbook of Modal Logic, pp. 1\u201384. Elsevier (2007)","DOI":"10.1016\/S1570-2464(07)80004-8"},{"key":"1_CR12","unstructured":"Bohrer, B., Platzer, A.: Toward structured proofs for dynamic logics. CoRR, abs\/1908.05535 (2019)"},{"key":"1_CR13","unstructured":"D\u2019Abrera, C., Gor\u00e9, R.: Verified synthesis of (very simple) Sahlqvist correspondents via Coq. In: AiML 2018, Short Presentations, pp. 26\u201330. College Publications (2018)"},{"key":"1_CR14","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"378","DOI":"10.1007\/978-3-319-21401-6_26","volume-title":"Automated Deduction \u2013 CADE-25","author":"L Moura de","year":"2015","unstructured":"de Moura, L., Kong, S., Avigad, J., van Doorn, F., von Raumer, J.: The lean theorem prover (system description). In: Felty, A.P., Middeldorp, A. (eds.) CADE 2015. LNCS (LNAI), vol. 9195, pp. 378\u2013388. Springer, Cham (2015). \nhttps:\/\/doi.org\/10.1007\/978-3-319-21401-6_26"},{"key":"1_CR15","volume-title":"Modal Logic in Coq","author":"P Wind de","year":"2001","unstructured":"de Wind, P.: Modal Logic in Coq. Vrije Universiteit, Amsterdam (2001)"},{"key":"1_CR16","doi-asserted-by":"crossref","unstructured":"Demri, S., Fervari, R.: On the complexity of modal separation logics. In: AiML 2018, pp. 179\u2013198. College Publications (2018)","DOI":"10.1093\/logcom\/exz019"},{"key":"1_CR17","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"692","DOI":"10.1007\/978-3-030-19570-0_45","volume-title":"Logics in Artificial Intelligence","author":"S Demri","year":"2019","unstructured":"Demri, S., Fervari, R., Mansutti, A.: Axiomatising logics with separating conjunction and modalities. In: Calimeri, F., Leone, N., Manna, M. (eds.) JELIA 2019. LNCS (LNAI), vol. 11468, pp. 692\u2013708. Springer, Cham (2019). \nhttps:\/\/doi.org\/10.1007\/978-3-030-19570-0_45"},{"key":"1_CR18","unstructured":"Fervari, R.: Relation-Changing Modal Logics. Ph.D. thesis, Universidad Nacional de C\u00f3rdoba, Argentina (2014)"},{"key":"1_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"82","DOI":"10.1007\/978-3-319-73579-5_6","volume-title":"Dynamic Logic. New Trends and Applications","author":"R Fervari","year":"2018","unstructured":"Fervari, R., Vel\u00e1zquez-Quesada, F.R.: Dynamic epistemic logics of introspection. In: Madeira, A., Benevides, M. (eds.) DALI 2017. LNCS, vol. 10669, pp. 82\u201397. Springer, Cham (2018). \nhttps:\/\/doi.org\/10.1007\/978-3-319-73579-5_6"},{"key":"1_CR20","first-page":"1","volume":"108","author":"R Fervari","year":"2019","unstructured":"Fervari, R., Vel\u00e1zquez-Quesada, F.R.: Introspection as an action in relational models. JLAMP 108, 1\u201323 (2019)","journal-title":"JLAMP"},{"key":"1_CR21","unstructured":"Girard, P., Seligman, J., Liu, F.: General dynamic dynamic logic. In: AiML 2012, pp. 239\u2013260. College Publications (2012)"},{"key":"1_CR22","unstructured":"Gonthier, G.: Formal proof \u2013 the four-color theorem (2008)"},{"key":"1_CR23","doi-asserted-by":"publisher","first-page":"e2","DOI":"10.1017\/fmp.2017.1","volume":"5","author":"TC Hales","year":"2017","unstructured":"Hales, T.C., et al.: A formal proof of the kepler conjecture. Forum Math. Pi 5, e2 (2017)","journal-title":"Forum Math. Pi"},{"key":"1_CR24","series-title":"Foundations of Computing","doi-asserted-by":"publisher","DOI":"10.7551\/mitpress\/2516.001.0001","volume-title":"Dynamic Logic","author":"D Harel","year":"2000","unstructured":"Harel, D.: Dynamic Logic. Foundations of Computing. The MIT Press, Cambridge (2000)"},{"key":"1_CR25","first-page":"479","volume":"44","author":"WA Howard","year":"1980","unstructured":"Howard, W.A.: The formulae-as-types notion of construction. To HB Curry: Essays Combin. Log. Lambda Calc. Formalism 44, 479\u2013490 (1980)","journal-title":"To HB Curry: Essays Combin. Log. Lambda Calc. Formalism"},{"key":"1_CR26","doi-asserted-by":"publisher","first-page":"67","DOI":"10.1002\/malq.19630090502","volume":"9","author":"S Kripke","year":"1963","unstructured":"Kripke, S.: Semantical analysis of modal logic I. Normal propositional calculi. Z. fur Math. Log. Grundlagen der Math. 9, 67\u201396 (1963)","journal-title":"Z. fur Math. Log. Grundlagen der Math."},{"key":"1_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"302","DOI":"10.1007\/978-3-540-24597-1_26","volume-title":"FST TCS 2003: Foundations of Software Technology and Theoretical Computer Science","author":"C L\u00f6ding","year":"2003","unstructured":"L\u00f6ding, C., Rohde, P.: Model checking and satisfiability for sabotage modal logic. In: Pandya, P.K., Radhakrishnan, J. (eds.) FSTTCS 2003. LNCS, vol. 2914, pp. 302\u2013313. Springer, Heidelberg (2003). \nhttps:\/\/doi.org\/10.1007\/978-3-540-24597-1_26"},{"key":"1_CR28","doi-asserted-by":"publisher","first-page":"67","DOI":"10.4204\/EPTCS.240.5","volume":"240","author":"Stefan Mitsch","year":"2017","unstructured":"Mitsch, S., Platzer, A.: The keymaera X proof IDE - concepts on usability in hybrid systems theorem proving. In: F-IDE@FM 2016. EPTCS, vol. 240, pp. 67\u201381 (2016)","journal-title":"Electronic Proceedings in Theoretical Computer Science"},{"key":"1_CR29","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0030541","volume-title":"Isabelle: A Generic Theorem Prover","year":"1994","unstructured":"Paulson, L.C. (ed.): Isabelle: A Generic Theorem Prover, vol. 828. Springer, Heidelberg (1994). \nhttps:\/\/doi.org\/10.1007\/BFb0030541"},{"issue":"3","key":"1_CR30","doi-asserted-by":"publisher","first-page":"483","DOI":"10.1007\/s13347-018-0312-8","volume":"32","author":"David Pym","year":"2018","unstructured":"Pym, D., Spring, J., O\u2019Hearn, P.W.: Why separation logic works. Philos. Technol. 32(3), 483\u2013516 (2019)","journal-title":"Philosophy & Technology"},{"key":"1_CR31","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS 2002, pp. 55\u201374. IEEE (2002)"},{"key":"1_CR32","unstructured":"Rohde, P.: On games and logics over dynamically changing structures. Ph.D. thesis, RWTH Aachen (2006)"},{"key":"1_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/978-3-540-71067-7_6","volume-title":"Theorem Proving in Higher Order Logics","author":"K Slind","year":"2008","unstructured":"Slind, K., Norrish, M.: A brief overview of HOL4. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 28\u201332. Springer, Heidelberg (2008). \nhttps:\/\/doi.org\/10.1007\/978-3-540-71067-7_6"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"268","DOI":"10.1007\/978-3-540-32254-2_16","volume-title":"Mechanizing Mathematical Reasoning","author":"J Benthem","year":"2005","unstructured":"Benthem, J.: An essay on sabotage and obstruction. In: Hutter, D., Stephan, W. (eds.) Mechanizing Mathematical Reasoning. LNCS (LNAI), vol. 2605, pp. 268\u2013276. Springer, Heidelberg (2005). \nhttps:\/\/doi.org\/10.1007\/978-3-540-32254-2_16"},{"issue":"2","key":"1_CR35","doi-asserted-by":"publisher","first-page":"157","DOI":"10.3166\/jancl.17.157-182","volume":"17","author":"J Benthem van","year":"2007","unstructured":"van Benthem, J., Liu, F.: Dynamic logic of preference upgrade. J. Appl. Non-Class. Log. 17(2), 157\u2013182 (2007)","journal-title":"J. Appl. Non-Class. Log."},{"key":"1_CR36","doi-asserted-by":"crossref","unstructured":"van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic epistemic logic with assignment. In: AAMAS 2005, pp. 141\u2013148. ACM (2005)","DOI":"10.1145\/1082473.1082495"},{"key":"1_CR37","series-title":"Synthese Library","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-5839-4","volume-title":"Dynamic Epistemic Logic","author":"H Ditmarsch van","year":"2007","unstructured":"van Ditmarsch, H., van der Hoek, W., Kooi, B.: Dynamic Epistemic Logic. Synthese Library. Springer, Heidelberg (2007). \nhttps:\/\/doi.org\/10.1007\/978-1-4020-5839-4"},{"key":"1_CR38","unstructured":"Wu, M., Gor\u00e9, R.: Verified decision procedures for modal logics. In: ITP 2019. LIPIcs, vol. 141, pp. 31:1\u201331:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019)"},{"key":"1_CR39","first-page":"219","volume":"338","author":"B Xavier","year":"2018","unstructured":"Xavier, B., Olarte, C., Reis, G., Nigam, V.: Mechanizing focused linear logic in Coq. ENTCS 338, 219\u2013236 (2018)","journal-title":"ENTCS"}],"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-38808-9_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,1,13]],"date-time":"2020-01-13T17:16:52Z","timestamp":1578935812000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-38808-9_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030388072","9783030388089"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-38808-9_1","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":"14 January 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":"Porto","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Portugal","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":"7 October 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 October 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"dali2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"http:\/\/workshop.dali.di.uminho.pt\/","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":"26","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":"12","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":"2","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":"46% - 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","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":"No","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}