@techreport{RISC3112,author = {Martin Giese and Bruno Buchberger},
title = {{Towards Practical Reflection for Formal Mathematics}},
language = {english},
abstract = {We describe a design for a system for mathematical theory
exploration that can be extended by implementing new reasoners using
the logical input language of the system. Such new reasoners can be
applied like the built-in reasoners, and it is possible to reason about
them, e.g. proving their soundness, within the system. This is achieved
in a practical and attractive way by adding reflection, i.e. a representation
mechanism for terms and formulae, to the system’s logical language, and
some knowledge about these entities to the system’s basic reasoners. The
approach has been evaluated using a prototypical implementation called
Mini-Tma. It will be incorporated into the Theorema system.},
number = {07-05},
year = {2007},
annote = {2007-04-10-A},
length = {12},
type = {RISC Report Series},
institution = {Research Institute for Symbolic Computation (RISC), Johannes Kepler University Linz},
address = {Altenberger Straße 69, 4040 Linz, Austria},
issn = {2791-4267 (online)}
}