Information Technology Reference
In-Depth Information
Functors have a computational and a reasoning aspect. The computational
aspect of functors already received strong attention in the design of programming
languages, see for example [14]: If we know how to compute with
then, given
the above definition of the functor AF , we also know how to compute with the
predicate AF [
].
However, in addition, functors have also a reasoning aspect which so far has
received little attention in reasoning systems: For example, one can easily prove
the following “conservation theorem”:
AR [
] ,
]
is-transitive [
,
∼,≤
]
is-transitive [
where
is-transitive [
z .
⇔∀ x,y,z x
y
]
z
x
y
In other words, if we know that
is in the “category” of transitive predicates
and
is related to
by the relator AR (or the corresponding functor AF )then
also is in the category of transitive predicates. Of course, studying a couple of
other conservation theorems for the relator AR , one soon arrives at the following
conservation theorem
AR [
] ,
]
is-quasi-ordering [
,
∼,≤
]
is-equivalence [
which is the theorem which motivates the consideration of the relator AR .
After some analysis of the propositions proved when building up mathemat-
ical theories, it should be clear that, in various disguises, conservation theorems
make up a considerable portion of the propositions proved in mathematics.
Functors for computation, in an attractive syntax, are available in Theo-
rema, see for example the case study [6]. Some tools for organizing proofs of
conservation theorems in Theorema where implemented in the PhD thesis [24]
but are not integrated into the current version of Theorema. An expanded
version of these tools will be available in the next version of Theorema.
5
Schemes for Invention
Given a (structured) knowledge base K (i.e. a structured collection of formulae
on a couple of notions expressed by predicates and functions), in one step of
the theory exploration process, progress can be made in one of the following
directions:
-
invention of notions (i.e. axioms or definitions for new functions or predi-
cates),
-
invention and verification of propositions about notions,
-
invention of problems involving notions,
-
invention and verification of methods (algorithms) for solving problems.
Search WWH ::




Custom Search