{"id":4987,"date":"2015-08-26T07:07:02","date_gmt":"2015-08-26T05:07:02","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=4987"},"modified":"2015-08-26T07:08:16","modified_gmt":"2015-08-26T05:08:16","slug":"resena-exploring-theories-with-a-model-finding-assistant","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-exploring-theories-with-a-model-finding-assistant\/","title":{"rendered":"Rese\u00f1a: Exploring theories with a model-finding assistant"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento titulado <a href=\"http:\/\/web.cs.wpi.edu\/~dd\/publications\/cade15.pdf\">Exploring theories with a model-finding assistant<\/a>.<\/p>\n<p>Sus autores son <a href=\"http:\/\/users.wpi.edu\/~salmans\/info\/Home.html\">Salman Saghafi<\/a>, <a href=\"http:\/\/ryandanas.github.io\">Ryan Danas<\/a> y <a href=\"http:\/\/web.cs.wpi.edu\/~dd\/\">Daniel J. Dougherty<\/a> (del <a href=\"http:\/\/web.cs.wpi.edu\/Research\/alas\/\">Applied Logic and Security Lab<\/a> en el <em>Worcester Polytechnic Institute<\/em>, Worcester, Massachusetts, USA).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\n  We present an approach to understanding first-order theories by exploring their models. A typical use case is the analysis of artifacts such as policies, protocols, configurations, and software designs. For the analyses we offer, users are not required to frame formal properties or construct derivations. Rather, they can explore examples of their designs, confirming the expected instances and perhaps recognizing bugs inherent in surprising instances.<\/p>\n<p>  Key foundational ideas include: the information preorder on models given by homomorphism, an inductively-defined refinement of the Herbrand base of a theory, and a notion of provenance for elements and facts in models. The implementation makes use of SMT-solving and an algorithm for minimization with respect to the information preorder on models.<\/p>\n<p>  Our approach is embodied in a tool, <a href=\"http:\/\/salmans.github.io\/Razor\">Razor<\/a>, that is complete for finite satisfiability and provides a read-eval-print loop used to navigate the set of finite models of a theory and to display provenance.\n<\/p><\/blockquote>\n<p>El trabajo se ha presentado en el <a href=\"http:\/\/conference.mi.fu-berlin.de\/cade-25\/home\">CADE-25<\/a> (<em>The 25th International Conference on Automated Deduction<\/em>).<\/p>\n<p>El c\u00f3digo en Haskell del sistema Razor se encuentra <a href=\"http:\/\/salmans.github.io\/Razor\">aqu\u00ed<\/a>.<\/p>\n<p>Este trabajo puede servir en los cursos de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf\">L\u00f3gica inform\u00e1tica<\/a>, <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/lmf\">L\u00f3gica matem\u00e1tica y fundamentos<\/a>, <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra\">Razonamiento autom\u00e1tico<\/a> y <em>L\u00f3gica computacional y teor\u00eda de modelos<\/em>.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo de automatizaci\u00f3n del razonamiento titulado Exploring theories with a model-finding assistant. Sus autores son Salman Saghafi, Ryan Danas y Daniel J. Dougherty (del Applied Logic and Security Lab en el Worcester Polytechnic Institute, Worcester, Massachusetts, USA). Su resumen es We present an approach to understanding first-order theories by exploring their&#8230;<\/p>\n","protected":false},"author":2,"featured_media":0,"comment_status":"open","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":[270,285,114,248],"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\/4987"}],"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=4987"}],"version-history":[{"count":3,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4987\/revisions"}],"predecessor-version":[{"id":4990,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/4987\/revisions\/4990"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=4987"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=4987"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=4987"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}