{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,28]],"date-time":"2025-03-28T04:51:05Z","timestamp":1743137465915,"version":"3.40.3"},"publisher-location":"Cham","reference-count":19,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783030510732"},{"type":"electronic","value":"9783030510749"}],"license":[{"start":{"date-parts":[[2020,1,1]],"date-time":"2020-01-01T00:00:00Z","timestamp":1577836800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/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":"https:\/\/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-51074-9_22","type":"book-chapter","created":{"date-parts":[[2020,6,29]],"date-time":"2020-06-29T22:02:47Z","timestamp":1593468167000},"page":"395-401","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":2,"title":["Logic-Independent Proof Search in\u00a0Logical Frameworks"],"prefix":"10.1007","author":[{"given":"Michael","family":"Kohlhase","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Rabe","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Claudio","family":"Sacerdoti Coen","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Jan Frederik","family":"Schaefer","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2020,6,24]]},"reference":[{"key":"22_CR1","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"162","DOI":"10.1007\/978-3-540-71070-7_14","volume-title":"Automated Reasoning","author":"C Benzm\u00fcller","year":"2008","unstructured":"Benzm\u00fcller, C., Paulson, L.C., Theiss, F., Fietzke, A.: LEO-II - A Cooperative Automatic Theorem Prover for Classical Higher-Order Logic (System Description). In: Armando, A., Baumgartner, P., Dowek, G. (eds.) IJCAR 2008. LNCS (LNAI), vol. 5195, pp. 162\u2013170. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-71070-7_14"},{"doi-asserted-by":"crossref","unstructured":"Chihani, Z., Miller, D., Renaud, F.: Checking foundational proof certificates for first-order logic. In: Blanchette, J., Urban, J. (eds.) Proof Exchange for Theorem Proving. EasyChair, pp. 58\u201366 (2013)","key":"22_CR2","DOI":"10.1007\/978-3-642-38574-2_11"},{"key":"22_CR3","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-22673-1_24","volume-title":"Intelligent Computer Mathematics","author":"M Codescu","year":"2011","unstructured":"Codescu, M., Horozal, F., Kohlhase, M., Mossakowski, T., Rabe, F.: Project Abstract: Logic Atlas and Integrator (LATIN). In: Davenport, J.H., Farmer, W.M., Urban, J., Rabe, F. (eds.) CICM 2011. LNCS (LNAI), vol. 6824, pp. 289\u2013291. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22673-1_24"},{"unstructured":"Coq Development Team: The Coq proof assistant: reference manual. Technical report INRIA (2015)","key":"22_CR4"},{"unstructured":"GLIF Demo. https:\/\/gl.kwarc.info\/COMMA\/glif-demo-ijcar-2020. Accessed 27 Jan 2020","key":"22_CR5"},{"unstructured":"Generated ELPI Provers. https:\/\/gl.mathhub.info\/MMT\/LATIN2\/tree\/devel\/elpi. Accessed 26 Jan 2020","key":"22_CR6"},{"issue":"1","key":"22_CR7","doi-asserted-by":"publisher","first-page":"143","DOI":"10.1145\/138027.138060","volume":"40","author":"R Harper","year":"1993","unstructured":"Harper, R., Honsell, F., Plotkin, G.: A framework for defining logics. J. Assoc. Comput. Mach. 40(1), 143\u2013184 (1993)","journal-title":"J. Assoc. Comput. Mach."},{"doi-asserted-by":"crossref","unstructured":"Kohlhase, M., Koller, A.: Resource-adaptive model generation as a performance model. Log. J. IGPL 11(4), 435\u2013456 (2003). http:\/\/jigpal.oxfordjournals.org\/cgi\/content\/abstract\/11\/4\/435","key":"22_CR8","DOI":"10.1093\/jigpal\/11.4.435"},{"doi-asserted-by":"crossref","unstructured":"Kohlhase, M., et al.: Logic-independent proof search in logical frameworks (extended report). Extended Report of Conference Submission (2020). https:\/\/kwarc.info\/kohlhase\/submit\/mmtelpi.pdf","key":"22_CR9","DOI":"10.1007\/978-3-030-51074-9_22"},{"doi-asserted-by":"publisher","unstructured":"Kohlhase, M., Schaefer, J.F.: GF + MMT = GLF - from language to semantics through LF. In: Miller, D., Scagnetto, I., (eds.) Proceedings of the Fourteenth Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2019). Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 307, pp. 24\u201339 (2019). https:\/\/doi.org\/10.4204\/EPTCS.307.4","key":"22_CR10","DOI":"10.4204\/EPTCS.307.4"},{"unstructured":"LATIN2 - Logic Atlas Version 2. https:\/\/gl.mathhub.info\/MMT\/LATIN2. Accessed 02 June 2017","key":"22_CR11"},{"unstructured":"Miller, D: \n$$\\lambda $$\nProlog. http:\/\/www.lix.polytechnique.fr\/Labo\/ Dale. Miller\/lProlog\/","key":"22_CR12"},{"unstructured":"Paulson, L.C.: Isabelle: The Next 700 Theorem Provers. In: arXiv CoRR cs.LO\/9301106 (1993). https:\/\/arxiv.org\/abs\/cs\/9301106","key":"22_CR13"},{"key":"22_CR14","series-title":"Lecture Notes in Computer Science","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. LNCS, vol. 828. Springer, Heidelberg (1994). https:\/\/doi.org\/10.1007\/BFb0030541"},{"issue":"6","key":"22_CR15","doi-asserted-by":"publisher","first-page":"1753","DOI":"10.1093\/logcom\/exu079","volume":"27","author":"F Rabe","year":"2017","unstructured":"Rabe, F.: How to identify, translate, and combine logics? J. Log. Comput. 27(6), 1753\u20131798 (2017)","journal-title":"J. Log. Comput."},{"issue":"4","key":"22_CR16","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1145\/3234693","volume":"19","author":"F Rabe","year":"2018","unstructured":"Rabe, F.: A modular type reconstruction algorithm. ACM Trans. Comput. Log. 19(4), 1\u201343 (2018)","journal-title":"ACM Trans. Comput. Log."},{"issue":"2","key":"22_CR17","doi-asserted-by":"publisher","first-page":"145","DOI":"10.1017\/S0956796803004738","volume":"14","author":"A Ranta","year":"2004","unstructured":"Ranta, A.: Grammatical framework, a type-theoretical grammar formalism. J. Funct. Programm. 14(2), 145\u2013189 (2004)","journal-title":"J. Funct. Programm."},{"unstructured":"Coen, C.S., Tassi, E.: The ELPI system (2015). https:\/\/github.com\/LPCIC\/elpi","key":"22_CR18"},{"unstructured":"Tishkovsky, D., Schmidt, R.A., Khodadadi, M.: MetTeL2: towards a tableau prover generation platform. In: Proceedings of the Third Workshop on Practical As- pects of Automated Reasoning (PAAR-2012), p. 149 (2012)","key":"22_CR19"}],"container-title":["Lecture Notes in Computer Science","Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-51074-9_22","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,7,2]],"date-time":"2022-07-02T21:33:49Z","timestamp":1656797629000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-030-51074-9_22"}},"subtitle":["(Short Paper)"],"short-title":[],"issued":{"date-parts":[[2020]]},"ISBN":["9783030510732","9783030510749"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-51074-9_22","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":"24 June 2020","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"IJCAR","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Joint Conference on Automated Reasoning","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Paris","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"France","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":"1 July 2020","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"4 July 2020","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"10","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"ijcar2020","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/ijcar2020.org\/","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":"150","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":"46","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":"5","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":"31% - 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.03","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":"7.38","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)"}},{"value":"11 system descriptions are also included. The conference was held virtually due to the COVID-19 pandemic.","order":10,"name":"additional_info_on_review_process","label":"Additional Info on Review Process","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"This content has been made available to all.","name":"free","label":"Free to read"}]}}