RISC RISC Research Institute for Symbolic Computation  
  • @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 = {Schloss Hagenberg, 4232 Hagenberg, Austria}