{'fraction_non_alphanumeric': 0.02533582724026526, 'fraction_numerical': 0.006121407923822479, 'mean_word_length': 5.3111587982832615, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 0, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Logicographic Symbols: A New Feature in Theorema

Theorema is a mathematical software system emphasizing computer-supported theorem proving. Theorema is implemented in Mathematica and, thus, can be used on all platforms on which Mathematica is available. In this paper and talk, we explain the new Theorema language feature of logicographic symbols. This feature allows to introduce arbitrary new symbols for mathematical functions and predicates so that the user is not confined to a fixed vocabulary of symbols. The implementation of logicographic symbols in Theorema heavily involves tools of the front-end of Mathematica. Introduction In this paper, we report on the new concept of logicographic symbols and its realization in the frame of the Theorema system, [Buchberger et. al. 1997], [Buchberger et. al. 2000]. This work is joint work with Koji Nakagawa: The concept of logicographic symbols is due to the author and was first introduced in [Buchberger 2000]. All the implementation of the concept in Theorema was done by Koji Nakagawa and is the main part of the forthcoming PhD thesis [Nakagawa 2001]. The development of formal mathematics is important for achieving a new level of rigor, reliability, manageabil ity, automation and re-usability in mathematics and a smooth and computer-supported transition from mathemati cal knowledge to mathematical algorithms and, ultimately, to applications. Currently, formal mathematics is based on the usual linear and/or two-dimensional mathematical notation of (some version of) predicate logic starting from constants for functions and predicates. The vocabulary of constants consists of infinitely many textual identifiers and a fixed arsenal of mathematical symbols as, for example, "+", "/" etc. Often, however, in order to understand the intuitive idea behind mathematical concepts, one uses graphics. These graphical illustrations of concepts and the constants (identifiers and/or symbols) used for denoting the concepts in formal texts, logically, are not connected: The constants live in the world of rigorous formal derivations whereas the graphical illustrations live in the world of informal heuristics. The graphical illustrations are helpful for understanding the concepts involved and their properties but do not have any logical bearing. The constants are the basic ingredients of the rigorous mathematical derivations but often do not convey well the underlying intuition. In Theorema, a system for formal mathematics implemented in Mathematica, we now introduced the new language feature of "logicographic symbols". These are two-dimensional graphics that can be composed by the user of the Theorema language (using various design tools for generating graphics) in order to convey the meaning of a concept in an intuitively easy and appealing way. Formally, however, these graphics are then treated as new function or predicate constants of Theorema. For this, logicographic symbols have "slots" for the function or predicate arguments. Consequently, logicographic symbols can also be nested and can be combined arbitrarily with ordinary function and predicate constants. Formal texts using logicographic symbols are then both formally rigorous and intuitively appealing. In other words, logicographic symbols aim at bridging the gap between formal rigor and intuition in mathematics. Alternatively, one can view logicographic symbols simply as a means for providing the user with an infinite source of mathematical symbols of arbitrary graphical complexity to be used as function and predicate symbols. In this paper and the talk, we will explain how the Theorema user can introduce, interactively, any desired logicographic symbol and how these symbols can then be used for improving the readability and self-explanatory power of mathematical texts without reducing formal rigor. In this paper, we cannot go into any detail about the implementation of logicographic symbols, which is fully explained in [Nakagawa 2001] and, partly, also in [Nakagawa and Buchberger 2001]. Note that the concept of logicographic symbols goes far beyond what is possible even in advanced mathematical text processing systems like TEX, [Knuth 1986a]: Although it is possible in TEX to create arbitrary new symbols by the METAFONT tool, [Knuth 1986b], these symbols have no logical functionality, i.e. their syntax does not follow the rules of predicate logic and neither can we attach any (computational or logical) semantics to such new symbols. In contrast, in the Theorema system, formulae containing logicographic symbols can be executed and, more importantly, can also be processed by automated provers, solvers, and simplifiers. With the new feature of logicographic symbols, we now provide a means for the user to invent arbitrary new symbols that are part of the formal language of Theorema (a version of higher order predicate logic) and, at the same time, also convey the intuitive meaning of the functions and predicates denoted by these symbols. In this paper we describe the essence of the concept of logicographic symbols and their usage by giving just two typical examples. As a credit to early forerunners, we would like to mention the work of Jason Harris, [Harris 1996], who, without having the general concept of logicographic symbols, designed a Mathematica package that allows to create slots for arguments at basically arbitrary positions when using symbols of the existing Mathematica vocabulary. However, for the implementation of our general concept of logicographic symbols, we needed implementation techniques that give more control on the design, shape, arity, and slot positions. The box structure of Mathematica expressions (with the two basic operations MakeExpression and MakeBoxes) turns out to be a very useful and sufficiently flexible platform on top of which our implementation can be built.