Logicographic Symbols: A New Feature in Theorema
Bruno Buchberger
In: Symbolic Computation - New Horizons (Proceedings of the 4th
International Mathematica Symposium, Tokyo Denki University, Chiba
Campus, Japan, June 25-27, 2001), Tokyo Denki University Press, 2001,
pp. 23-30.
(ISBN 4-501-73020-X C3041. Copyright: Tokyo Denki University Press.)
ABSTRACT:
We introduce the concept of logicographic symbols and
describe a first implementation (by the author's PhD student Koji
Nakagawa) in the Theorema system.
Logicographic symbols are two-dimensional symbols (e.g. graphics or
photos) to be used as function or predicate constants in predicate
logic that may be designed freely by the user so that the intuitive
meaning of the symbols can be expressed by their shape. Logicographic
symbols have slots at arbitrary position for the parameters. Logically
and internally in Theorema, logicographic symbols are just ordinary
constants so that text using logicographic symbols is both formal in
the sense of predicate logic and intuitive in the sense of conveying
meaning by the graphical information contained in the external appearance
of the symbols.
Terms and formulae containing logicographic symbols and identifier
constants can be nested to arbitrary depth. In contrast to ordinary
notations of predicate logic that use parantheses for indicating the
nesting of expressions, we introduce two-dimensional colored boxes
for supporting easy readability of nested expressions.
Also, logicographic symbols may have internal structure: For logico-
graphic ymbols composed from smaller constituents one may declare
whether the composed meaning is the conjunction or disjunction of
the meaning of the constituent symbols. Also, parameters of logico-
graphic symbols may be left out with the intention of quantifying
(universally or existentially) over the parameter omitted. These
systematic variation rules for logicographic symbols make it possible
to introduce a huge number of variants of mathematical concepts with
a few basic definitions only.
We demonstrate the usage and practical advantage of logicographic
symbols by the example of the merge sort algorithm and variants of
the notion of function and relation in set theory.