En la clase de hoy del curso Lógica matemática y fundamentos se han resuelto los ejercicios 10, 11, 12, 13 y 16 de la relación 7 sobre deducción natural en lógica de primer orden con Isabelle/HOL.
Las soluciones de los ejercicios resueltos se muestran a continuación:
Read More “LMF2013: Ejercicios de deducción natural en lógica de primer orden con Isabelle/HOL (1)”
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.