Taclets: a new paradigm for constructing interactive theorem provers.

Beckert, Bernhard ; Giese, Martin ; Habermalz, Elmar ; Hähnle, Reiner ; Roth, Andreas ; Rümmer, Philipp ; Schlager, Steffen

RACSAM, Tome 98 (2004), p. 17-53 / Harvested from Biblioteca Digital de Matemáticas

Abstract

Frameworks for interactive theorem proving give the user explicit control over the construction of proofs based on meta languages that contain dedicated control structures for describing proof construction. Such languages are not easy to master and thus contribute to the already long list of skills required by prospective users of interactive theorem provers. Most users, however, only need a convenient formalism that allows to introduce new rules with minimal overhead. On the the other hand, rules of calculi have not only purely logical content, but contain restrictions on the expected context of rule applications and heuristic information. We suggest a new and minimalist concept for implementing interactive theorem provers called taclet. Their usage can be mastered in a matter of hours, and they are efficiently compiled into the GUI of a prover. We implemented the KeY system, an interactive theorem prover for the full JAVA CARD language based on taclets.

Résumé

Los marcos para la demostración interactiva de teoremas permiten al usuario tener control explícito de la construcción de las demostraciones sobre la base de unos metalenguajes que contienen unas estructuras de control dedicadas a la descripción de la construcción de las demostraciones. Estos lenguajes no son fáciles de dominar y se añaden así a la ya larga lista de habilidades requeridas a los potenciales usuarios de los demostradores interactivos de teoremas. Sin embargo, la mayoría de los usuarios sólo necesitan un formalismo conveniente que les permita introducir nuevas reglas con el mínimo esfuerzo. Por otra parte, las reglas de cálculo no sólo tienen un contenido puramente lógico, sino que también contienen restricciones sobre el contexto esperado de las aplicaciones de reglas y la información heurística. Se propone un concepto nuevo y minimalista para la implementación de los demostradores interactivos de teoremas que se ha denominado ?taclet?. Se puede dominar su uso en cuestión de horas, y se compilan de forma eficaz en la interfaz gráfica de usuario de un demostrador. Se ha implementado el sistema KeY, un demostrador interactivo de teoremas basado en taclets para el lenguaje completo JAVA CARD.

Détail

Publié le : 2004-01-01

Zbl 1103.68798

DMLE-ID : 3595