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.
En la clase de hoy de Informática de 1º del Grado en Matemáticas se han explicado las soluciones de los ejercicios de la 22ª relación, en la que se definen funciones para resolver los siguientes problemas de cálculo numérico:
Un aspecto a destacar desde el punto de vista de la programación es el uso de la abstracción de procedimientos.
Los ejercicios, y sus soluciones, se muestran a continuación.
Read More “I1M2012: Ejercicios de cálculo numérico en Haskell”
En la clase de hoy del curso Lógica matemática y fundamentos se ha estudiado la deducción natural en la lógica de primer orden.
Las transparencias de estas clases son las del tema 8.
A la vez que se presentaba las reglas, se ha comentado su formalización en Isabelle/HOL. La teoría correspondiente es
Read More “LMF2013: Deducción natural en lógica de primer orden”
Se ha publicado un artículo sobre razonamiento formalizado titudado Formalization of real analysis: A survey of proof assistants and libraries.
Sus autores son Sylvie Boldo, Catherine Lelay y Guillaume Melquiond.
Su resumen es
In the recent years, numerous proof systems have improved enough to be used for formally verifying non-trivial mathematical results. They, however, have different purposes and it is not always easy to choose which one is adapted to undertake a formalization effort. In this survey, we focus on properties related to real analysis: real numbers, arithmetic operators, limits, differentiability, integrability, and so on. We have chosen to look into the formalizations provided in standard by the following systems: Coq, HOL4, HOL Light, Isabelle/HOL, Mizar, ProofPower-HOL, and PVS. We have also accounted for large developments that play a similar role or extend standard libraries: ACL2(r) for ACL2, C-CoRN/MathClasses for Coq, and the NASA PVS library. This survey presents how real numbers have been defined in these various provers and how the notions of real analysis described above have been formalized. We also look at the proof automations these systems provide for real analysis.