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