todo revision ead55e5013b301de3b72a254a9fb347ae04ba0a4
5d92fff82718cd018f0b61a10b9ad4d2b8064c95rpluemPlan and priority list for CoFI tool activities
9c67ffea79ab184351b5d554b57814e13285e758jim************************************************
33e53d7c6aa5d004d96ea11d7f3ca35b30e82544trawick************************************************
33e53d7c6aa5d004d96ea11d7f3ca35b30e82544trawickSuchfunktion f�r einen Knoten im DG:
20e0c71be778348516719e1e58a9f55c8e78c570trawick welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
027f7b141f164258b254c38319d06452b25d7660trawick erstmal auf eine Logik (z.B. CASL) beschr�nken
027f7b141f164258b254c38319d06452b25d7660trawick - Funktion f�r Morphismus-Suche zwischen Theorien
977c4527be5a21182f24fc22a40a79d576a52f86trawick - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
977c4527be5a21182f24fc22a40a79d576a52f86trawick RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
977c4527be5a21182f24fc22a40a79d576a52f86trawick - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
7fef9f66804ea10d5bf343cdd3d607465e8340cajimBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
7fef9f66804ea10d5bf343cdd3d607465e8340cajimKonfidenzgrade von Beweisen?
3770ed746d69c7a4111cba9966169bd5d7a509a6poiriervon Till/HiWi zu erledigen:
3770ed746d69c7a4111cba9966169bd5d7a509a6poirierRepr�sentation �ndern:
3770ed746d69c7a4111cba9966169bd5d7a509a6poirier Beweisobjekte an DGs, nicht an Regeln -- done
3770ed746d69c7a4111cba9966169bd5d7a509a6poirier F�r Theoreme in Theorien an Beweisobjekte -- done
7bd92b29516bc4bf7351d35aa447dbe68f1e8bb4jorton BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
7bd92b29516bc4bf7351d35aa447dbe68f1e8bb4jorton Definitionen auszeichnen -- done
7bd92b29516bc4bf7351d35aa447dbe68f1e8bb4jorton F�r alles siehe G_theory, ThSens und SenStatus.
a81c0c1ae464b2063a21b45f80c9da8d89bb840ecovener Isabelles Beweisobjekte einbinden
ffae06377667a5d8f9699ac7512134de7000a83dminfrin************************************************
ffae06377667a5d8f9699ac7512134de7000a83dminfrinRazvan (Till)
ffae06377667a5d8f9699ac7512134de7000a83dminfrin************************************************
efc81fe729a2b7401028387da184b4a98f0b854atrawickIntegration with PGIP
efc81fe729a2b7401028387da184b4a98f0b854atrawick Hets needs to be equipped with a command-line interface that reads in
efc81fe729a2b7401028387da184b4a98f0b854atrawick specification libraries and proof commands
efc81fe729a2b7401028387da184b4a98f0b854atrawick Proof commands are special annotations in the libraries
9c67ffea79ab184351b5d554b57814e13285e758jim All menu commands of the development graph interface (GUI/...) should become (proof) commands
8f066564bfc0fd6ddc6ca4b2f2410615554597d1jim when stepping through the specs, dg calculus generates proof obligations
8f066564bfc0fd6ddc6ca4b2f2410615554597d1jim (for the current dg node only),
4acc1efe19ac2e6f2df0abb4d5bf99bd8ae3c5c6jim which then can be discharged by Isabelle, SPASS etc.
4acc1efe19ac2e6f2df0abb4d5bf99bd8ae3c5c6jim That is, the proof commands always occur at the position in the text
4acc1efe19ac2e6f2df0abb4d5bf99bd8ae3c5c6jim that generates the dg node?!? or should they occur after each specification?
29ecbd9db1622e74964264d078336f7604d65093jim needs incremental parsing and static analysis for Hets libraries
29ecbd9db1622e74964264d078336f7604d65093jim easy: parse and analyse one specification at a time, and then process it with proof commands
29ecbd9db1622e74964264d078336f7604d65093jim more challenging: incrementally parse and analyse also individual specifications
a503caacf7ab36d5bc42cb7c78256e1221642656jim************************************************
da40dfabefd6f8eb8450e9a097c594ee2ab13e3eminfrinAnton (Till)
da40dfabefd6f8eb8450e9a097c594ee2ab13e3eminfrin************************************************
da40dfabefd6f8eb8450e9a097c594ee2ab13e3eminfrinModal-CASL <-> CASL-DL
59d316b83d42d2a07e25c20d8c35a07b369618bdsf see Chapter 4 of "The Description Logic Handbook"
59d316b83d42d2a07e25c20d8c35a07b369618bdsf and ask Klaus for a print out of it
59d316b83d42d2a07e25c20d8c35a07b369618bdsfimprove Modal-CASL
8602c898d4e06a7e7b9d6b7cf4b172a8e7310987sf possibly also modal logic in CoCASL
8602c898d4e06a7e7b9d6b7cf4b172a8e7310987sf**************** task A ************************
8602c898d4e06a7e7b9d6b7cf4b172a8e7310987sfProofs with Isabelle and SPASS
4acc1efe19ac2e6f2df0abb4d5bf99bd8ae3c5c6jimCASL basic datatypes
4acc1efe19ac2e6f2df0abb4d5bf99bd8ae3c5c6jimHasCASL examples
4acc1efe19ac2e6f2df0abb4d5bf99bd8ae3c5c6jim- improve simplifier for partiality in Isabelle coding
4acc1efe19ac2e6f2df0abb4d5bf99bd8ae3c5c6jim program interaction between solver, subgoaler and simplifier in such a way
4acc1efe19ac2e6f2df0abb4d5bf99bd8ae3c5c6jim that proofs of definedness conditions are postponed
3e2582713ed6883683272fbc628a27419d0ed543minfrin************************************************
2c132b1e3610da2fb9e6b3594a313efa3ff29e22minfrinFlorian (Till)
2c132b1e3610da2fb9e6b3594a313efa3ff29e22minfrin************************************************
a46801e6532423aa7bd184471eb49158d7c9ae62sfModelchecker f�r algebraische Eigenschaften
a46801e6532423aa7bd184471eb49158d7c9ae62sf neue Hets-Option daf�r (Christian Maeder fragen)
a46801e6532423aa7bd184471eb49158d7c9ae62sf hets -n NonAssocRelationAlgebra --model datei.lisp Calculi/Algebra/RelationAlgebra.casl
808a26d70f28498b9d7252a70d9fb23def781901minfrin Datenstruktur zerlegen, siehe
808a26d70f28498b9d7252a70d9fb23def781901minfrin http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/debugging_e.htm
6f9bf764bc79571d1da19dfbbd78527fca278a8eminfrin Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:
6f9bf764bc79571d1da19dfbbd78527fca278a8eminfrin Allquantoren --> all, Existenzquantor --> any
6f9bf764bc79571d1da19dfbbd78527fca278a8eminfrin CASL-Junktoren --> Haskell-Junktoren
6f9bf764bc79571d1da19dfbbd78527fca278a8eminfrin Terme rekursiv auswerten, Operationen aus der Table nehmen
e63e8b4b886d2144fed7946d0fbe8d27386be2dcjortonAufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken
e63e8b4b886d2144fed7946d0fbe8d27386be2dcjorton - ggf. Server nutzen
e63e8b4b886d2144fed7946d0fbe8d27386be2dcjorton - Vorverarbeitung f�r Solver (z.B. Duplikate raus)
223c64b836fbc2bc8611da9604379dfe13f56abasf - Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)
223c64b836fbc2bc8611da9604379dfe13f56abasfApplikation1 ---
bf507cc1e6ad55303c3d436c6ca153f46c788be6sf | | -- Freibuger Solver
bf507cc1e6ad55303c3d436c6ca153f46c788be6sf XML --- |---- Franz�sischer Solver
bf507cc1e6ad55303c3d436c6ca153f46c788be6sf | |-- Hets -- Bremer Solver
bf507cc1e6ad55303c3d436c6ca153f46c788be6sfApplikation2 ----- |
93cf7fc650197b941ae31a7c7e51e901b129e954igalic ConstraintCASL
93cf7fc650197b941ae31a7c7e51e901b129e954igalic Semantische Modelle/Korrektheit (CASL, HAsCASL)
a1b1c78faf7969affb320f5c8eb270ffa21314c4rjungXML-Einlesen in Haskell:
a1b1c78faf7969affb320f5c8eb270ffa21314c4rjungHXT (siehe OMDoc.XmlHandling): kann Namespaces
a2558ec3af4391b7da7fe61e1e53383bbd0174b9jorton(HaXML: kann Haskell-Datenypen in DTDs umwandeln)
a2558ec3af4391b7da7fe61e1e53383bbd0174b9jortonOutline der Diplomarbeit
a2558ec3af4391b7da7fe61e1e53383bbd0174b9jorton Qualitative Constraint-Kalk�le (siehe Thomas)
8d6b3720340d0bd7f8d25e2a8563527e97a48df8jorton CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:
8d6b3720340d0bd7f8d25e2a8563527e97a48df8jorton the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)
8d6b3720340d0bd7f8d25e2a8563527e97a48df8jorton CASL-Formeln nur ganz kurz
8d6b3720340d0bd7f8d25e2a8563527e97a48df8jorton ConstraintCASL
48e4b65042d94992c50f1db6c0b0cdbd99ca77e8sf Signaturen, Signaturmorphismen (aus CASL)
48e4b65042d94992c50f1db6c0b0cdbd99ca77e8sf Modelle (aus CASL)
48e4b65042d94992c50f1db6c0b0cdbd99ca77e8sf Erf�lltheit von Formeln
48e4b65042d94992c50f1db6c0b0cdbd99ca77e8sf optional: Erf�lltheitsbedingung
48e4b65042d94992c50f1db6c0b0cdbd99ca77e8sf M |= sigma(phi) <=> M|_sigma |= phi
47ae8ca3c79d279b2e5424d6b8cf5e4e61ea968fjim f�r Signaturmorphismus sigma:Sigma_1->Sigma_2
47ae8ca3c79d279b2e5424d6b8cf5e4e61ea968fjim M \in Mod(Sigma_2), phi\in Sen(Sigma_1)
47ae8ca3c79d279b2e5424d6b8cf5e4e61ea968fjim Formalisierung von Kalk�len in ConstraintCASL
47ae8ca3c79d279b2e5424d6b8cf5e4e61ea968fjim Constraint-Solver (auch in ihren Eigenheiten)
47ae8ca3c79d279b2e5424d6b8cf5e4e61ea968fjim �bersetzungen zwischen den verschieden Formaten
397df70abe0bdd78a84fb6c38c02641bcfeadceasf praktischer Vergleich
397df70abe0bdd78a84fb6c38c02641bcfeadceasf�bersetzungen bis 30.Juni
9b5fe1d4ec48643fb819bbce9dc80f93f444fb48sf ConstraintCASL -> Bremer Solver
9b5fe1d4ec48643fb819bbce9dc80f93f444fb48sf Bremer Solver -> ConstraintCASL
dd9f60fdfeb73f829fe0b260b7975b4b22be0838sf Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers
dd9f60fdfeb73f829fe0b260b7975b4b22be0838sf parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt
dd9f60fdfeb73f829fe0b260b7975b4b22be0838sf Das kann das als Option in Hets eingebunden werden (Christian Maeder)
135e1d6a301398168e3b2e5125508828591e1673niqFreiburger Constraint-Solver angucken im Juli
135e1d6a301398168e3b2e5125508828591e1673niq�bersetzungen bis 31. Juli
135e1d6a301398168e3b2e5125508828591e1673niq ConstraintCASL -> Freibuger Solver/XML-Format
135e1d6a301398168e3b2e5125508828591e1673niq Freibuger Solver/XML-Format -> ConstraintCASL
c7de70e936ac1e36c25676fe62e65dbacb947619minfrin************************************************
c7de70e936ac1e36c25676fe62e65dbacb947619minfrinHendrik (Till)
c7de70e936ac1e36c25676fe62e65dbacb947619minfrin************************************************
c7de70e936ac1e36c25676fe62e65dbacb947619minfrinwerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der
c7de70e936ac1e36c25676fe62e65dbacb947619minfrin sie als erstes eingef�hrt wurden?
c7de70e936ac1e36c25676fe62e65dbacb947619minfrin checken f�r Library-Importe
1b1621900bd89ddc496d721c865a726f635ebd7esfOMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden
1b1621900bd89ddc496d721c865a726f635ebd7esfHiding: unterschiedlich in OMDoc und Hets
1b1621900bd89ddc496d721c865a726f635ebd7esfein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als
4203a35c28d7c60adb7e9ef3be87aad34951c79asf Signaturmorphismus
4203a35c28d7c60adb7e9ef3be87aad34951c79asf wird �bersetzt in einen OMDoc-Theoriemorphismus
4203a35c28d7c60adb7e9ef3be87aad34951c79asf mit leerer/identischer Abbildung, bei dem die Symbole aus
c094add0a23fe1120fd33711ba2e2d084f5629a1sf Sigma_2 \ Sigma_1 versteckt werden
c094add0a23fe1120fd33711ba2e2d084f5629a1sf Wenn der Signaturmorphismus keine Inklusion ist, ist keine
c094add0a23fe1120fd33711ba2e2d084f5629a1sf �bersetzung m�glich -> Fehler
12b26f433fd7d6fc9f76413d7c2cabf4fa5cb300sfein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist
12b26f433fd7d6fc9f76413d7c2cabf4fa5cb300sf (also leere bzw. identische Abbildung) wird �bersetzt
12b26f433fd7d6fc9f76413d7c2cabf4fa5cb300sf in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus
26f56d4a3c12077d605362e97490e34522fa4814covener falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss
26f56d4a3c12077d605362e97490e34522fa4814covener ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,
26f56d4a3c12077d605362e97490e34522fa4814covener der dann die Umbenennung macht, erzeugt werden
2cef7e294acb5d8b8b5dcb21a55438da0b73f63figalicLogiken: �ber verschiedene OMDoc-Theorien mit URI
2d2de64c25c1519122a76150a7daf2c05f53fd9asf************************************************
2d2de64c25c1519122a76150a7daf2c05f53fd9asfMingyi (Till)
27c5ebb7d411a214f5b6b55a881086ce086d3dd3covener************************************************
27c5ebb7d411a214f5b6b55a881086ce086d3dd3covenerDiplomarbeit
27c5ebb7d411a214f5b6b55a881086ce086d3dd3covener- CASL-Logik: "Relating CASL with other specification languages", S.401-408
7697b1b7376a532163c621e050b70c90dcb15d66covener- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz
7697b1b7376a532163c621e050b70c90dcb15d66covener siehe CASL reference manual (suche nach conservative)
7697b1b7376a532163c621e050b70c90dcb15d66covener- warum sind konservative Erweiterungen wichtig?
7697b1b7376a532163c621e050b70c90dcb15d66covener - um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert
7697b1b7376a532163c621e050b70c90dcb15d66covener werden k�nnen
9e0536cd66a389bdaa758a825b8bbd8fea665a3eigalic - f�r Refinement-Beweise
9e0536cd66a389bdaa758a825b8bbd8fea665a3eigalic- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,
9e0536cd66a389bdaa758a825b8bbd8fea665a3eigalic definitional oder monomorph sind
862bbb262644e8aefae1bf352552b01908ecae0eminfrin - Beschreibung des Algorithmus in Pseudocode
862bbb262644e8aefae1bf352552b01908ecae0eminfrin - Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus
862bbb262644e8aefae1bf352552b01908ecae0eminfrin als konservativ erkennt, muss f�r jedes Modell der kleineren
dd3b88790af9d18429c732ca7bc83ec4ef43d3ffrpluem Spezifikation eine Modellerweiterung zur gr��eren Spezifikation
dd3b88790af9d18429c732ca7bc83ec4ef43d3ffrpluem gefunden werden. Z.B. im Falle von free types kann dies eine
dd3b88790af9d18429c732ca7bc83ec4ef43d3ffrpluem Termalgebra-Konstruktion sein.
5bbabc874e3fcfbea08c199f7a79ee05b4817a70sf SP1 -- \sigma --> SP2
5bbabc874e3fcfbea08c199f7a79ee05b4817a70sf konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem
5bbabc874e3fcfbea08c199f7a79ee05b4817a70sf SP2-Modell M2 mit M2|_\sigma=M1.
aec9747aa70c1dce98e536e8eef5a6a0ab0f1d6cjimport CCC to Haskell
7b7e8ba34e262064914ceedacd5f7d9201b6575ccovenerFunktionen imageOfMorphism und inhabited
7b7e8ba34e262064914ceedacd5f7d9201b6575ccovener von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
7b7e8ba34e262064914ceedacd5f7d9201b6575ccovener mit "cvs add SigFuns.hs" einchecken
220bc4233b21982d7c51842a1774db0ba6172ca4covener"free datatypes and recursive equations are consistent"
6f2fbf354b34981f398cf0313aa44702ea2a7066covenercheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
6f2fbf354b34981f398cf0313aa44702ea2a7066covenerJust True => Yes, is consistent
6f2fbf354b34981f398cf0313aa44702ea2a7066covenerJust False => No, is inconsistent
9e7c7a8fa19c33d1e90f8f7ffab69beacbe72566covenerNothing => don't know
9e7c7a8fa19c33d1e90f8f7ffab69beacbe72566covenercall the symbols in the image of the signature morphism "new"
a961006b347d6527ccaeab9cf019a4e68d26bfb0covener- each new sort must be a free type,
a961006b347d6527ccaeab9cf019a4e68d26bfb0covener i.e. it must occur in a sort generation constraint that is marked as free
a961006b347d6527ccaeab9cf019a4e68d26bfb0covener (Sort_gen_ax constrs True)
e3f43882b4f7ac7d1aa679be4b319cca04fd22eecovener such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
e3f43882b4f7ac7d1aa679be4b319cca04fd22eecovener if not, output "don't know"
e3f43882b4f7ac7d1aa679be4b319cca04fd22eecovener and there must be one term of that sort (inhabited)
e3f43882b4f7ac7d1aa679be4b319cca04fd22eecovener if not, output "no"
8dea7832dea3789fe0b90c434c284bcaad96d40fcovener- group the axioms according to their leading operation/predicate symbol,
8dea7832dea3789fe0b90c434c284bcaad96d40fcovener i.e. the f resp. the p in
999661242470e4dc0258982d5f183efc2d157ae7covener forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
0bfcc4d046f6735af2f15981fb53e4c0680b4731covener forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
b761a57b4e63006c287823270876ab40d3212160covener Implication Application Strong_equation
b761a57b4e63006c287823270876ab40d3212160covener forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
b761a57b4e63006c287823270876ab40d3212160covener forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
b761a57b4e63006c287823270876ab40d3212160covener Implication Predication Equivalence
5d92fff82718cd018f0b61a10b9ad4d2b8064c95rpluem if there are axioms not being of this form, output "don't know"
01195d035ccef88e72009e9607157d5eddcb6b7drjungcheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
aec9747aa70c1dce98e536e8eef5a6a0ab0f1d6cjimcheck' [] = ([([],[])],emptyUniqSet)
84fbf855118f318dd5e511d8e5b902cecc1177c0jim-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
0ed19acadd3d3dd593759173d87d2243e97914e2sfcheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
0ed19acadd3d3dd593759173d87d2243e97914e2sf | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
0ed19acadd3d3dd593759173d87d2243e97914e2sf-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
041b426f9b15072b59a32f132e6d04173ab3df68covenercheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
041b426f9b15072b59a32f132e6d04173ab3df68covener | all_vars ps = (pats, addOneToUniqSet indexs n)
cb838cc4d5fd559efd6c0579a0fcb8f6e5a7af22minfrin (pats,indexs) = check' rs
cb838cc4d5fd559efd6c0579a0fcb8f6e5a7af22minfrin-- falls ein Konstruktor dabei ist: split_by_constructor
cb838cc4d5fd559efd6c0579a0fcb8f6e5a7af22minfrin-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
15ff8c621815e8337abc10638f2b2853ee6fd076minfrincheck' qs@((EqnInfo n ctx ps result):_)
15ff8c621815e8337abc10638f2b2853ee6fd076minfrin | all_vars ps = ([], unitUniqSet n)
15ff8c621815e8337abc10638f2b2853ee6fd076minfrin | constructors = split_by_constructor qs
21ccb6cd9272c9066a8f5bb3e7785f46115289desf | only_vars = first_column_only_vars qs
21ccb6cd9272c9066a8f5bb3e7785f46115289desf | otherwise = panic "Check.check': Not implemented :-("
b0ac1e83f8582a9b5a72bff798ffb31a419c8adesf -- Note: RecPats will have been simplified to ConPats
b0ac1e83f8582a9b5a72bff798ffb31a419c8adesf -- at this stage.
b0ac1e83f8582a9b5a72bff798ffb31a419c8adesf constructors = or (map is_con qs)
b682e60dd82772dba52ba77138e494f15c00a551trawick only_vars = and (map is_var qs)
b682e60dd82772dba52ba77138e494f15c00a551trawicksubsort definitions: are conservative if formula is satisfiable
b682e60dd82772dba52ba77138e494f15c00a551trawick (generate proof obligation)
79c754eb51681c3389cd966753e902c429f78939trawick************************************************
79c754eb51681c3389cd966753e902c429f78939trawickHeng (Klaus)
79c754eb51681c3389cd966753e902c429f78939trawick************************************************
8651de219ec5f595af20afdc9da41ce72aaa50d5minfrinOWL-DL logic
8651de219ec5f595af20afdc9da41ce72aaa50d5minfrinOWL-DL (<)-> CASL-DL
8fae12696bce44be9ce4c56888690cad8ac7b8f9sfemacs mode:
8fae12696bce44be9ce4c56888690cad8ac7b8f9sf highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
8fae12696bce44be9ce4c56888690cad8ac7b8f9sf some operation symbols
8fae12696bce44be9ce4c56888690cad8ac7b8f9sf show hets output immediately
8fae12696bce44be9ce4c56888690cad8ac7b8f9sf C-c C-g for hets -g
8fae12696bce44be9ce4c56888690cad8ac7b8f9sf when hets terminates abnormally (e.g. with a fail), emacs loops
d5612bd28e194390b2c74fcf712d564b0e002684sf C-n jumps to the next error, but the message windows is not always scrolled
d5612bd28e194390b2c74fcf712d564b0e002684sf in such a way that the error is at the top (for long error lists)
d5612bd28e194390b2c74fcf712d564b0e002684sf Version for XEamcs?
4ea161d94782fa56f4b36d496f35ff8577c43065covener should work with parser error messages as well (adapt these?)
b588214d6e6fe09abe709e83e894921fbc7e25c8covener************************************************
b588214d6e6fe09abe709e83e894921fbc7e25c8covener************************************************
c64fc4e9830bb1ffdc3491aef5ed3be5b90c466bcovenerlook at command line interface (just call hets)
c64fc4e9830bb1ffdc3491aef5ed3be5b90c466bcovenerimplement simplified rule Theorem-Hide-Shift
ae5efbbf49a7ca6d233209a4d011550989e22556covenertry out examples
8c2bb916633b1eb3dccf91c776363bbc3a6145decovenerconservativity calculus
8c2bb916633b1eb3dccf91c776363bbc3a6145decovenerweakly amalgamable cocones
8c2bb916633b1eb3dccf91c776363bbc3a6145decovenerdevelopment graph calculus
503bec4c591d28ac6cec7182294cdef2ec6a9829covener(see Sect. IV:4.4 of the CASL Reference Manual)
503bec4c591d28ac6cec7182294cdef2ec6a9829covenerlook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs
c00149c3cb27e0381362d07ccf2143574b4f600dsftest command line interface (just call hets)
766b0a4793197ccef3dfa202d1fee1e1f929ffa7sftest development graph GUI:
766b0a4793197ccef3dfa202d1fee1e1f929ffa7sf global decomposition
766b0a4793197ccef3dfa202d1fee1e1f929ffa7sf menu edit - unnamed nodes - hide/show nodes,
97b692bfc8673c8858f03498f81a993ac0c04c01sf node menu: show just subtree / undo
97b692bfc8673c8858f03498f81a993ac0c04c01sf interaction with edit - proofs - automatic?
97b692bfc8673c8858f03498f81a993ac0c04c01sf use update of uDrawGraph-nodes,edges instead of erasing and adding nodes
5e6cf205d2b0c848e15c65dab9711805395a5108minfrin for attribute changes like color
5e6cf205d2b0c848e15c65dab9711805395a5108minfrinprofiling for "automatic" (look at www.haskell.org/ghc)
df419be6d7d4b68823efa05722375552af49c2b6minfrinrestrict proofs: only one prove window per node at a given time
c03e31374e50a227cb554a0f1d4a9056ce80d99asf************************************************
c03e31374e50a227cb554a0f1d4a9056ce80d99asffurther task 1
c03e31374e50a227cb554a0f1d4a9056ce80d99asf************************************************
40b22d3b20454959fe51fdc89907908d77701078minfrin************************************************
b4a00883f358625923365ca1560c96edec172a52sffurther task 2
b4a00883f358625923365ca1560c96edec172a52sf************************************************
b4a00883f358625923365ca1560c96edec172a52sfUni-Refactoring,
0553e62d75ef12d9a6646bb874be1fbf9e4c1dfbsfmake modules hierarchical, change scoped type variables for ghc-6.5
0553e62d75ef12d9a6646bb874be1fbf9e4c1dfbsf(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),
87af9ffc3a42633fe12e11a0ff77bc099ecdca82sfuse HaXml as a cabalized library, provide uni as (one?) cabal
f58bb3da705eb7ec926f4883597fc2eb1336a360minfrinpackage(s), uni used to work under windows as well, watch the
f58bb3da705eb7ec926f4883597fc2eb1336a360minfrini.e. FilePath, Process discussions (libraries@haskell.org)
f58bb3da705eb7ec926f4883597fc2eb1336a360minfrinpossibly switch to a subversion repository, talk to Achim
f58bb3da705eb7ec926f4883597fc2eb1336a360minfrin(amahnke@tzi.de)
be192cefa381d5bae6868034687471754cb43175sf************************************************
be192cefa381d5bae6868034687471754cb43175sffurther task 3
be192cefa381d5bae6868034687471754cb43175sf************************************************
f4a0825e91eec135b5e41c697439e9a13014fa2cminfrinchange management
5876f43a746f688a32b7201bced8591ddf19bd43minfrin reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)
5876f43a746f688a32b7201bced8591ddf19bd43minfrin reload macht folgendes:
5876f43a746f688a32b7201bced8591ddf19bd43minfrin lade CASL-Datei neu ==> neuer Entwicklungsgraph
5876f43a746f688a32b7201bced8591ddf19bd43minfrin vergleiche alten+neuen Entwicklungsgraph, konstruiere eine
bbba414c5bbf770e505778265bbe7a4a0e4fbdaaniq Abbildung (Common/Lib/Map.hs) von alt nach neu
bbba414c5bbf770e505778265bbe7a4a0e4fbdaaniq (jeweils eine Abblidung f�r Knoten und eine f�r Kanten)
bbba414c5bbf770e505778265bbe7a4a0e4fbdaaniq Kriterien f�r Finden der Knotenabbildung:
4aef34911af88f96c5b6d9b71a550a5a97bbc0b6minfrineinfaches Merge von lokalen Beweisen eines abgespeichteren DG
4cefc38158672f5de8119886d9754cf0609a9371minfrin in aktuellen DG
4cefc38158672f5de8119886d9754cf0609a9371minfrin************************************************
4cefc38158672f5de8119886d9754cf0609a9371minfrinfurther task 4
4cefc38158672f5de8119886d9754cf0609a9371minfrin************************************************
11d3c510dca5b5178ad4739ffc1567ef2155bda9minfringraph of Haskell module dependencies
11d3c510dca5b5178ad4739ffc1567ef2155bda9minfrin using .import files
d974a1624c0bb4f1c2e8b36fcf8ba1f12284ed8dsf************************************************
d974a1624c0bb4f1c2e8b36fcf8ba1f12284ed8dsffurther task 5
1a8c329935111a5059363efe927d631371b78414minfrin************************************************
fac37c9794a18c24d187f4e0f97a9476c4344118minfrinport hets to windows. -- costs too much energy at this stage! Till
fac37c9794a18c24d187f4e0f97a9476c4344118minfrinIf hets should become successful then requests for support under
fc58f0ff708564b67cd578c626b6500d1cd63a51sfwindows will surely follow.
fc58f0ff708564b67cd578c626b6500d1cd63a51sfGhc, uni and uDrawGraph should work under windows. Only Isabelle does
fc58f0ff708564b67cd578c626b6500d1cd63a51sfnot exist for windows, but SPASS does. Probably only a few path
fc58f0ff708564b67cd578c626b6500d1cd63a51sfcomputations need to be adapted (made modular) within hets. Also
fc58f0ff708564b67cd578c626b6500d1cd63a51sfposition computations (of Parsec) should be checked under windows.
4e5fe1d203ddf3956a77be3c797c01fd4be8b211sf************************************************
4e5fe1d203ddf3956a77be3c797c01fd4be8b211sffurther task 6
dcb4802d9ea9fc4ba89671e8f8faa70c9535b202minfrin************************************************
dcb4802d9ea9fc4ba89671e8f8faa70c9535b202minfrinrefactor pretty printing
dcb4802d9ea9fc4ba89671e8f8faa70c9535b202minfrineine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
ce4dc40a4e87991087488f70d96d3447d7557294sfund andere Formate besser zu unterst�tzen und einheitlichen PP code
ce4dc40a4e87991087488f70d96d3447d7557294sf(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)
0119f1301a880cf39c0aad0fa2a77240af964691sfDatentypen (particularly for HasCASL data types) zu bekommen.
9db0b0ee6ffade769db57b37a06b3f4849b5d367minfrinLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
9db0b0ee6ffade769db57b37a06b3f4849b5d367minfrin************************************************
9db0b0ee6ffade769db57b37a06b3f4849b5d367minfrinremaining stuff
033d82412cc4af9d939b7e1645425b9e7f4ebf60minfrin************************************************
033d82412cc4af9d939b7e1645425b9e7f4ebf60minfrinset up a ticket and tracking systems (for bugs and features) instead
033d82412cc4af9d939b7e1645425b9e7f4ebf60minfrinof this messy todo list
033d82412cc4af9d939b7e1645425b9e7f4ebf60minfrin--> sourceforge???
1b390add6886fb1c0acdea82be0ef0920f1158casfrefactoring of dgraphs: add unique tags + hashes (but no table)
1b390add6886fb1c0acdea82be0ef0920f1158casf how to compare complex datastructures:
5fd471ec540a088d143a223096d35661bf87c15btrawick tag x1==tag x2 || (hash x1==hash x2 && x1==x2)
5fd471ec540a088d143a223096d35661bf87c15btrawickdisplay library graph
f2472b79d241967fa28f8284470b1c5cafee7b12wroweunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs
f2472b79d241967fa28f8284470b1c5cafee7b12wrowe(make it really abstract), possibly contact amahnke@tzi.de regarding
f2472b79d241967fa28f8284470b1c5cafee7b12wroweTaxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
c9201c790435060b1322d86949183085ca5f6c0cwroweset up default simplifier
c9201c790435060b1322d86949183085ca5f6c0cwroweset up default tactics using axioms
c9201c790435060b1322d86949183085ca5f6c0cwrowe (see DOLCE sample files)
38bd9dba7627c6b2f331cd0731c272ee6bd876b1wroweimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
38bd9dba7627c6b2f331cd0731c272ee6bd876b1wrowe************************************************
c1ba97f41a4526d84fb7a1596afe3dd11e065a2cminfrin************************************************
c1ba97f41a4526d84fb7a1596afe3dd11e065a2cminfringenerate infrastructure for circular coinduction
c1ba97f41a4526d84fb7a1596afe3dd11e065a2cminfrinCCS example: commutativity of || by coinduction
97cc46935ec496b83fef9d6feb094d706c895b3bsf************************************************
4ed33a14c26d78bbe6bd0b9d5091cdb184e348basf************************************************
97cc46935ec496b83fef9d6feb094d706c895b3bsfIsabelle coding
72e3829dbd019a63b1091987fc6e7b1c028b089cminfrin- improve display syntax in HasCASL-Isabelle coding
72e3829dbd019a63b1091987fc6e7b1c028b089cminfrin- identifiers in mixfix templates must be excluded as ordinary
72e3829dbd019a63b1091987fc6e7b1c028b089cminfrinidentifiers (i.e. as quantified variables)
1081aff66582e2cac722fb3b6f09da4f524b5962minfrinmore abstract datatypes?
9f0c32ae318f33c93a47d83f4709242c18339bbcminfrincollect the patches for programatica (or create a package)
9f0c32ae318f33c93a47d83f4709242c18339bbcminfrin- conv (SN i p) = PN i (S p)
9f0c32ae318f33c93a47d83f4709242c18339bbcminfrin+ conv (SN i p) = PN i (Sn (show i) p)
9474e446514b06765775eb0c1ec6645e2c5e50f6minfrinfixes translation error of Pair
9474e446514b06765775eb0c1ec6645e2c5e50f6minfrinsimplification of HasCASL sentences (omit types)
b7557ab9828d2017224a12968f82c3118b6a8c0aminfrinLogic COL is a ruin
b7557ab9828d2017224a12968f82c3118b6a8c0aminfrinlogic coding from the comand line with printing of results
b7557ab9828d2017224a12968f82c3118b6a8c0aminfrinHaskell modules: hiding, renaming
9474e446514b06765775eb0c1ec6645e2c5e50f6minfrin- group the axioms according to their leading operation/predicate symbol,
9474e446514b06765775eb0c1ec6645e2c5e50f6minfrin i.e. the f resp. the p in
9474e446514b06765775eb0c1ec6645e2c5e50f6minfrin forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
b7557ab9828d2017224a12968f82c3118b6a8c0aminfrin forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
e302f38fd646764ce1a1e1c578d794aef514a9e5sf if there are axioms not being of this form, output error
b32d756dae79045a9bc90e0d0b85582f6f28eaf3sfStatic analysis for HasCASL
e302f38fd646764ce1a1e1c578d794aef514a9e5sf pattern analysis for program equations
9c233808c898095865fcc0a2dc1cf594d0d8faf3sf implemented only atomic subtyping
3b41ccdaa163f4e900bbf8a7aa6a366df033822dminfrinWeak amalgamation analysis?
3b41ccdaa163f4e900bbf8a7aa6a366df033822dminfrinInstantiate Transformation Application system for HasCASL?
3b41ccdaa163f4e900bbf8a7aa6a366df033822dminfrinAutomatic generation of Haskell (for a HasCASL subset)
3b41ccdaa163f4e900bbf8a7aa6a366df033822dminfrinProofs in HasCASL
28587db43bc4bea96a36fbcffdd967e7b422bb97minfrinCoding HasCASL -> Isabelle with definedness axioms
5a2dcc476c33985b7681aa72256bcd7266057eddsf only strict functions are defined
5a2dcc476c33985b7681aa72256bcd7266057eddsfIsabelle interface
e08076ca56e6cb68b30846b9e9339061058aae6dpoirier One emacs with spec and proof buffer
e08076ca56e6cb68b30846b9e9339061058aae6dpoirier Reload button should rebuild buffers while keeping as much as possible
e08076ca56e6cb68b30846b9e9339061058aae6dpoirier keep structuring of Hets theories
e08076ca56e6cb68b30846b9e9339061058aae6dpoirier************************************************
e08076ca56e6cb68b30846b9e9339061058aae6dpoirierRainer (Klaus)
e08076ca56e6cb68b30846b9e9339061058aae6dpoirier************************************************
b7a2f855b5e31abc24dab2eef28e9e2f985ae25brpluemSPASS encoding improvements in SPASS.Conversions/Comorphisms.CASL2SPASS
b7a2f855b5e31abc24dab2eef28e9e2f985ae25brpluem - if there is only one sort in the signature eliminate it
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener special case: (freely) generated sorts are not eliminated
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener new flag in SPASS sign: singleSorted
fa1c7ce09927decc1eecd1e9a35cc5331078a052covener Sentences are modified in CASL2SPASS
84fbf855118f318dd5e511d8e5b902cecc1177c0jim all variable declarations have to consider the flag
ac45a43afbf38aa4a91c1402c6beef6ef8a2696dniq (quantified formulas) variable lists without types
ac45a43afbf38aa4a91c1402c6beef6ef8a2696dniq - F:Membership ==> true
ac45a43afbf38aa4a91c1402c6beef6ef8a2696dniq - T:Cast is omitted
b2b9b7f0644773b50aee41956a841ac884086250niq - T:Sorted_term is omitted
b2b9b7f0644773b50aee41956a841ac884086250niq typings in the signature have to be removed in SPASS.Conversions
b2b9b7f0644773b50aee41956a841ac884086250niq empty declarations list
b2b9b7f0644773b50aee41956a841ac884086250niqSPASS encoding improvements in CASL2SPASS
b4f348c8e74ba8166410ddeffac03e4887696788niq - if there are predicates defined upon equality substitute them with equality
b4f348c8e74ba8166410ddeffac03e4887696788niq and remove them from the signature
b4f348c8e74ba8166410ddeffac03e4887696788niq find definitions (Equivalences) where one side is a binary predicate
4fda5fb4cc40703a76e261bbf21ec1d6b51b7d3fjim and the other side is a builtin equality application (Strong_equation)
4fda5fb4cc40703a76e261bbf21ec1d6b51b7d3fjim return the full qualified (with type) predicate(s)
fa0dc2a4f675a868378a52946e5b244d6bf41196sf this is done before the translation of the signature/sentences happens
fa0dc2a4f675a868378a52946e5b244d6bf41196sf remove eqPrediate symbols from signature
0807f6da6091b748ab47c21ba66252fe8da2a966sf substitute eqPredications with Strong_equation in the Formulas
b92a868b537899a51efd8c200c396fa51c63839dtrawick************************************************
dc52cac281d8b311dc47d115ed979f923b667679rjung************************************************
dc52cac281d8b311dc47d115ed979f923b667679rjungfor ProofManagement-GUI
2534e869d2ba209bd0c43717ea80992e6de0c51djim mark imported theorems for selection
2534e869d2ba209bd0c43717ea80992e6de0c51djim provide structured (based on spec-names) selection/deselection facility
f8033d657a57eab45af44368774d8beb3e4f7f35pquerna of axioms and theorems
f8033d657a57eab45af44368774d8beb3e4f7f35pquernatrace if liniarity of sentences along development is given
02fd88c85a9850109753b87612955ad372de1575sffor consistency checking with Isabelle, look at the following SAT-Solvers:
02fd88c85a9850109753b87612955ad372de1575sfMChaff, ZChaff, Berkmin
da48ae521bcc2751f8eb8dfb02f7aab0f46943c6sfConsistency checker interface
da48ae521bcc2751f8eb8dfb02f7aab0f46943c6sf via global interface, accessible from global and node menus
da48ae521bcc2751f8eb8dfb02f7aab0f46943c6sf use falseSentence from Logic.Logic (property: holds in no model)
1374472d83ce061a431b7f6eeb5e5135fb4cd922jim proved -> inconsistent
1374472d83ce061a431b7f6eeb5e5135fb4cd922jim disproved -> consistent (assuming completeness)
1374472d83ce061a431b7f6eeb5e5135fb4cd922jim batch mode for automatic provers such as SPASS
1374472d83ce061a431b7f6eeb5e5135fb4cd922jim (use automatic flag for provers)
ab7a123efe997d907274eb672ab2b36746bb3f57sfbatch interface for Isabelle
ab7a123efe997d907274eb672ab2b36746bb3f57sf each goal is proved separatedly, with a time limit enforced
ab7a123efe997d907274eb672ab2b36746bb3f57sf by killing the process
a44d29a3794110c558c940bd903a1930d717a7d7sf the tactic is
a44d29a3794110c558c940bd903a1930d717a7d7sf "using Ax1 ... Axn by auto"
a44d29a3794110c558c940bd903a1930d717a7d7sf where Ax1 ... Axn is the list of all axioms.
a44d29a3794110c558c940bd903a1930d717a7d7sf "auto" could be replaced with "best", "blast" etc. (user selection)
70003ce816d7851e49ecb0cdc5137becd647ed18niqIgnore axiom selection for interactive provers
b5e45168970cefb8b2d0bea709ea69790f3eab96niqTranslation between Achim's ontology data structure and CASL (in Hets)
815067bc5eff8fc218019e18ee5ea868372917cdsfvisualization of "taxonomy" of CASL signatures
9f2c7096ac1f41aca1328d304d54dbaef4ebb06drjung (subsorts = inheritance, unary preds = concepts, binary preds = relations)
ff5e24709209b13601480827b0fecf32c428ff32rjung last two ... partially done
39d67f66729a7008c1e73d65a81e778ce819a227rjungRecognize guarded fragment of CASL:
da20b997bf4652f7597e0a7845db371aab2f7187rjung G ::= forall x . At(x) => G where At is a conjunction of atoms
da20b997bf4652f7597e0a7845db371aab2f7187rjung | exists x . At(x) /\ G
133cbcba0df4ba0e72f7eaaaebabe119f145f261niqJoost Visser wg. ATerms in Haskell => neues Repository
c8dcde16853eef36b713d4633fac83b66e49aa5eniq************************************************
c8dcde16853eef36b713d4633fac83b66e49aa5eniqMarkus, Lutz
c8dcde16853eef36b713d4633fac83b66e49aa5eniq************************************************
1a7a4f8c6a312cb237e428c77da0792eb165dc7aniqBeweise in Isabelle
1a7a4f8c6a312cb237e428c77da0792eb165dc7aniqCASL consistency checker
1a7a4f8c6a312cb237e428c77da0792eb165dc7aniqWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
927e277b4be750e06960b3d4f1c2b1ca146e0555niq (Vorbild: Larch-Handbuch)
927e277b4be750e06960b3d4f1c2b1ca146e0555niqSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
927e277b4be750e06960b3d4f1c2b1ca146e0555niqParser and static analysis for CSP-CASL
83de39879307034216ce0af15a47a88a55af11e3rjung************************************************
7cfa48136e3b42a14cdff1a46b60f4e4d2ad5291niq************************************************
7cfa48136e3b42a14cdff1a46b60f4e4d2ad5291niqCASL consistency checker
7cfa48136e3b42a14cdff1a46b60f4e4d2ad5291niqIntegration with generic prover interface?
0a4924de8350e2bbfa16a27f42ff0bc61aa52d43rjung************************************************
8e8568ec7d29f056a2a4942d1d50481e441c25d9covener************************************************
bec2a2e375fe46599b68399abfcf67b89b270b57wroweenhance Web interface with SPASS (%implied, consistency)
bec2a2e375fe46599b68399abfcf67b89b270b57wrowetranslation of proofs along comorphisms (it this necessary at all???)
bec2a2e375fe46599b68399abfcf67b89b270b57wrowe use inverse morphism?
bec2a2e375fe46599b68399abfcf67b89b270b57wrowe leads to translation of G_theory along comorphism that also
bec2a2e375fe46599b68399abfcf67b89b270b57wrowe keeps proof status info
bec2a2e375fe46599b68399abfcf67b89b270b57wrowe this may be used in GUI prover interfaces for recovering old proof attempts
bec2a2e375fe46599b68399abfcf67b89b270b57wrowe and offering them as default
46fdfef7dfc745effe179387e1dcb8245d3804batrawickproveCMDLinteractive (PGIP)
46fdfef7dfc745effe179387e1dcb8245d3804batrawickModel expansion flag for comorphisms
46fdfef7dfc745effe179387e1dcb8245d3804batrawickUmlaute in daVinci anzeigen
46fdfef7dfc745effe179387e1dcb8245d3804batrawickFragen an Michael:
46fdfef7dfc745effe179387e1dcb8245d3804batrawickwerden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?
46fdfef7dfc745effe179387e1dcb8245d3804batrawick was ist dort eigentlich das Problem?
46fdfef7dfc745effe179387e1dcb8245d3804batrawickCodierung von Subsorten?
f4845813cd6fa5749dfec8e3bc647b85c1df0980wrowepaper with Paolo
f4845813cd6fa5749dfec8e3bc647b85c1df0980wrowe semantic adequecy of HOL translation
f4845813cd6fa5749dfec8e3bc647b85c1df0980wroweRegulate concurrent proving
f4845813cd6fa5749dfec8e3bc647b85c1df0980wrowe.dg files: store only current library; import .dg files for other libraries
f55c048e33a905f9f771b3aed309373bdf547944jortonMarkus' Bsp:
f55c048e33a905f9f771b3aed309373bdf547944jortonIsabelle: use meta-quantifiers
f55c048e33a905f9f771b3aed309373bdf547944jortonlocal subsumption ?
cddaaa6378c5082e8dff0d11dc21cf6c4928ecbcjortonbetter syntax (Tina)
cddaaa6378c5082e8dff0d11dc21cf6c4928ecbcjortoncheck for proved theorems
cddaaa6378c5082e8dff0d11dc21cf6c4928ecbcjortonAbstractGraphView: switch to Result monad
9b2bd9e83cbb6f5debb2edba59a0c12089eb37c3minfrinunite or rename consCheck and cons_checkers
9b2bd9e83cbb6f5debb2edba59a0c12089eb37c3minfrinBinInt.casl: revealing in Int1 does not work correctly
9b2bd9e83cbb6f5debb2edba59a0c12089eb37c3minfrinfrom Stefan W�lfl:
a89e2c1651aab7734345fa3a6712a757708535ferjungcomputeTheory does not work across library imports
a89e2c1651aab7734345fa3a6712a757708535ferjunglocal theorems
a89e2c1651aab7734345fa3a6712a757708535ferjungall nodes named
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjunghierarchical Isabelle theories
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjungdaVinci printing is not adequate
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjunghiding of internal nodes does not work
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjungFOL without quantifiers and with uniform disjunctions
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjung (i.e. x R1 y \/ x R2 y)
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjung (with and without =)
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjungalgorithmic path consistency over a relation algebra
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjung plug in reasoner for this
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjung develop correctness results (algorithmic path consistency=path consistency)
adc9a2e2b2e56a7416c90f949bd0c72ddd6f1793rjung within CASL
23bc6974af15e69a9aa4b5b3fc06b800b53ca234sfCASL sublogics:
23bc6974af15e69a9aa4b5b3fc06b800b53ca234sf---------------
23bc6974af15e69a9aa4b5b3fc06b800b53ca234sfFOL without quantifiers (with and without =)
298eb744831be682f749ffe1c01c88d82adf215esfguarded fragment
298eb744831be682f749ffe1c01c88d82adf215esf[from DOLCE cooperation:
298eb744831be682f749ffe1c01c88d82adf215esfontology mediation via pushouts/pullbacks/pulations
298eb744831be682f749ffe1c01c88d82adf215esfRobinson consistency with shared theory constructed via pre-image?
298eb744831be682f749ffe1c01c88d82adf215esfshow theorem links between same instances of different parameterized
b9aa9ca00496f67eb755d67764775ff23ac7eb03covener specs (where one is an extension of the other one)
b9aa9ca00496f67eb755d67764775ff23ac7eb03covenerlink menu for %implies, $def, %cons, even without open proof obligation
f2386b627177c7a80d38fed6ec0aed3c086909c1covenerfor a proved theorem, show minimal part of DG needed for proof
f2386b627177c7a80d38fed6ec0aed3c086909c1covenercons, def, mono for nodes
70d4e28f12f8cc2e130457c841095dc69c67cf31minfrinIsabelle interface: each qed should write proof info into file
70d4e28f12f8cc2e130457c841095dc69c67cf31minfringlobally display nodes containing symbols mapped "twice" (i.e. via
70d4e28f12f8cc2e130457c841095dc69c67cf31minfrin different signature morphisms)
70d4e28f12f8cc2e130457c841095dc69c67cf31minfrin and add a menu for each node allowing for tracking the different
1a668f25bc6b4b111822caaba70bb9289d64ade5niqtopsort coding: partial functions as relations?
7a6c86627922e38fa227943b9f888f96109681e5covenertheorem link menu for proof obligations
7a6c86627922e38fa227943b9f888f96109681e5covenerUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
7a6c86627922e38fa227943b9f888f96109681e5covenerin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
17efe57eb8d88fa0d371f4ac4939dbbbe78fd09bcovenerBuffer.het, sublogic of node Buffer:
17efe57eb8d88fa0d371f4ac4939dbbbe78fd09bcovenerFail: illegal node type in sublogic computation
8068423ee2d80a7c42b2325a71c24ac9485327cecovenerJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
8068423ee2d80a7c42b2325a71c24ac9485327cecovenerfor CSP-CASL example: with logic
8068423ee2d80a7c42b2325a71c24ac9485327cecovenerheterogeneous static ana
7703bad94964cc64022e08e2d1ae2c5fbfe2d3c6covenertheorem links between nodes in different libraries
7703bad94964cc64022e08e2d1ae2c5fbfe2d3c6covenerbasicProofs: use info about used axioms
689ee47a7329cf0d0ce4c5a98670b33fcf00d81btrawick ensure that axiom/thm names are unique
689ee47a7329cf0d0ce4c5a98670b33fcf00d81btrawickOverload / inlineAxioms: injections
5a2f24f5e41d52e59e1c11e90cd423b8967d4184trawickremove "prove" menu in abstracted dg
19ce7effbcc8a735f1a883f9266e086fde2adb63poirierbetter sublogic analysis in codings
5d58d0bc1ce35e0ee814b6c2dc21a5286e460b87covenerthy files in subdir
8eac2273e3d5f2dc8464fada76fcfbf33a938a2fcoveneradjust path for thy files, such that hets can also be started from subdirs
8eac2273e3d5f2dc8464fada76fcfbf33a938a2fcovenerRestrict Sonjas simplifications to HasCASL
8eac2273e3d5f2dc8464fada76fcfbf33a938a2fcoveneradd suitable axioms to simplifier and CR
c6124d7fde07b58d51785d0f1cb509026eeaa138jimcomputeTheory: remove double axioms
c6124d7fde07b58d51785d0f1cb509026eeaa138jimadd suitable axioms to simplifier and classical reasoner
c6124d7fde07b58d51785d0f1cb509026eeaa138jimbetter display of internal nodes (use tooltip?)
680e7b4c70df00b695883c824947ca6ec15d69ecsfupdate Hets, CASL, daVinci on web page
3a49a6c98ef80c71830e66e7f8f46083001b494ctrawickCASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
6fee4e2faa2e45fe2636d01e35d03c2cf0c9d431minfrinpacking of binaries: add hets-update, refer to TclTk
6fee4e2faa2e45fe2636d01e35d03c2cf0c9d431minfrinCCC interface
03aa31ad82759363ba1a55589e517b16308ef635minfrintest for sublogic before applying comorphism
03aa31ad82759363ba1a55589e517b16308ef635minfrinMissing points for heterogeneous WADT 04 example:
03aa31ad82759363ba1a55589e517b16308ef635minfrin- coding to Isabelle: translate sort gen constraints
9fe23388f983cb652b5d68e2bd92aa9f0568c574minfrin- Improve adapation to Isabelle's lexis
e9eabac76b50e8f00d0c391f6070d0f42db77aa2wroweIsabelle: (ask Christoph)
e9eabac76b50e8f00d0c391f6070d0f42db77aa2wrowe remove datatypes from sort list
e9eabac76b50e8f00d0c391f6070d0f42db77aa2wrowe prove local thm link (=> green)
e9eabac76b50e8f00d0c391f6070d0f42db77aa2wrowe "prove" menu with choice windows
433d36fd71af86369719893afe09877be4cb4f3asf incorporate sublogics
433d36fd71af86369719893afe09877be4cb4f3asf sublogic translation table
14e5a8cc15b1dcc26ad5420973304e53a9e5406bsf better interaction between Isabelle instance (for one node)
14e5a8cc15b1dcc26ad5420973304e53a9e5406bsf + selection of single goals that are proved
14e5a8cc15b1dcc26ad5420973304e53a9e5406bsf => use PGIP interface (Christoph, David)
46fdfef7dfc745effe179387e1dcb8245d3804batrawick correct show theory
46fdfef7dfc745effe179387e1dcb8245d3804batrawick Keep proofs and lemmas in .thy files (kind of merge)
46fdfef7dfc745effe179387e1dcb8245d3804batrawick CASL-like syntax
46fdfef7dfc745effe179387e1dcb8245d3804batrawick CASL annotation for lemmas that should be used in proof
46fdfef7dfc745effe179387e1dcb8245d3804batrawick inherit CASL's mixfix syntax
46fdfef7dfc745effe179387e1dcb8245d3804batrawickSignatures versus theories: where to store additional infos?
46fdfef7dfc745effe179387e1dcb8245d3804batrawickcomp(id,x)=x for comorphism names
573f949c582f06bd738a96196f40b646b6d540b8rpluemGeneralise CASL2Modal
573f949c582f06bd738a96196f40b646b6d540b8rpluemMixfix analysis + typecheck for modality axiomatizations
573f949c582f06bd738a96196f40b646b6d540b8rpluemModal logics: modal logic, temporal logic, mu calculus
c44902d07eab7deb803a59e959f57cf3b7d56655poirier+ translations (e.g. modal to FOL)
c44902d07eab7deb803a59e959f57cf3b7d56655poirierCASL->Haskell with free DTs (mark sortgens) + recursion
ae1981fc94adf2b231e2d0e15d2f895b2138c969covener- List[Dec] wird List[Pos]
ae1981fc94adf2b231e2d0e15d2f895b2138c969covener- node numbers do not match
ae1981fc94adf2b231e2d0e15d2f895b2138c969covener- thm links with external target should be provable as well
4ac05f9625e37cc421f4ea548422827b4de163d7niqRemove warnings
4ac05f9625e37cc421f4ea548422827b4de163d7niqDifferent types of logic translations
4ac05f9625e37cc421f4ea548422827b4de163d7niqImprove Static analysis of structured specs
6999a76d8eb5ef6b4b295e51df0b2fb6064bd373covenerDevelopment graph calculus, Strategies for DG rules
6999a76d8eb5ef6b4b295e51df0b2fb6064bd373covener use graph grammars to model rules? transformation units?
6999a76d8eb5ef6b4b295e51df0b2fb6064bd373covenerManagement of change
ead0b57bbeaec5acb14f931b5641962f429dabc9trawickIntegrate provers
ead0b57bbeaec5acb14f931b5641962f429dabc9trawick Otter model checker
77d6f9d5c2a5cab805e9ace265628f3d791b937dniq FOL-prover by Uli Furhbach
77d6f9d5c2a5cab805e9ace265628f3d791b937dniq modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
77d6f9d5c2a5cab805e9ace265628f3d791b937dniq Isabelle codings: www.inf.ethz.ch/~vigano
a9d359cdeb1cee65cdb9fab5e19ffb4846172183trawick Renate Schmidt, Manchester: uses FOL prover for description logic
77d6f9d5c2a5cab805e9ace265628f3d791b937dniq (as efficient as DL-specific tools!)
9f35dd32eedd781d218a85f0315ea5526a8adc84minfrin Look at PROSPER toolkit
9f35dd32eedd781d218a85f0315ea5526a8adc84minfrin consistency: see IJCAR-workshop on non-provability in Cork
9f35dd32eedd781d218a85f0315ea5526a8adc84minfrin IJCAR workshop about logical frameworks and meta-languages
9f35dd32eedd781d218a85f0315ea5526a8adc84minfrinIntegrate CCC
5dc4220fc22561537ce1421a03e11846a5b719ebminfrinKlaus' wayfinding example
a9d359cdeb1cee65cdb9fab5e19ffb4846172183trawickask Detlef: critical pairs, Fossacs paper by Francesco
68c4447ba8e057cf38cbbec918e0549b817f20b4minfrinUniForM workbench:
68c4447ba8e057cf38cbbec918e0549b817f20b4minfrinfirst steps towards CASL instance, using ATerms and re-using MMISS instance
68c4447ba8e057cf38cbbec918e0549b817f20b4minfrinvariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
68c4447ba8e057cf38cbbec918e0549b817f20b4minfrinIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
e33d0698670fead33dbd7c907363053b9e2be454minfrin Grothendieck logic)
e33d0698670fead33dbd7c907363053b9e2be454minfrin + for TAS: reflection of HOL in HOL, to be composed with encodings
e33d0698670fead33dbd7c907363053b9e2be454minfrin (i.e. signatures, axioms, signature morphisms in HOL,
e33d0698670fead33dbd7c907363053b9e2be454minfrin re-use ML signatures) (Einar)
cf8a8738330694e60bad421fcc8361d80b0e9124minfrinDisplay Specs as daVinci subgraphs
cf8a8738330694e60bad421fcc8361d80b0e9124minfrinUser interface
4ea8055e720d18f386b8026b546e5836ecccba4arjung--------------
a9d359cdeb1cee65cdb9fab5e19ffb4846172183trawickLogic graph window
a9d359cdeb1cee65cdb9fab5e19ffb4846172183trawickInput text window
4ea8055e720d18f386b8026b546e5836ecccba4arjungDevelopment graph window
fd80868005a61e747bc45b39df83cae7abb3d151pgollucciProver windows
60a8830541cd85d23a42ccb1639bc4744de9d526poirier************************************************
60a8830541cd85d23a42ccb1639bc4744de9d526poirierFOR STUDENTS
60a8830541cd85d23a42ccb1639bc4744de9d526poirier************************************************
5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrinHets interactive (provide cmd line interface, but hold loaded libraries in memory, provide switch to context of spec, and type checking of expressions, interaction with emacs mode)
5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrinPackaging of installation
5ae15cd9d22fb3bdfd2eb0b9761c4ef07fbf2f96minfrinGUI (vgl. VSE)
69fc9805c344b2dd5fd49a4f75cbf55dedeac7d6minfrin with Eclipse, WXHaskell or GTk?
69fc9805c344b2dd5fd49a4f75cbf55dedeac7d6minfrin how to integrate with event system of UniForM workbench?
69fc9805c344b2dd5fd49a4f75cbf55dedeac7d6minfrinintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
46fdfef7dfc745effe179387e1dcb8245d3804batrawick this interacts with GUI!
46fdfef7dfc745effe179387e1dcb8245d3804batrawickData.Serizable (only when ghc supports it) better: rely on pointer equality
46fdfef7dfc745effe179387e1dcb8245d3804batrawickXML interface
ca0a943242b488c162aa89874498e0316f7b2f2eminfrinincrease performance
e1c6c1dac26c35ecebe158438bb0c56afbb9bfb0sfintegrate QuickCheck: come to lecture!
38451a13fb80b89e704792ebc0e6f9e5e5877d7dsf++++++++++++++++++++++++++++++++++++++++++++++++
38451a13fb80b89e704792ebc0e6f9e5e5877d7dsfRemaining things
38451a13fb80b89e704792ebc0e6f9e5e5877d7dsf++++++++++++++++++++++++++++++++++++++++++++++++
38451a13fb80b89e704792ebc0e6f9e5e5877d7dsfMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
505e342aefa9fbccc857f1bc653a310e25511946sf Coq, PTT in Maude
505e342aefa9fbccc857f1bc653a310e25511946sfProofs with basic datatypes
26734c75baf170a492ef6a82f07b24ee1af7d0b1sfVerbesserung der Fehlermeldungen
dda254ba84bdff5e236917af1b31693ca4360eabcovenerImprove encoding: CATS/basic_encode.sml (3 days)
dda254ba84bdff5e236917af1b31693ca4360eabcovenerMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
dda254ba84bdff5e236917af1b31693ca4360eabcovenerRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
dda254ba84bdff5e236917af1b31693ca4360eabcovenerExample of Agnes und Frank: proofs in HOL-CASL (2 days)
bcb567d8f48f5de8aa84e0b19e93357e0a4d970epquernaTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
bf52162f2d05c1fb1a107c7ef108de73f739b3edpquernaExamples for cond rewriting -> Christophe
e1d33ac481c6683a069630c8f9aceec3a48babcetrawickDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
e1d33ac481c6683a069630c8f9aceec3a48babcetrawickAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
cf12a027b0859c14d5c4852efffeff62158cd98dtrawickEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
3becbd2611ffb2e8391a8eacce765b43dcb1c669wroweHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
8e5e9b2d4c6cbcd21ca182fe1109d59284239515wroweHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
3becbd2611ffb2e8391a8eacce765b43dcb1c669wroweHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
9c78f8d71737dfbbbf4da2f9acb397567a10e88bsfEncoding of structured free (3 days)
9c78f8d71737dfbbbf4da2f9acb397567a10e88bsfEncoding of structured cofree (2 weeks)
9c78f8d71737dfbbbf4da2f9acb397567a10e88bsfEingabesyntax als Mix zwischen CASL und HOL (3 days)
9c78f8d71737dfbbbf4da2f9acb397567a10e88bsfAdapt Isabelle unions to CASL unions (1 week)
4be9c459920a7c1cfe62d654327dae5c4bb6b284sfGenerate Proof obligations (1 week)
4be9c459920a7c1cfe62d654327dae5c4bb6b284sfAdd renaming to Isabelle kernel (2 months)
47ff2654d827dd3596ce2e4099d69cec0f1009b9takashiRepository mit korrekten und fehlerhaften Specs
b4ae72381175122ebfe42ff0d11db7a7f4162014takashiHetCATS User manual, Doku fuer Environments (2 weeks)
b4ae72381175122ebfe42ff0d11db7a7f4162014takashiConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
5e1ae35c05125b8b6c6c648c60e576f5796ea061rpluemComparsion of parsers (ML-yacc parser, SDF-Parser)
b115299831a7b4bbec58a88d708d8536e1ecd50csfConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
5e1ae35c05125b8b6c6c648c60e576f5796ea061rpluemPVS anbinden (Kooperation mit Cachan?)
b9a830d395feaa66ab621841a5cd86e1fa2d184brjungPortations: Intel-Solaris, Mac OS-10 (2 weeks)
b9a830d395feaa66ab621841a5cd86e1fa2d184brjung(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
82e6711dc508d2822d9397f07136ba4ddd8764e1niqViews on CASL specs: CATS/viewer.sml (2 weeks)
82e6711dc508d2822d9397f07136ba4ddd8764e1niqUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
82e6711dc508d2822d9397f07136ba4ddd8764e1niqModule graph CATS/module_graph.sml (1 week) -> Maya?
82e6711dc508d2822d9397f07136ba4ddd8764e1niqATerms via XML: CATS/aterms.sml (2 weeks)
82e6711dc508d2822d9397f07136ba4ddd8764e1niqNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
f43104f173247435cb4ade2b89aa2ca8108aedb7niqLibrary management: CATS/lib_ana.sml (2 weeks)
f43104f173247435cb4ade2b89aa2ca8108aedb7niqVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
c26aa743a70c2148cdca1e6c637c605d9025b051niq{- This does not work due to needed ordering:
c26aa743a70c2148cdca1e6c637c605d9025b051niqinstance Functor Set where
c26aa743a70c2148cdca1e6c637c605d9025b051niq fmap = mapSet
c26aa743a70c2148cdca1e6c637c605d9025b051niqinstance Monad Set where
e076b09731977eafcef2bfc6f5323f3ab7e83b15niq return = unitSet
e076b09731977eafcef2bfc6f5323f3ab7e83b15niq m >>= k = unionManySets (setToList (fmap k m))
22d3cfb8f14471efbc3bbc8faa2c59805ac2395fjimAufbau von comptable
64dbb5532fba398c5e81efeb21c7fd50c05819d7niq--------------------
d31d6c32262a8d1cbfc63d9f7adccae46002c8f7niq[("normal","normal","normal"),
d31d6c32262a8d1cbfc63d9f7adccae46002c8f7niq ("normal","inclusion","normal"),
d31d6c32262a8d1cbfc63d9f7adccae46002c8f7niq ("inclusion","normal","normal"),
bcb567d8f48f5de8aa84e0b19e93357e0a4d970epquerna ("inclusion","inclusion","inclusion")]
11f2c481e1d57bedb3f758565307501e9a2730ddtrawickAufbau von ginfo
11f2c481e1d57bedb3f758565307501e9a2730ddtrawick--------------------
11f2c481e1d57bedb3f758565307501e9a2730ddtrawickMit initgraphs erzeugen
11f2c481e1d57bedb3f758565307501e9a2730ddtrawickAufbau des Graphen selbst
11f2c481e1d57bedb3f758565307501e9a2730ddtrawick------------------------