{"id":6989,"date":"2020-02-09T05:21:41","date_gmt":"2020-02-09T04:21:41","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6989"},"modified":"2020-02-08T19:24:47","modified_gmt":"2020-02-08T18:24:47","slug":"resena-a-comprehensive-framework-for-saturation-theorem-proving","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-a-comprehensive-framework-for-saturation-theorem-proving\/","title":{"rendered":"Rese\u00f1a: A comprehensive framework for saturation theorem proving"},"content":{"rendered":"<div id=\"content\">\n<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre l\u00f3gica titulado <a href=\"http:\/\/matryoshka.gforge.inria.fr\/pubs\/saturate_report.pdf\">A comprehensive framework for saturation theorem proving<\/a>.<\/p>\n<p>Sus autores son<\/p>\n<ul class=\"org-ul\">\n<li><a href=\"https:\/\/www.mpi-inf.mpg.de\/departments\/automation-of-logic\/people\/uwe-waldmann\/\">Uwe Waldmann<\/a> (del grupo <a href=\"https:\/\/www.mpi-inf.mpg.de\/departments\/automation-of-logic\/\">Automation of Logic<\/a> en el Max-Planck-Institut f\u00fcr Informatik, Saarland Informatics Campus, Saarbr\u00fccken, Alemania),<\/li>\n<li><a href=\"https:\/\/www.mpi-inf.mpg.de\/departments\/automation-of-logic\/people\/sophie-tourret\/\">Sophie Tourret<\/a> (del grupo <a href=\"https:\/\/www.mpi-inf.mpg.de\/departments\/automation-of-logic\/\">Automation of Logic<\/a> en el Max-Planck-Institut f\u00fcr Informatik, Saarland Informatics Campus, Saarbr\u00fccken, Alemania),<\/li>\n<li><a href=\"https:\/\/simon-robillard.net\/\">Simon Robillard<\/a> (del <a href=\"http:\/\/www.imt-atlantique.fr\/\">IMT Atlantique<\/a>, Nantes, Francia)) y<\/li>\n<li><a href=\"http:\/\/people.mpi-inf.mpg.de\/~jblanche\/\">Jasmin Blanchette<\/a> (del grupo <a href=\"https:\/\/www.cs.vu.nl\/~tcs\/\">Theoretical Computer Science<\/a> en la Vrije Universiteit Amsterdam, Netherlands).<\/li>\n<\/ul>\n<p>Su resumen es<\/p>\n<blockquote><p>One of the indispensable operations of realistic saturation theorem provers is (backward and forward) deletion of subsumed formu- las. In presentations of proof calculi, however, this is usually discussed only informally, and in the rare cases where there is a formal exposition, it is typically clumsy. This is because the equivalence of dynamic and static refutational completeness holds only for derivations where all deleted formulas are redundant, but using a standard notion of redundancy, a clause C does not make an instance C\u03c3 redundant.<\/p>\n<p>We present a framework for formal refutational completeness proofs of abstract provers that implement saturation calculi, such as ordered resolution or superposition. The framework relies on modular extensions of lifted redundancy criteria. It permits us to extend redundancy criteria so that they cover subsumption, and also to model entire prover architectures in such a way that the static refutational completeness of a calculus immediately implies the dynamic refutational completeness of, e.g., an Otter or DISCOUNT loop prover implementing the calculus. Our framework is mechanized in Isabelle\/HOL.<\/p><\/blockquote>\n<p>El trabajo es parte del proyecto <a href=\"http:\/\/matryoshka.gforge.inria.fr\/\">Matryoshka (Fast interactive verification through strong higher-order automation)<\/a><\/p>\n<p>El c\u00f3digo est\u00e1 incluido en el repositorio <a href=\"https:\/\/bitbucket.org\/isafol\/isafol\/src\/master\/Saturation_Framework\/\">IsaFoL<\/a> (<i>Isabelle Formalization of Logic<\/i>).<\/p>\n<\/div>\n<div id=\"postamble\" class=\"status\"><\/div>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de razonamiento formalizado en Isabelle\/HOL sobre l\u00f3gica titulado A comprehensive framework for saturation theorem proving. Sus autores son Uwe Waldmann (del grupo Automation of Logic en el Max-Planck-Institut f\u00fcr Informatik, Saarland Informatics Campus, Saarbr\u00fccken, Alemania), Sophie Tourret (del grupo Automation of Logic en el Max-Planck-Institut f\u00fcr Informatik, Saarland Informatics Campus,&#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":[144],"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\/6989"}],"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=6989"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6989\/revisions"}],"predecessor-version":[{"id":6991,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6989\/revisions\/6991"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6989"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6989"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6989"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}