{"id":3647,"date":"2013-09-17T07:14:58","date_gmt":"2013-09-17T05:14:58","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3647"},"modified":"2013-09-17T07:14:58","modified_gmt":"2013-09-17T05:14:58","slug":"theory-exploration-for-interactive-theorem-proving","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/theory-exploration-for-interactive-theorem-proving\/","title":{"rendered":"Theory exploration for interactive theorem proving"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre automatizaci\u00f3n del razonamiento titulado <a href=\"http:\/\/www.cse.chalmers.se\/~jomoa\/papers\/ai4fm2013.pdf\">Theory exploration for interactive theorem proving<\/a>.<\/p>\n<p>Su autora es <a href=\"http:\/\/www.cse.chalmers.se\/~jomoa\/\">Moa Johansson<\/a> (de la Universidad T\u00e9cnica Chalmers en Gotemburgo, Suecia).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nTheory exploration is an automated reasoning technique for discovering and proving interesting properties about some set of given functions, constants and datatypes. In this note we describe ongoing work on integrating the <a href=\"https:\/\/github.com\/danr\/hipspec\">HipSpec<\/a> theory exploration system with the interactive prover <a href=\"http:\/\/www.cl.cam.ac.uk\/research\/hvg\/Isabelle\/index.html\">Isabelle<\/a>. We believe that such an integration would be beneficial for several reasons. In an interactive proof attempt a natural application would be to allow the user to ask for some suggestions of new lemmas that might help the current proof development. Theory exploration may also be used to automatically generate and prove some basic lemmas as a first step in a new theory development. Furthermore, when the theory exploration system is used as a stand-alone system, it should output a checkable proofs, for instance for Isabelle, so that sessions can be saved for future use.\n<\/p><\/blockquote>\n<p>El trabajo se present\u00f3 el 22 de julio en el <a href=\"http:\/\/www.ai4fm.org\/ai4fm-2013\/\">AI4FM 2013<\/a> (<i>4th International Workshop on Artifical Intelligence for Formal Methods<\/i>).<\/p>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre automatizaci\u00f3n del razonamiento titulado Theory exploration for interactive theorem proving. Su autora es Moa Johansson (de la Universidad T\u00e9cnica Chalmers en Gotemburgo, Suecia). Su resumen es Theory exploration is an automated reasoning technique for discovering and proving interesting properties about some set of given functions, constants and datatypes. In&#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,220,144,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\/3647"}],"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=3647"}],"version-history":[{"count":1,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3647\/revisions"}],"predecessor-version":[{"id":3648,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3647\/revisions\/3648"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3647"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3647"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3647"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}