{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T16:53:24Z","timestamp":1753894404097,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>As the development of formal proofs is a time-consuming task, it is important\nto devise ways of sharing the already written proofs to prevent wasting time\nredoing them. One of the challenges in this domain is to translate proofs\nwritten in proof assistants based on impredicative logics to proof assistants\nbased on predicative logics, whenever impredicativity is not used in an\nessential way. In this paper we present a transformation for sharing proofs\nwith a core predicative system supporting prenex universe polymorphism. It\nconsists in trying to elaborate each term into a predicative\nuniverse-polymorphic term as general as possible. The use of universe\npolymorphism is justified by the fact that mapping each universe to a fixed one\nin the target theory is not sufficient in most cases. During the elaboration,\nwe need to solve unification problems in the equational theory of universe\nlevels. In order to do this, we give a complete characterization of when a\nsingle equation admits a most general unifier. This characterization is then\nemployed in a partial algorithm which uses a constraint-postponement strategy\nfor trying to solve unification problems. The proposed translation is of course\npartial, but in practice allows one to translate many proofs that do not use\nimpredicativity in an essential way. Indeed, it was implemented in the tool\nPredicativize and then used to translate semi-automatically many non-trivial\ndevelopments from Matita's library to Agda, including proofs of Bertrand's\nPostulate and Fermat's Little Theorem, which (as far as we know) were not\navailable in Agda yet.<\/jats:p>","DOI":"10.46298\/lmcs-20(3:23)2024","type":"journal-article","created":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:05:22Z","timestamp":1725973522000},"source":"Crossref","is-referenced-by-count":0,"title":["Sharing proofs with predicative theories through universe-polymorphic elaboration"],"prefix":"10.46298","volume":"Volume 20, Issue 3","author":[{"given":"Thiago","family":"Felicissimo","sequence":"first","affiliation":[]},{"given":"Fr\u00e9d\u00e9ric","family":"Blanqui","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2024,9,10]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/14237\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/14237\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,9,10]],"date-time":"2024-09-10T13:05:22Z","timestamp":1725973522000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/12213"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,9,10]]},"references-count":0,"URL":"https:\/\/doi.org\/10.46298\/lmcs-20(3:23)2024","relation":{"has-preprint":[{"id-type":"arxiv","id":"2308.15465v3","asserted-by":"subject"},{"id-type":"arxiv","id":"2308.15465v2","asserted-by":"subject"}],"is-same-as":[{"id-type":"arxiv","id":"2308.15465","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.2308.15465","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2024,9,10]]},"article-number":"12213"}}