Presentación | Participantes | Bibliografía (DML-E) | Bibliografía adicional | Enlaces de interés | Otros proyectos DML | Ayuda  
INICIO | 29 de marzo de 2024
  

Taclets: a new paradigm for constructing interactive theorem provers.

Título inglés Taclets: a new paradigm for constructing interactive theorem provers.
Título español Taclets: un nuevo paradigma para construir demostradores automáticos interactivos.
Autor/es Beckert, Bernhard ; Giese, Martin ; Habermalz, Elmar ; Hähnle, Reiner ; Roth, Andreas ; Rümmer, Philipp ; Schlager, Steffen
Organización Dep. Comput. Sci. Chalmers Univ. Technol. Göteborg Univ., Goteborg, Suecia;Dep. Comput. Sci. Univ. Karlsruhe, Karlsruhe, Alemania;Inst. Comput. Sci. Univ. Koblenz-Landau, Coblenza, Alemania;Softw. Des. Manag. AG, Offenbach, Alemania
Revista 1578-7303
Publicación 2004, 98 (1): 17-53, 24 Ref.
Tipo de documento articulo
Idioma Inglés
Resumen español 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.
Resumen inglés 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.
Icono pdf Acceso al artículo completo
Equipo DML-E
Instituto de Ciencias Matemáticas (ICMAT - CSIC)
rmm()icmat.es