Presenting proofs using logicographic symbols

K. Nakagawa, B. Buchberger. Presenting proofs using logicographic symbols. 6, 2001.

  • Koji Nakagawa
  • Bruno Buchberger
BuchProc. Int. Joint Conf. on Automated Reasoning (IJCAR 2001)
TypIn Konferenzband
Abstract 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.