{"id":6453,"date":"2019-01-24T19:29:21","date_gmt":"2019-01-24T18:29:21","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=6453"},"modified":"2019-01-25T12:33:55","modified_gmt":"2019-01-25T11:33:55","slug":"ra2018-editores-logicos","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/ra2018-editores-logicos\/","title":{"rendered":"RA2018: Editores l\u00f3gicos"},"content":{"rendered":"<p>En la primera parte de la clase de hoy del curso de <a href=\"http:\/\/www.cs.us.es\/~jalonso\/cursos\/m-ra-18\">Razonamiento autom\u00e1tico<\/a> se han comentado el uso de editores l\u00f3gicos, distintos de Isabelle\/HOL, que facilitan y corrigen la escritura de demostraciones por deducci\u00f3n natural o mediante secuentes.<\/p>\n<p>El primero que se ha presentado es <a href=\"http:\/\/www.doc.ic.ac.uk\/pandora\/newpandora\">Pandora<\/a>. Es un editor para la deducci\u00f3n natural. Se han realizado las demostraciones que se muestran en este <a href=\"http:\/\/bit.ly\/1tqZIOe\">v\u00eddeo<\/a>. Un libro usando Pandora es <a href=\"https:\/\/www.doc.ic.ac.uk\/~susan\/firstyearbook.pdf\">Reasoned programming<\/a>.<\/p>\n<p>El segundo que se ha presentado es <a href=\"http:\/\/web.student.chalmers.se\/~jespolss\/Conan.html\">Conan<\/a>. Tambi\u00e9n es un editor para deducci\u00f3n natural. Se han realizado las mismas demostraciones que con Pandora. La descripci\u00f3n de Conan se encuentra en <a href=\"https:\/\/t.co\/8aNC1H9MvD\">Proof editor for natural deduction in first-order logic<\/a>.<\/p>\n<p>El tercero que se ha presentado es <a href=\"http:\/\/logitext.mit.edu\/main\">Logitext<\/a>. Es un un editor para el c\u00e1lculo de secuentes. Se han realizado las demostraciones propuestas en su <a href=\"http:\/\/logitext.mit.edu\/tutorial\">tutorial<\/a>.<\/p>\n<p>Finalmente se ha presentado <a href=\"http:\/\/protosmart.uhu.es\/apli2\/login\">APLI2 (APLIcaci\u00f3n de Ayuda Para L\u00f3gica Inform\u00e1tica)<\/a> que contiene una colecci\u00f3n de problemas para traducir argumentos del lenguaje natural al lenguaje de la l\u00f3gica de primer orden y autom\u00e1ticamente corrige la traducci\u00f3n.<\/p>\n","protected":false},"excerpt":{"rendered":"<p>En la primera parte de la clase de hoy del curso de Razonamiento autom\u00e1tico se han comentado el uso de editores l\u00f3gicos, distintos de Isabelle\/HOL, que facilitan y corrigen la escritura de demostraciones por deducci\u00f3n natural o mediante secuentes. El primero que se ha presentado es Pandora. Es un editor para la deducci\u00f3n natural. Se&#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":[322],"tags":[189,323],"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\/6453"}],"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=6453"}],"version-history":[{"count":4,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6453\/revisions"}],"predecessor-version":[{"id":6457,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/6453\/revisions\/6457"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=6453"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=6453"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=6453"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}