Reseña: AI over large formal knowledge bases: The first decade

Se ha publicado un artículo sobre aplicaciones de la inteligencia artificial a la demostración automática de teoremas titulado AI over large formal knowledge bases: The first decade.

Su autor es Josef Urban (de la Univ. de Nimega, Países Bajos) y lo presentará mañana en el ARW2013 (20th Automated Reasoning Workshop).

Su resumen es

In March 2003, the first version of the Mizar Problems for Theorem Proving (MpTP) 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 Mizar, HOL Light, and Isabelle (ii) advising and tuning first-order automated theorem provers such as E and leanCoP, and (iii) building larger inductive/deductive AI systems such as MaLARea. Here I focus on the wider motivation for this work.