Information Technology Reference
In-Depth Information
1
2
is-sorted
[
≤
2
,
2
,
5
,
7
]
,
etc.
(The extension of predicate logic by sequence variable is practically useful
because it allows the elegant formulation of pattern matching programs. For
example, the formula
p
[
v, w, x, w, y
]=1saysthat
p
yields 1 if two arguments are
identical. The meta-mathematical implications of introducing sequence variables
in predicate logic are treated in [16].)
Hence, Theorema has the possibility of formulating and executing any
mathematical algorithm within the same logic frame in which the correctness
of these algorithms and any other mathematical theorem can be proved. In ad-
dition, Theorema has a possibility to invoke any algorithm from the underlying
Mathematica algorithm library as a black box so that, if one wants, the en-
tire functionality of Mathematica can be taken over into the logic frame of
Theorema.
3
Attractive Syntax
Of course, the internal syntax of mathematical formulae on which algorithmic
reasoners may be based, theoretically, is not a big issue. Correspondingly, in
logic books, syntax is kept minimal. As a means for human thinking and ex-
pressing ideas, however, syntax plays an enormous role. Improving syntax for
the formulae appearing in the input and the output of algorithmic reasoners and
in mathematical knowledge bases is an important practical means for making
future math systems more attractive for working mathematicians. Most of the
current reasoning systems, in the past few years, started to add functionalities
that allow to use richer syntax.
The Theorema system put a particular emphasis on syntax right from
the beginning, see the papers on Theorema on the home page of the project
http://www.theorema.org/
. We allow two-dimensional syntax and user-prog-
ramming of syntax, nested presentation of proofs, automated generation of nat-
ural language explanatory text in automated proofs, hyperlinks in proofs etc. In
recent experiments, we even provided tools for graphical syntax, called ”logico-
graphic” syntax, see [19]. The implementation of these feature was made com-
paratively easy by the tools available in the front-end of Mathematica which
is the programming environment for Theorema. Of course, whatever syntax is
programmed by the user, the formulae in the external syntax is then translated
into the internal standard form, which is a nested Mathematica expression,
used as the input format of all the Theorema reasoners. For example,
is-sorted
[
x
y
is-sorted
[
≤
∀
x,y,z
x, y, z
]
⇔
y, z
]
internally is the nested prefix expression:
Search WWH ::
Custom Search