Presenting proofs using logicographic symbols

Autoren Koji Nakagawa
Bruno Buchberger
Titel Presenting proofs using logicographic symbols
Buchtitel Proc. Int. Joint Conf. on Automated Reasoning (IJCAR 2001)
Typ in Konferenzband
Ort Siena, Italy
Monat June
Jahr 2001
SCCH ID# 128

Mathematics has a rich tradition in creating symbols and notation that is soundly integrated into the syntax of the underlying formal language and, at the same time, conveys the intuition behind the concepts described by the symbols and notation. Continuing this idea, in the Theorema system, with the new feature of logicographic symbols, we now provide a means to invent arbitrary new symbols and notation.In this paper we describe how logicographic symbols can be created, declared, and afterwards used as a part of the formal language of Theorema with an example. Also with logicographic symbols, formal proof text automatically generated by Theorema provers can become easy to read in a way that resembles telling a pictorial story about the mathematical concepts involved.