todo revision 242691238a8d1a89581751d782af87ec5d7470c0
57221209d11b05aa0373cc3892d5df89ba96ebf9Christian Maeder************************************************
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder************************************************
e6d40133bc9f858308654afb1262b8b483ec5922Till Mossakowski(X) George fragen wg. proofs-Men�
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu(X) Warum werden bei import_test-1.casl nicht alle internen Knoten versteckt?
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder- Ausgaben (show spec etc.) in eigenes Fenster, mittels htk
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder (George oder Christoph fragen)
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder(X) lokale Links anders darstellen (gepunktet?)
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder(X) Knoten sind auch von sich selbst locally reachable
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder => bei Global Decomposition immer auch ein lokaler Link
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder von urspr�nglichem Source zu Target
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder(X) Kantenmen� zum Anzeigen des Signaturmorphismus (mittels show anzeigen)
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder(X) (Global) Subsumption optimieren: auch globale Theorem-Links zulassen
ad270004874ce1d0697fb30d7309f180553bb315Christian Maeder dazu muss in DevGraph.hs der Bool-Wert in den Theorem-Links durch
5e46b572ed576c0494768998b043d9d340594122Till Mossakowski data ThmLinkStatus = Open | Proved [DGLinkLab]
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang ersetzt werden
23a00c966f2aa8da525d7a7c51933c99964426c0Christian Maeder Gleichzeitig hier auch noch einen ThmLinkStatus f�r die
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder Conservativity einsetzen
575a55eadc8dcab8ee350324b417cbd9e52e69c0Christian Maeder (default ist Open, z.B. in Static/AnalysisStructured.hs)
8e9c3881fb6e710b1e08bf5ac8ff9d393df2e74eChristian Maeder LocalThm ThmLinkStatus Conservativity ThmLinkStatus
db453fe9625a9dab5d108f7a5e464598814144b8Jian Chun Wang GlobalThm ThmLinkStatus Conservativity ThmLinkStatus
8c63cd89ef840cd7a3d3b75f0207dc800388c800Christian Maeder HidingThm GMorphism ThmLinkStatus
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder(X) es muss gepr�ft werden, ob die benutzten theorem links solche
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder sind, die nicht in ihrer DGLinkLab-Liste den aktuell zu beweisenden
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski Theorem-Link enthalten
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder- Local Subsumption-Regel ausbauen zu Loc-Decomposition (I+II)
90c174bac60a72ffd81bc3bf5ae2dd9a61943b8bChristian Maeder zu einem lokalen Theoremlink alle parallelen "locally reachable" Links (Thm+Def)
2561b4bfc45d280ee2be8a7870314670e4e682e4Christian Maeder Signaturmorphismen d�rfen verschieden sein
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Ringbeweis-Check, + sich selbst darf er auch nicht nehmen
aea143fff7a50aceb809845fbc42698b0b3f545aChristian Maeder pr�fen, ob beide die lokalen Axiome des Startknotens gleich abbilden
ca020e82eb3567e7bdbb1cf70729efbd07e9caa4Klaus Luettich Funktion dgn_sens_rekursiv: steigt bei DGRef rekrusiv ab
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder (�ber dgn_libname und dgn_node in anderer Library nachgucken)
a001917177db7ae636853b37c0d0f9f4e90a83ffChristian Maeder bis DGNode erreicht ist, dann
58b671de3fe578346fef9642ffa3c5a0a0edb3cbTill Mossakowski lokale Axiome mit dgn_sens die lokalen Axiome berechnen
4b6aa93c12e4db86ccc7694a48a73e9cf7262d06Christian Maeder Abbilden der Axiome entlang eines Signaturmorphismus: mit
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder let sens = dgn_sens_rekursiv node
986d3f255182539098a97ac86da9eeee5b7a72e3Christian Maeder sens1 <- translateG_l_sentence_list mor1 sens
01aafb6a9520f05df5ff467b591ecb5474dcfc86Christian Maeder sens2 <- translateG_l_sentence_list mor2 sens
8e80792f474d154ff11762fac081a422e34f1accChristian Maeder return $ eq_G_l_sentence_set sens1 sens2
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder Vergleichen: Abbildung des Axiome mit Morphismus1 + Morphismus2
9ecf13b5fd914bc7272f1fc17348d7f4a8c77061Christian Maeder aus resultierenden Listen Mengen machen (Set.fromList aus Common.Lib.set)
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder + diese dann vergleichen
03136b84a0c70d877e227444f0875e209506b9e4Christian Maeder genauso optimieren wie Subsumption, d.h. auch Theorem-Links zulassen
16e124196c6b204769042028c74f533509c9b5d3Christian Maeder (allerdings lokale Links immer nur im 1. Schritt!)
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Loc-Decomposition I
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Local Inference
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Schlie�en der Fenster ohne "Absturz"
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Dokumentation
b2026c46f0e4c6a05931f1bf0ab2e84ce884c814Christian Maeder Anzeige von Logik-Graphen