Presenting proofs using logicographic symbols

Autoren Koji Nakagawa
Bruno Buchberger
TitelPresenting proofs using logicographic symbols
BuchtitelProc. Int. Joint Conf. on Automated Reasoning (IJCAR 2001)
Typin Konferenzband
OrtSiena, Italy
MonatJune
Jahr2001
SCCH ID#128
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.