{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T05:05:23Z","timestamp":1750309523113,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":27,"publisher":"ACM","license":[{"start":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T00:00:00Z","timestamp":1736467200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2025,1,10]]},"DOI":"10.1145\/3703595.3705877","type":"proceedings-article","created":{"date-parts":[[2025,1,10]],"date-time":"2025-01-10T21:23:16Z","timestamp":1736544196000},"page":"98-111","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Tactic Script Optimisation for Aesop"],"prefix":"10.1145","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8861-5231","authenticated-orcid":false,"given":"Jannis","family":"Limperg","sequence":"first","affiliation":[{"name":"University of Munich (LMU), Munich, Germany"}]}],"member":"320","published-online":{"date-parts":[[2025,1,10]]},"reference":[{"key":"e_1_3_2_2_1_1","doi-asserted-by":"publisher","unstructured":"Jesse Alama. 2012. Escape to Mizar for ATPs. https:\/\/doi.org\/10.48550\/arXiv.1204.6615 arxiv:1204.6615. 10.48550\/arXiv.1204.6615","DOI":"10.48550\/arXiv.1204.6615"},{"key":"e_1_3_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.29007\/wm8b"},{"key":"e_1_3_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9335-3"},{"key":"e_1_3_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3372885.3373824"},{"key":"e_1_3_2_2_5_1","doi-asserted-by":"publisher","unstructured":"The Coq development team. 2022. The Coq proof assistant. https:\/\/doi.org\/10.5281\/zenodo.5846982 10.5281\/zenodo.5846982","DOI":"10.5281\/zenodo.5846982"},{"key":"e_1_3_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_3"},{"key":"e_1_3_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-79876-5_37"},{"key":"e_1_3_2_2_8_1","volume-title":"Improving representation of knowledge within the Mizar library. Studies in Logic, Grammar and Rhetoric, 18, 31","author":"Grabowski Adam","year":"2009","unstructured":"Adam Grabowski and Christoph Schwarzweller. 2009. Improving representation of knowledge within the Mizar library. Studies in Logic, Grammar and Rhetoric, 18, 31 (2009), https:\/\/inf.ug.edu.pl\/~schwarzw\/papers\/slgr09b.pdf"},{"key":"e_1_3_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-75100-4_5"},{"key":"e_1_3_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58156-1_53"},{"key":"e_1_3_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-61532-6_34"},{"key":"e_1_3_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-38574-2_18"},{"key":"e_1_3_2_2_13_1","doi-asserted-by":"publisher","unstructured":"Jannis Limperg. 2024. Supplement for Tactic Script Optimisation for Aesop. https:\/\/doi.org\/10.5281\/zenodo.14343543 10.5281\/zenodo.14343543","DOI":"10.5281\/zenodo.14343543"},{"key":"e_1_3_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3573105.3575671"},{"key":"e_1_3_2_2_15_1","first-page":"35","volume":"22","author":"Logic Karol P\u0105k.","year":"2010","unstructured":"Karol P\u0105k. 2010. The algorithms for improving and reorganizing natural deduction proofs. Studies in Logic, Grammar and Rhetoric, 22, 35 (2010), https:\/\/alioth.uwb.edu.pl\/~pakkarol\/articles\/KP-SLGR.pdf","journal-title":"Rhetoric"},{"key":"e_1_3_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-012-9267-0"},{"key":"e_1_3_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08434-3_27"},{"key":"e_1_3_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-015-9337-1"},{"key":"e_1_3_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.48456\/tr-396"},{"key":"e_1_3_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00165-019-00492-1"},{"key":"e_1_3_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74591-4_18"},{"key":"e_1_3_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-10(3:23)2014"},{"key":"e_1_3_2_2_23_1","volume-title":"PxTP","author":"Rudnicki Piotr","year":"2011","unstructured":"Piotr Rudnicki and Josef Urban. 2011. Escape to ATP for Mizar. In PxTP 2011. https:\/\/inria.hal.science\/hal-00677240"},{"key":"e_1_3_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.29007\/zbdb"},{"key":"e_1_3_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-53518-6_16"},{"key":"e_1_3_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-17511-4_25"},{"key":"e_1_3_2_2_27_1","volume-title":"Studies in Logic, Grammar, and Rhetoric, 10, 23","author":"Wenzel Makarius","year":"2007","unstructured":"Makarius Wenzel. 2007. Isabelle\/Isar\u2014a generic framework for human-readable proof documents. Studies in Logic, Grammar, and Rhetoric, 10, 23 (2007), https:\/\/mizar.uwb.edu.pl\/trybulec65\/19.pdf"}],"event":{"name":"CPP '25: 14th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG"],"location":"Denver CO USA","acronym":"CPP '25"},"container-title":["Proceedings of the 14th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705877","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3703595.3705877","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T01:18:08Z","timestamp":1750295888000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3703595.3705877"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,10]]},"references-count":27,"alternative-id":["10.1145\/3703595.3705877","10.1145\/3703595"],"URL":"https:\/\/doi.org\/10.1145\/3703595.3705877","relation":{},"subject":[],"published":{"date-parts":[[2025,1,10]]},"assertion":[{"value":"2025-01-10","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}