background image

7 Future directions

There are advantages and disadvantages of both untyped (such as Isabelle/ZF) and strongly typed
(such as Isabelle/HOL) logical systems.

In this work I have shown that in untyped systems can be mastered the notion of generalization.
I think that we should invent something having advantages of both untyped and typed systems.

We need a good idea how to crossbred different type systems to provide common advantages.
Defining generalization in ZF seems being a step in this direction.

As a smaller challenge we also should polish my implementation and usage of generalizations

in Isabelle/ZF because my implementation is not ideal.

4

Section 7