Mechanisms identifying, implying or interpreting theorems between intuitively "similar" notions should be discussed in general.
As of the current Mizar, I would include among them the ClusterImplementation, TypeImplementation? and the RedefinitionMechanism?.
However more is probably needed to avoid frequent painful reconsidering in more advanced theories, when different aspects of the discussed mathematical objects have to be used (there are many examples of this, I just wrote RelationsAndGraphs).
Additionally, we probably do not want to sacrifice the clean set-theoretical semantics of Mizar, to solve this (e.g. as in IMPS) by various InterpretatonTheories?.
-- JosefUrban - 18 Jul 2002
| WebForm | |
|---|---|
| TopicClassification | FeatureBrainstorming |
| ProjectGroup? | |
| ImplementationDate? | N/A |
Edit | Attach | Print version | History: r1 | Backlinks | Raw View | Raw edit | More topic actions
Topic revision: r1 - 2002-07-18 - 11:33:13 - JosefUrban
 |
|
Copyright © by the contributing authors. All material on this collaboration platform is the property of the contributing authors. Ideas, requests, problems regarding TWiki? Send feedback