Bruno Buchberger, Martin Giese,
"Towards Practical Reflection for Formal Mathematics"
, Serie RISC Report Series, RISC, University of Linz, Altenbergerstraße 69, 4040 Linz, Austria, 2007
Original Titel:
Towards Practical Reflection for Formal Mathematics
Sprache des Titels:
Englisch
Original Kurzfassung:
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.
Sprache der Kurzfassung:
Englisch
Veröffentlicher:
RISC
Verlagsanschrift:
University of Linz, Altenbergerstraße 69, 4040 Linz, Austria
Forschungs-