=ADD=
=reftype=
14
=number=
99-38
=url=
ftp://ftp.risc.uni-linz.ac.at/pub/techreports/1999/99-38.ps.gz
=year=
1999
=month=
12
=author=
Windsteiger; Wolfgang
=title=
Building up Hierarchical Mathematical Domains Using Functors in Theorema
=abstract=
The world of mathematical domains is
structured hierarchically. There are elementary domains and there are
well-known techniques how to build up new domains from existing
ones. Which of the domains to view as the actual basis of the
hierarchy is the freedom of the mathematician who wants to work
with these domains and it depends of course on the intention of
their use. The strength of the concept lies, however, in the fact
that a new domain is constructed from given domains by
well-defined rules, which {\em do not depend} on the actually
given domains but only rely on {\em certain properties} that hold
{\em in the given domains}, and the construction rules guarantee
{\em certain properties for the new domain} then.

In the {\em Theorema} system, B. Buchberger introduced the concept of
{\em functors} to represent these domain construction rules. A functor
can actually be viewed as a function that produces a new domain
from given domains by {\em describing}, which objects and
operations are available in the new domain, and by {\em defining},
how new objects can be constructed from known objects and how
operations on the new objects can be carried out using known
operations in the underlying domains. Following the general
philosophy of the {\em Theorema} system, functors play a role both
in {\em proving} and in {\em computing}. The domain description
contained in the functor holds structural information, which can be
used by a prover for the new domain in order to find an
appropriate structure of proofs for formulae containing objects of
the new domain. The domain definitions, on the other hand, contain
rules, which can be used by an evaluator for executing computations
involving objects of the new domain.

In the sequel, we will demonstrate the facilities that are provided
in {\em Theorema} to define functors, to build up a hierarchy of
domains using functors, and to do computations in the constructed
domains.
=howpublished=
Proceedings of the CALCULEMUS '99 Workshop, Electronic Notes in Theoretical Computer Science, Elsevier, 1999.
=sponsor=
FWF (Austrian Science Fundation), SFB project P1302
=keywords=
automatic reasoning