{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,27]],"date-time":"2025-03-27T17:47:58Z","timestamp":1743097678439,"version":"3.40.3"},"publisher-location":"Cham","reference-count":13,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030810962"},{"type":"electronic","value":"9783030810979"}],"license":[{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"},{"start":{"date-parts":[[2021,1,1]],"date-time":"2021-01-01T00:00:00Z","timestamp":1609459200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2021]]},"DOI":"10.1007\/978-3-030-81097-9_3","type":"book-chapter","created":{"date-parts":[[2021,7,19]],"date-time":"2021-07-19T23:04:38Z","timestamp":1626735878000},"page":"32-46","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Formalizing Axiomatic Systems for\u00a0Propositional Logic in Isabelle\/HOL"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3601-0804","authenticated-orcid":false,"given":"Asta Halkj\u00e6r","family":"From","sequence":"first","affiliation":[]},{"given":"Agnes Moesg\u00e5rd","family":"Eschen","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3624-1159","authenticated-orcid":false,"given":"J\u00f8rgen","family":"Villadsen","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,7,20]]},"reference":[{"key":"3_CR1","doi-asserted-by":"crossref","unstructured":"Blanchette, J.C.: Formalizing the metatheory of logical calculi and automatic provers in Isabelle\/HOL (invited talk). In: Mahboubi, A., Myreen, M.O. (eds.) Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2019, 14\u201315 January 2019, Cascais, Portugal, pp. 1\u201313. ACM (2019)","DOI":"10.1145\/3293880.3294087"},{"issue":"1","key":"3_CR2","doi-asserted-by":"publisher","first-page":"109","DOI":"10.1007\/s10817-013-9278-5","volume":"51","author":"JC Blanchette","year":"2013","unstructured":"Blanchette, J.C., B\u00f6hme, S., Paulson, L.C.: Extending sledgehammer with SMT solvers. J. Autom. Reason. 51(1), 109\u2013128 (2013). https:\/\/doi.org\/10.1007\/s10817-013-9278-5","journal-title":"J. Autom. Reason."},{"key":"3_CR3","volume-title":"Introduction to Mathematical Logic","author":"A Church","year":"1956","unstructured":"Church, A.: Introduction to Mathematical Logic. Princeton University Press, Princeton (1956)"},{"issue":"3","key":"3_CR4","doi-asserted-by":"publisher","first-page":"329","DOI":"10.1023\/A:1012486904520","volume":"68","author":"B Fitelson","year":"2001","unstructured":"Fitelson, B., Wos, L.: Finding missing proofs with automated reasoning. Studia Logica 68(3), 329\u2013356 (2001). https:\/\/doi.org\/10.1023\/A:1012486904520","journal-title":"Studia Logica"},{"key":"3_CR5","unstructured":"From, A.H.: Formalizing Henkin-style completeness of an axiomatic system for propositional logic. In: Proceedings of the Web Summer School in Logic, Language and Information (WeSSLLII) and the European Summer School in Logic, Language and Information (ESSLLI) Virtual Student Session (2020), pp. 1\u201312, preliminary paper. https:\/\/www.brandeis.edu\/nasslli2020\/pdfs\/student-session-proceedings-compressed.pdf#page=8. Accepted for Springer post-proceedings"},{"key":"3_CR6","doi-asserted-by":"publisher","unstructured":"From, A.H., Villadsen, J., Blackburn, P.: Isabelle\/HOL as a meta-language for teaching logic. In: Quaresma, P., Neuper, W., Marcos, J. (eds.) Proceedings 9th International Workshop on Theorem Proving Components for Educational Software, ThEdu@IJCAR 2020, 29th June 2020, Paris, France. EPTCS, vol. 328, pp. 18\u201334 (2020). https:\/\/doi.org\/10.4204\/EPTCS.328.2","DOI":"10.4204\/EPTCS.328.2"},{"key":"3_CR7","unstructured":"From, A.H.: Epistemic logic: completeness of modal logics. Archive of Formal Proofs, October 2018. https:\/\/devel.isa-afp.org\/entries\/Epistemic_Logic.html, Formal proof development"},{"key":"3_CR8","unstructured":"From, A.H.: Formalizing a Seligman-style tableau system for hybrid logic. Archive of Formal Proofs, December 2019. https:\/\/isa-afp.org\/entries\/Hybrid_Logic.html, Formal proof development"},{"key":"3_CR9","unstructured":"Michaelis, J., Nipkow, T.: Formalized proof systems for propositional logic. In: Abel, A., Forsberg, F.N., Kaposi, A. (eds.) 23rd International Conference on Types for Proofs and Programs, TYPES 2017, 29 May\u20131 June 2017, Budapest, Hungary. LIPIcs, vol. 104, pp. 5:1\u20135:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2017)"},{"key":"3_CR10","doi-asserted-by":"publisher","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C. (eds.): Isabelle\/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45949-9","DOI":"10.1007\/3-540-45949-9"},{"issue":"7","key":"3_CR11","doi-asserted-by":"publisher","first-page":"1169","DOI":"10.1007\/s10817-020-09561-0","volume":"64","author":"A Schlichtkrull","year":"2020","unstructured":"Schlichtkrull, A., Blanchette, J., Traytel, D., Waldmann, U.: Formalizing Bachmair and Ganzinger\u2019s ordered resolution prover. J. Autom. Reason. 64(7), 1169\u20131195 (2020)","journal-title":"J. Autom. Reason."},{"key":"3_CR12","unstructured":"\u0141ukasiewicz, J.: The shortest axiom of the implicational calculus of propositions. Proc. Royal Irish Acad. Sect. A: Math. Phys. Sci. 52, 25\u201333 (1948)"},{"key":"3_CR13","unstructured":"Wos, L., Pieper, G.W.: Automated Reasoning and the Discovery of Missing and Elegant Proofs. Rinton Press, Princeton (2003)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-81097-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,19]],"date-time":"2021-07-19T23:05:25Z","timestamp":1626735925000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-81097-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021]]},"ISBN":["9783030810962","9783030810979"],"references-count":13,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-81097-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2021]]},"assertion":[{"value":"20 July 2021","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CICM","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Intelligent Computer Mathematics","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Timisoara","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Romania","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2021","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"26 July 2021","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"31 July 2021","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"14","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"mkm2021","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/cicm-conference.org\/2021\/cicm.php","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":"38","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":"8","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":"32% - 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":"3,5","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)"}}]}}