Automation of mathematical induction as part of the history of logic

PorJosé A. Alonso

Se ha publicado un artículo sobre la historia del razonamiento automático titulado Automation of mathematical induction as part of the history of logic.

Sus autores son

Su resumen es

We review the history of the automation of mathematical induction.

This article is further organized as follows.

§§ 4 and 5 offer a self-contained reference for the readers who are not familiar with the field of mathematical induction and its automation. In § 4 we introduce the essentials of mathematical induction. In § 5 we have to become more formal regarding recursive function definitions, their consistency, termination, and induction templates and schemes.

The main part is § 6, where we present the historically most important systems in automated induction, and discuss the details of software systems for explicit induction, with a focus on the 1970s. After describing the application context in § 6.1, we describe the following Boyer–Moore theorem provers: the Pure LISP Theorem Prover (§ 6.2) Thm (§ 6.3) Nqthm (§ 6.4), and ACL2 (§ 6.5). The most noteworthy remaining explicit- induction systems are sketched in § 6.6.

Alternative approaches to the automation of induction that do not follow the paradigm of explicit induction are discussed in § 7.

After summarizing the lessons learned in § 8, we conclude with § 9.

A fully automatic problem solver with human-style output

PorJosé A. Alonso

Se ha publicado un artículo sobre automatización del razonamiento titulado A fully automatic problem solver with human-style output.

Sus autores son Mohan Ganesalingam y Timothy Gowers.

Su resumen es

This paper describes a program that solves elementary mathematical problems, mostly in metric space theory, and presents solutions that are hard to distinguish from solutions that might be written by human mathematicians. The program is part of a more general project, which we also discuss.

Reseña: The Boyer-Moore waterfall model revisited

PorJosé A. Alonso

Uno de los problemas fundamentales dentro del campo del razonamiento automático es la automatización de la inducción. El método fundamental para automatizar la inducción es el de la cascada presentado por Robert S. Boyer y J S. Moore en su libro A Computational Logic e integrado en sus sistemas Nqthm y ACL2.

En el trabajo The Boyer-Moore waterfall model revisited se presenta una implementación del modelo de Boyer-Moore en el sistema HOL Light.

Sus autores son Petros Papapanagiotou y Jacques Fleuriot (de la Universidad de Edimburgo).

Su resumen es

In this paper, we investigate the potential of the Boyer-Moore waterfall model for the automation of inductive proofs within a modern proof assistant. We analyze the basic concepts and methodology underlying this 30-year-old model and implement a new, fully integrated tool in the theorem prover HOL Light that can be invoked as a tactic. We also describe several extensions and enhancements to the model. These include the integration of existing HOL Light proof procedures and the addition of state-of-the-art generalization techniques into the waterfall. Various features, such as proof feedback and heuristics dealing with non-termination, that are needed to make this automated tool useful within our interactive setting are also discussed. Finally, we present a thorough evaluation of the approach using a set of 150 theorems, and discuss the effectiveness of our additions and relevance of the model in light of our results.

El trabajo es una extensión de la Tesis de Máster de Petros Papapanagiotou titulada On the automation of inductive proofs in HOL
Light y sirve como lectura complementaria en el curso Automated Reasoning (2012-13) de la Universidad de Edimburgo. Las transparencias del correspondiente tema del curso son Inductive theorem proving.

Reseña: Lifting and transfer: A modular design for quotients in Isabelle/HOL

PorJosé A. Alonso

Se ha publicado un nuevo artículo sobre automatización del razonamiento en Isabelle/HOL: Lifting and transfer: A modular design for quotients in Isabelle/HOL.

Sus autores son Brian Huffman y Ondřej Kunčar (de la Technische Universität München).

El trabajo se presentará el 12 de agosto en el Isabelle Users Workshop 2012 en el marco del ITP 2012 (third conference on Interactive Theorem Proving).

Su resumen es

Quotients, subtypes, and other forms of type abstraction are ubiquitous in formal reasoning with higher-order logic. Typically, users want to build a library of operations and theorems about an abstract type, but they want to write definitions and proofs in terms of a more concrete representation type, or “raw” type. Earlier work on the Isabelle Quotient package [1, 2] has yielded great progress in automation, but it still has many technical limitations.

We present an improved, modular design centered around two new packages: the Transfer package for proving theorems, and the Lifting package for defining constants. Our new design is simpler, applicable in more situations, and has more user-friendly automation. An initial implementation is available in Isabelle 2012.

Reseña: Coq, a proof assistant based on higher-order intuitionistic type theory

PorJosé A. Alonso

La semana pasada Jean-Pierre Jouannaud hizo una presentación sobre razonamiento automático en el Instituto de estudios avanzados de la Universidad de Tsinghua: Coq, a proof assistant based on higher-order intuitionistic type theory.

En la presentación se incluyen comentarios sobre objetivos y logros del razonamiento formalizado, los fundamentos teóricos de los demostradores, la correspondencia de Curry-Horward, el cálculo de construcciones de Coq y su adecuación.