Information Technology Reference
In-Depth Information
TM ForAll[
range[
simpleRange[
var[ x ]] ,
simpleRange[
var[ y ]] ,
simpleRange[
var[
seq[ z ]]]] ,
True ,
TM Iff[is-sorted[ TM Tuple[
var[ x ] ,
var[ y ] ,
var[
seq[ z ]]]] ,
TM And[ TM LessEqual[
var[ x ] ,
var[ y ]] ,
is-sorted[ TM Tuple[
var[ y ] ,
var[
seq[ z ]]]]]]]
Translators exist for translating formulae in the syntax of other systems to
the Theorema syntax and vice versa. A translator to the recent Omdoc [15]
standard is under development.
4
Structured Mathematical Knowledge Bases
We think that future math systems need “external” and “internal” tools for
structuring mathematical knowledge bases.
External tools are tools that partition collections of formulae into sections,
subsections, etc. and maybe, in addition, allow to give key words like 'Theorem',
'Definition' etc. and labels to individual formulae so that one can easily reference
and re-arrange individual formulae and blocks of formulae in large collections of
formulae. Such tools, which we call “label management tools”, are implemented
in the latest version of Theorema, see [23].
In contrast, internal structuring tools consider the structure of mathemati-
cal knowledge bases itself as a mathematical relation, which essentially can be
described by “functors” (or, more generally, “relators”). The essence of this func-
torial approach to structuring mathematical knowledge can be seen in a formula
as simple as
x,y x
x .
x
y
y
y
In this formula, the predicate
is defined in terms of the predicate
.We
may want to express this relation between
explicitly by defining the higher-
order binary predicate AR :
AR [
x .
⇔∀ x,y x
x
y
∼,≤
,
y
]
y
We may turn this “relator” into a “functor” by defining, implicitly,
x .
x,y AR [
x
y
][ x, y ]
y
(In this paper, we do not distinguish the different types of the different variables
occurring in formulae because we do not want to overload the presentation with
technicalities.)
Search WWH ::




Custom Search