{"id":3199,"date":"2013-04-10T06:27:43","date_gmt":"2013-04-10T06:27:43","guid":{"rendered":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/?p=3199"},"modified":"2013-04-10T06:28:26","modified_gmt":"2013-04-10T06:28:26","slug":"resena-ai-over-large-formal-knowledge-bases-the-first-decade","status":"publish","type":"post","link":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/resena-ai-over-large-formal-knowledge-bases-the-first-decade\/","title":{"rendered":"Rese\u00f1a: AI over large formal knowledge bases: The first decade"},"content":{"rendered":"<p>Se ha publicado un art\u00edculo sobre aplicaciones de la inteligencia artificial a la demostraci\u00f3n autom\u00e1tica de teoremas titulado <a href=\"http:\/\/www.computing.dundee.ac.uk\/staff\/katya\/arw13\/papers\/paper_21.pdf\">AI over large formal knowledge bases: The first decade<\/a>.<\/p>\n<p>Su autor es <a href=\"http:\/\/www.cs.ru.nl\/~urban\">Josef Urban<\/a> (de la Univ. de Nimega, Pa\u00edses Bajos) y lo presentar\u00e1 ma\u00f1ana en el <a href=\"http:\/\/www.computing.dundee.ac.uk\/staff\/katya\/arw13\/index.html\">ARW2013<\/a> (20th Automated Reasoning Workshop).<\/p>\n<p>Su resumen es<\/p>\n<blockquote><p>\nIn March 2003, the first version of the <a href=\"http:\/\/wiki.mizar.org\/twiki\/bin\/view\/Mizar\/MpTP\">Mizar Problems for Theorem Proving (MpTP)<\/a> was released. In the past ten years, such large formal knowledge bases have started to provide an interesting playground for combining deductive and inductive AI methods. The talk will discuss three related areas of application in which machine learning and general AI have been recently experimented with: (i) premise selection for theorem proving over large formal libraries built with systems like <a href=\"http:\/\/www.mizar.org\">Mizar<\/a>, <a href=\"http:\/\/www.cl.cam.ac.uk\/~jrh13\/hol-light\">HOL Light<\/a>, and <a href=\"http:\/\/isabelle.in.tum.de\">Isabelle<\/a> (ii) advising and tuning <a href=\"http:\/\/www.cs.miami.edu\/~tptp\/cgi-bin\/SystemOnTPTP\">first-order automated theorem provers<\/a> such as <a href=\"http:\/\/www4.informatik.tu-muenchen.de\/~schulz\/E\/E.html\">E<\/a> and <a href=\"http:\/\/www.leancop.de\">leanCoP<\/a>, and (iii) building larger inductive\/deductive AI systems such as <a href=\"https:\/\/github.com\/JUrban\/MPTP2\/tree\/master\/MaLARea\">MaLARea<\/a>. Here I focus on the wider motivation for this work.\n<\/p><\/blockquote>\n","protected":false},"excerpt":{"rendered":"<p>Se ha publicado un art\u00edculo sobre aplicaciones de la inteligencia artificial a la demostraci\u00f3n autom\u00e1tica de teoremas titulado AI over large formal knowledge bases: The first decade. Su autor es Josef Urban (de la Univ. de Nimega, Pa\u00edses Bajos) y lo presentar\u00e1 ma\u00f1ana en el ARW2013 (20th Automated Reasoning Workshop). Su resumen es In March&#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":[1],"tags":[60,188,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\/3199"}],"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=3199"}],"version-history":[{"count":2,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3199\/revisions"}],"predecessor-version":[{"id":3201,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/posts\/3199\/revisions\/3201"}],"wp:attachment":[{"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/media?parent=3199"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/categories?post=3199"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/www.glc.us.es\/~jalonso\/vestigium\/wp-json\/wp\/v2\/tags?post=3199"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}