{"id":7634,"date":"2021-12-28T13:18:26","date_gmt":"2021-12-28T12:18:26","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=7634"},"modified":"2021-12-28T13:18:26","modified_gmt":"2021-12-28T12:18:26","slug":"resena-completeness-theorems-for-first-order-logic-analysed-in-constructive-type-theory","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-completeness-theorems-for-first-order-logic-analysed-in-constructive-type-theory\/","title":{"rendered":"Rese\u00f1a: Completeness theorems for first-order logic analysed in constructive type theory"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en <a href=\"https:\/\/coq.inria.fr\/\">Coq<\/a> sobre l\u00f3gica titulado <a href=\"https:\/\/arxiv.org\/pdf\/2006.04399.pdf\">Completeness theorems for first-order logic analysed in constructive type theory<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/yforster.github.io\/\">Yannick Forster<\/a> (del <a href=\"https:\/\/gallinette.gitlabpages.inria.fr\/website\/\">Gallinette team<\/a> de Nantes y del <a href=\"https:\/\/www.ps.uni-saarland.de\/\">Programming Systems Lab<\/a> en la <a href=\"http:\/\/www.uni-saarland.de\/en\/home.html\">Saarland University<\/a>, Alemania),<\/li>\n<li><a href=\"https:\/\/www.ps.uni-saarland.de\/~kirst\/\">Dominik Kirst<\/a> (del <a href=\"https:\/\/www.ps.uni-saarland.de\/\">Programming Systems Lab<\/a> en la <a href=\"http:\/\/www.uni-saarland.de\/en\/home.html\">Saarland University<\/a>, Alemania) y<\/li>\n<li><a href=\"https:\/\/dowehr.dortselb.st\/\">Dominik Wehr<\/a> (del <a href=\"https:\/\/www.logic-gu.se\/\">Logic Group<\/a> en la <a href=\"https:\/\/www.gu.se\/en\/flov\">University of Gothenburg<\/a>).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>We study various formulations of the completeness of first-order logic phrased in constructive type theory and mechanised in the Coq proof assistant. Specifically, we examine the completeness of variants of classical and intuitionistic natural deduction and sequent calculi with respect to model-theoretic, algebraic, and game-theoretic semantics. As completeness with respect to the standard model-theoretic semantics \u00e0 la Tarski and Kripke is not readily constructive, we analyse connections of completeness theorems to Markov&#8217;s Principle and Weak K\u00f6nig&#8217;s Lemma and discuss non-standard semantics admitting assumption-free completeness. We contribute a reusable Coq library for first-order logic containing all results covered in this paper.<\/p><\/blockquote>\n<p>El trabajo se ha presentado en el <a href=\"https:\/\/lfcs.ws.gc.cuny.edu\/lfcs-2020\/\">Logical Foundations of Computer Science (LFCS 2020)<\/a> y publicado en el <a href=\"https:\/\/academic.oup.com\/logcom\/search-results?f_Authors=Dominik+Wehr\">Journal of Logic and Computation<\/a>.<\/p>\n<p>El c\u00f3digo de las correspondientes teor\u00edas se encuentra <a href=\"https:\/\/www.ps.uni-saarland.de\/extras\/fol-completeness-ext\/website\/toc.html\">aqu\u00ed<\/a>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Coq sobre l\u00f3gica titulado Completeness theorems for first-order logic analysed in constructive type theory. Sus autores son Yannick Forster (del Gallinette team de Nantes y del Programming Systems Lab en la Saarland University, Alemania), Dominik Kirst (del Programming Systems Lab en la Saarland University, Alemania) y&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"closed","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"jetpack_post_was_ever_published":false,"_kad_post_transparent":"","_kad_post_title":"","_kad_post_layout":"","_kad_post_sidebar_id":"","_kad_post_content_style":"","_kad_post_vertical_padding":"","_kad_post_feature":"","_kad_post_feature_position":"","_kad_post_header":false,"_kad_post_footer":false,"_jetpack_newsletter_access":"","_jetpack_dont_email_post_to_subs":false,"_jetpack_newsletter_tier_id":0,"_jetpack_memberships_contains_paywalled_content":false,"footnotes":"","_jetpack_memberships_contains_paid_content":false},"categories":[100],"tags":[45,166,285],"jetpack_featured_media_url":"","jetpack_sharing_enabled":true,"jetpack_likes_enabled":false,"_links":{"self":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7634"}],"collection":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/users\/2"}],"replies":[{"embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/comments?post=7634"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7634\/revisions"}],"predecessor-version":[{"id":7635,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/7634\/revisions\/7635"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=7634"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=7634"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=7634"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}