{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:30:40Z","timestamp":1750221040219,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":36,"publisher":"ACM","license":[{"start":{"date-parts":[[2019,1,14]],"date-time":"2019-01-14T00:00:00Z","timestamp":1547424000000},"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":[[2019,1,14]]},"DOI":"10.1145\/3293880.3294094","type":"proceedings-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:56Z","timestamp":1546608836000},"page":"78-90","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["A proof-theoretic approach to certifying skolemization"],"prefix":"10.1145","author":[{"given":"Kaustuv","family":"Chaudhuri","sequence":"first","affiliation":[{"name":"Inria, France \/ LIX, France \/ \u00c9cole Polytechnique, France"}]},{"given":"Matteo","family":"Manighetti","sequence":"additional","affiliation":[{"name":"Inria, France \/ LIX, France \/ \u00c9cole Polytechnique, France"}]},{"given":"Dale","family":"Miller","sequence":"additional","affiliation":[{"name":"Inria, France \/ LIX, France \/ \u00c9cole Polytechnique, France"}]}],"member":"320","published-online":{"date-parts":[[2019,1,14]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.3.297"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/322248.322249"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/772062.772068"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.2178\/jsl\/1333566645"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.5555\/2383418.2383422"},{"key":"e_1_3_2_1_6_1","volume-title":"Scalable Fine-Grained Proofs for Formula Processing. In 26th International Conference on Automated Deduction (CADE) (LNCS) , Leonardo de Moura (Ed.)","volume":"10395","author":"Barbosa Haniel","year":"2017","unstructured":"Haniel Barbosa , Jasmin Christian Blanchette , and Pascal Fontaine . 2017 . Scalable Fine-Grained Proofs for Formula Processing. In 26th International Conference on Automated Deduction (CADE) (LNCS) , Leonardo de Moura (Ed.) , Vol. 10395 . Springer, 398\u2013412. Haniel Barbosa, Jasmin Christian Blanchette, and Pascal Fontaine. 2017. Scalable Fine-Grained Proofs for Formula Processing. In 26th International Conference on Automated Deduction (CADE) (LNCS) , Leonardo de Moura (Ed.), Vol. 10395. Springer, 398\u2013412."},{"key":"e_1_3_2_1_7_1","volume-title":"Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction","author":"Blanco Roberto","year":"2017","unstructured":"Roberto Blanco , Zakaria Chihani , and Dale Miller . 2017. Translating Between Implicit and Explicit Versions of Proof . In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction , Gothenburg, Sweden, August 6-11, 2017 , Proceedings (Lecture Notes in Computer Science) , Leonardo de Moura (Ed.), Vol. 10395 . Springer , 255\u2013273. Roberto Blanco, Zakaria Chihani, and Dale Miller. 2017. Translating Between Implicit and Explicit Versions of Proof. In Automated Deduction - CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 6-11, 2017, Proceedings (Lecture Notes in Computer Science) , Leonardo de Moura (Ed.), Vol. 10395. Springer, 255\u2013273."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exu030"},{"key":"e_1_3_2_1_9_1","unstructured":"Kaustuv Chaudhuri Matteo Manighetti and Dale Miller. 2018. Github repository accompanying this paper. https:\/\/github.com\/chaudhuri\/ proofcert-deskolemize\/ .  Kaustuv Chaudhuri Matteo Manighetti and Dale Miller. 2018. Github repository accompanying this paper. https:\/\/github.com\/chaudhuri\/ proofcert-deskolemize\/ ."},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-24312-2_14"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2016.06.007"},{"key":"e_1_3_2_1_12_1","volume-title":"Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013)","volume":"14","author":"Chihani Zakaria","year":"2013","unstructured":"Zakaria Chihani , Dale Miller , and Fabien Renaud . 2013 . Checking Foundational Proof Certificates for First-Order Logic (extended abstract) . In Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013) (EPiC Series) , J. C. Blanchette and J. Urban (Eds.) , Vol. 14 . EasyChair, 58\u201366. Zakaria Chihani, Dale Miller, and Fabien Renaud. 2013. Checking Foundational Proof Certificates for First-Order Logic (extended abstract). In Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013) (EPiC Series) , J. C. Blanchette and J. Urban (Eds.), Vol. 14. EasyChair, 58\u201366."},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9380-6"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.2307\/2266170"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.5555\/647852.737549"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/1099014.1709517"},{"key":"e_1_3_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48899-7_32"},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-40229-1_20"},{"key":"e_1_3_2_1_19_1","volume-title":"Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR) (CEUR Workshop Proceedings) , Pascal Fontaine, Stephan Schulz 0001","volume":"1635","author":"F\u00e4rber Michael","year":"2016","unstructured":"Michael F\u00e4rber and Cezary Kaliszyk . 2016 . No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions . In Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR) (CEUR Workshop Proceedings) , Pascal Fontaine, Stephan Schulz 0001 , and Josef Urban (Eds.) , Vol. 1635 . CEUR-WS.org, 24\u201331. Michael F\u00e4rber and Cezary Kaliszyk. 2016. No Choice: Reconstruction of First-order ATP Proofs without Skolem Functions. In Proceedings of the 5th Workshop on Practical Aspects of Automated Reasoning (PAAR) (CEUR Workshop Proceedings) , Pascal Fontaine, Stephan Schulz 0001, and Josef Urban (Eds.), Vol. 1635. CEUR-WS.org, 24\u201331."},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/11691372_11"},{"volume-title":"The Collected Papers of Gerhard Gentzen","author":"Gentzen Gerhard","key":"e_1_3_2_1_21_1","unstructured":"Gerhard Gentzen . 1935. Investigations into Logical Deduction . In The Collected Papers of Gerhard Gentzen , M. E. Szabo (Ed.). North-Holland , Amsterdam , 68\u2013131. Gerhard Gentzen. 1935. Investigations into Logical Deduction. In The Collected Papers of Gerhard Gentzen , M. E. Szabo (Ed.). North-Holland, Amsterdam, 68\u2013131."},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/3.6.827"},{"volume-title":"Mathematical Logic","author":"Kleene S. C.","key":"e_1_3_2_1_24_1","unstructured":"S. C. Kleene . 1968. Mathematical Logic . Wiley and Sons . S. C. Kleene. 1968. Mathematical Logic. Wiley and Sons."},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0168-0072(02)00081-7"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.07.041"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00370646"},{"volume-title":"Logic and Computer Science","author":"Miller Dale","key":"e_1_3_2_1_29_1","unstructured":"Dale Miller . 1990. Abstractions in logic programming . In Logic and Computer Science , Piergiorgio Odifreddi (Ed.). Academic Press , 329\u2013359. http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/ AbsInLP.pdf.pdf Dale Miller. 1990. Abstractions in logic programming. In Logic and Computer Science , Piergiorgio Odifreddi (Ed.). Academic Press, 329\u2013359. http:\/\/www.lix.polytechnique.fr\/Labo\/Dale.Miller\/papers\/ AbsInLP.pdf.pdf"},{"key":"e_1_3_2_1_30_1","volume-title":"Eighth International Logic Programming Conference. MIT Press","author":"Miller Dale","year":"1991","unstructured":"Dale Miller . 1991 . Unification of Simply Typed Lambda-Terms as Logic Programming . In Eighth International Logic Programming Conference. MIT Press , Paris, France, 255\u2013269. Dale Miller. 1991. Unification of Simply Typed Lambda-Terms as Logic Programming. In Eighth International Logic Programming Conference. MIT Press, Paris, France, 255\u2013269."},{"volume-title":"Programming with HigherOrder Logic","author":"Miller Dale","key":"e_1_3_2_1_31_1","unstructured":"Dale Miller and Gopalan Nadathur . 2012. Programming with HigherOrder Logic . Cambridge University Press . Dale Miller and Gopalan Nadathur. 2012. Programming with HigherOrder Logic . Cambridge University Press."},{"key":"e_1_3_2_1_32_1","volume-title":"Mitchell","author":"Nadathur Gopalan","year":"1999","unstructured":"Gopalan Nadathur and Dustin J . Mitchell . 1999 . System Description : Teyjus \u2014 A Compiler and Abstract Machine Based Implementation of \u03bbProlog. In 16th Conf. on Automated Deduction (CADE) (LNAI), H. Ganzinger (Ed.). Springer , Trento, 287\u2013291. Gopalan Nadathur and Dustin J. Mitchell. 1999. System Description: Teyjus \u2014 A Compiler and Abstract Machine Based Implementation of \u03bbProlog. In 16th Conf. on Automated Deduction (CADE) (LNAI), H. Ganzinger (Ed.). Springer, Trento, 287\u2013291."},{"volume-title":"Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.).","author":"Nonnengart Andreas","key":"e_1_3_2_1_33_1","unstructured":"Andreas Nonnengart and Christoph Weidenbach . 2001. Computing Small Clause Normal Forms . In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Vol. I . Elsevier Science B.V. , Chapter 6, 335\u2013367. Andreas Nonnengart and Christoph Weidenbach. 2001. Computing Small Clause Normal Forms. In Handbook of Automated Reasoning, Alan Robinson and Andrei Voronkov (Eds.). Vol. I. Elsevier Science B.V., Chapter 6, 335\u2013367."},{"key":"e_1_3_2_1_34_1","volume-title":"ARCADE","author":"Reger Giles","year":"2017","unstructured":"Giles Reger and Martin Suda . 2017. Checkable Proofs for First-Order Theorem Proving . In ARCADE 2017 , 1st International Workshop on Automated Reasoning : Challenges, Applications, Directions, Exemplary Achievements (EPiC Series in Computing) , Giles Reger and Dmitriy Traytel (Eds.), Vol. 51 . EasyChair , 55\u201363. http:\/\/www.easychair.org\/ publications\/paper\/5W2B Giles Reger and Martin Suda. 2017. Checkable Proofs for First-Order Theorem Proving. In ARCADE 2017, 1st International Workshop on Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements (EPiC Series in Computing) , Giles Reger and Dmitriy Traytel (Eds.), Vol. 51. EasyChair, 55\u201363. http:\/\/www.easychair.org\/ publications\/paper\/5W2B"},{"volume-title":"Mathematical Logic","author":"Shoenfield Joesph R.","key":"e_1_3_2_1_35_1","unstructured":"Joesph R. Shoenfield . 1967. Mathematical Logic . Addison-Wesley . Joesph R. Shoenfield. 1967. Mathematical Logic. Addison-Wesley."},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-012-0163-3"},{"key":"e_1_3_2_1_37_1","unstructured":"Enrico Tassi. 2018. Elpi: an extension language for Coq. CoqPL 2018: The Fourth International Workshop on Coq for Programming Languages. https:\/\/hal.inria.fr\/hal-01637063\/  Enrico Tassi. 2018. Elpi: an extension language for Coq. CoqPL 2018: The Fourth International Workshop on Coq for Programming Languages. https:\/\/hal.inria.fr\/hal-01637063\/"}],"event":{"name":"CPP '19: 8th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","SIGLOG ACM Special Interest Group on Logic and Computation"],"location":"Cascais Portugal","acronym":"CPP '19"},"container-title":["Proceedings of the 8th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294094","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3293880.3294094","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:43:50Z","timestamp":1750207430000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3293880.3294094"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,14]]},"references-count":36,"alternative-id":["10.1145\/3293880.3294094","10.1145\/3293880"],"URL":"https:\/\/doi.org\/10.1145\/3293880.3294094","relation":{},"subject":[],"published":{"date-parts":[[2019,1,14]]},"assertion":[{"value":"2019-01-14","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}