************************************************

Jorina

************************************************

(X) George fragen wg. proofs-Men�

(X) Warum werden bei import_test-1.casl nicht alle internen Knoten versteckt?

- Ausgaben (show spec etc.) in eigenes Fenster, mittels htk

(George oder Christoph fragen)

(X) lokale Links anders darstellen (gepunktet?)

\--> Dashed

(X) Knoten sind auch von sich selbst locally reachable

=> bei Global Decomposition immer auch ein lokaler Link

von urspr�nglichem Source zu Target

(X) Kantenmen� zum Anzeigen des Signaturmorphismus (mittels show anzeigen)

(X) (Global) Subsumption optimieren: auch globale Theorem-Links zulassen

dazu muss in DevGraph.hs der Bool-Wert in den Theorem-Links durch

data ThmLinkStatus = Open | Proved [DGLinkLab]

ersetzt werden

Gleichzeitig hier auch noch einen ThmLinkStatus f�r die

Conservativity einsetzen

(default ist Open, z.B. in Static/AnalysisStructured.hs)

LocalThm ThmLinkStatus Conservativity ThmLinkStatus

GlobalThm ThmLinkStatus Conservativity ThmLinkStatus

HidingThm GMorphism ThmLinkStatus

(X) es muss gepr�ft werden, ob die benutzten theorem links solche

sind, die nicht in ihrer DGLinkLab-Liste den aktuell zu beweisenden

Theorem-Link enthalten

- Local Subsumption-Regel ausbauen zu Loc-Decomposition (I+II)

zu einem lokalen Theoremlink alle parallelen "locally reachable" Links (Thm+Def)

Signaturmorphismen d�rfen verschieden sein

Ringbeweis-Check, + sich selbst darf er auch nicht nehmen

pr�fen, ob beide die lokalen Axiome des Startknotens gleich abbilden

Funktion dgn_sens_rekursiv: steigt bei DGRef rekrusiv ab

(�ber dgn_libname und dgn_node in anderer Library nachgucken)

bis DGNode erreicht ist, dann

lokale Axiome mit dgn_sens die lokalen Axiome berechnen

Abbilden der Axiome entlang eines Signaturmorphismus: mit

do

let sens = dgn_sens_rekursiv node

sens1 <- translateG_l_sentence_list mor1 sens

sens2 <- translateG_l_sentence_list mor2 sens

return $ eq_G_l_sentence_set sens1 sens2

Result: siehe Common/Result.hs

Vergleichen: Abbildung des Axiome mit Morphismus1 + Morphismus2

aus resultierenden Listen Mengen machen (Set.fromList aus Common.Lib.set)

+ diese dann vergleichen

genauso optimieren wie Subsumption, d.h. auch Theorem-Links zulassen

(allerdings lokale Links immer nur im 1. Schritt!)

Loc-Decomposition I

Local Inference

Schlie�en der Fenster ohne "Absturz"

Dokumentation

Anzeige von Logik-Graphen