todo revision d4f60a7dc41e0430d16c79f0d156e556d6d1ba37
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiHaskell parser f�r XHaskell erweitern
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiDimplom: Encoding for HasCASL in Isabelle/HOL(CF)
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowskidevelopment graph calculus
9b6a240bf8a37887add38054413d7f880bd59cf3Till Mossakowski- Stack overflow for "show just subtree"
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski- view-test7.casl should be provable with globDecomp + locDecopm
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski- fail when doing first globDecomp, then local decomp in RelationsAndOrders
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski- correct MAYA: glob decomp: some links are not found (Jorina)
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowskitype check for CASL
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski*** Error encode.casl:8.30, No correct typing for
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski************************************************
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTest auf Einpunkt-Modell
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski (ein Datenelement, wahre Pr�dikate, totale Funktionen)
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiport CCC to Haskell
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiZicheng (Till)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiTranslation from CASL with subsorts to CASL without subsorts
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskisee CATS/basic_encode.sml, encode SubCFOL into CFOL
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiencode subsorting by injection functions
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski1. translation of signatures (see HetCATS/CASL/Sign.hs)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski2. genertion of axioms (injectivity, overloading ...)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskidetails: see paper in Theoretical Computer Science, p. 407
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiLaTeX pretty printer
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowskivon Christian:
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowskia) analysierte Formeln und Terme optimal/k�rzer ausgeben:
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowskishorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till MossakowskiIn Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskiunqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskimit dem Ergebnistyp qualifiziert.
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski((a: Nat) + (b: Nat)): Nat
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskib) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskif�r die CASL Datentypen zu bekommen.
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski************************************************
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski************************************************
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiMissing points for heterogeneous WADT 04 example:
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski- improve display of HasCASL sigs + mors
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiStatic analysis for HasCASL
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski checking class constraints of terms
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski pattern analysis for program equations
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski - for simple types (currently type synonyms)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski symbol representation
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski symbol map analysis (hiding sub/supertypes)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiWeak amalgamation analysis?
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiInstantiate Transformation Application system for HasCASL?
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiProofs in HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich (subsorts = inheritance, unary preds = concepts, binary preds = relations)
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus LuettichRecognize guarded fragment of CASL:
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski | exists x . At(x) /\ G
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski************************************************
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski************************************************
87268d03b727bc9091716644fcf4048379accf02Till MossakowskiBeweise in Isabelle
87268d03b727bc9091716644fcf4048379accf02Till MossakowskiCASL consistency checker
87268d03b727bc9091716644fcf4048379accf02Till MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
1604c7123ebd603b2ca3eb6d2bd325cbdb23ee99Till Mossakowski (Vorbild: Larch-Handbuch)
aa6f6fa09091e92016598584162b9ba909af48ccTill MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiParser and static analysis for CSP-CASL
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
e1f2ef9a7f4d41a42927b2e352cbb558791a4007Klaus Luettich************************************************
b021b399b59fb7009308ed7a3eda30182dea7976Klaus LuettichCASL consistency checker
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiIsaWin: support CASL-libraries
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
6c82551a9e6a38aa7c774db95ee957379f03df75Christian MaederStatic analysis of architectural specs
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiMissing points for heterogeneous WADT 04 example:
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- coding to Isabelle: translate sort gen constraints
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- correct display of CASL sublogis
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- extended globDecomp rule: existing local Thm links
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski (e.g. generated by %implied) should lead to fewer new local
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski links ("local composition" rule)
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder- Improve adapation to Isabelle's lexis
b303a3717d229b102bca29e58d9e38c2f91fd233Christian MaederIsabelle: (ask Christoph)
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski free datatypes
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder prove local thm link (=> green)
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski better interaction between Isabelle instance (for one node)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski + selection of single goals that are proved
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski => use PGIP interface (Christoph, David)
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski correct show theory
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski Keep proofs and lemmas in .thy files (kind of merge)
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski CASL-like syntax
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski CASL annotation for lemmas that should be used in proof
566b6a416bde2bc90d3aece2d992127303fb5d75Till Mossakowski inherit CASL's mixfix syntax
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskicomp(id,x)=x for comorphism names
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiGeneralie CASL2Modal
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiMixfix analysis + typecheck for modality axiomatizations
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiModal logics: modal logic, temporal logic, mu calculus
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski+ translations (e.g. modal to FOL)
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiComorphisms: also map of theories; with default definition
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiCASL->Haskell with free DTs (mark sortgens) + recursion
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiCoding of subsorts as unary predicates (for ontologies)
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- List[Dec] wird List[Pos]
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- George wg. Schlie�en von Fenstern
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- node numbers do not match
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- thm links with external target should be provable as well
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiRemove warnings
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiDifferent types of logic translations
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiImprove Static analysis of structured specs
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiDevelopment graph calculus, Strategies for DG rules
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiManagement of change
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiIntegrate provers
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski Otter model checker
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski FOL-prover by Uli Furhbach
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Isabelle codings: www.inf.ethz.ch/~vigano
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Renate Schmidt, Manchester: uses FOL prover for description logic
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (as efficient as DL-specific tools!)
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder Look at PROSPER toolkit
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder consistency: see IJCAR-workshop on non-provability in Cork
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder IJCAR workshop about logical frameworks and meta-languages
4dcd2d1b64ccc7f705f2ce10d129ef9304ae413bChristian MaederKlaus' wayfinding example
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian MaederUniForM workbench:
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowskifirst steps towards CASL instance, using ATerms and re-using MMISS instance
0d42a1490aa92c24b19823f745104eefbf29675dChristian Maedervariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill MossakowskiIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski Grothendieck logic)
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski + for TAS: reflection of HOL in HOL, to be composed with encodings
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski (i.e. signatures, axioms, signature morphisms in HOL,
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski re-use ML signatures) (Einar)
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiDisplay Specs as daVinci subgraphs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUser interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski--------------
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederLogic graph window
96cc01853b72b9d0fdc9e3d309a196a2216de119Christian MaederInput text window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph window
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederProver windows
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichHets Web interface (cf. CATS/web_interface2.sml)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPackaging of installation
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichintegrate QuickCheck
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichGUI (vgl. VSE)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichincrease performance
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich++++++++++++++++++++++++++++++++++++++++++++++++
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichRemaining things
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich++++++++++++++++++++++++++++++++++++++++++++++++
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich Coq, PTT in Maude
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichProof general interface (1 day)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichTest Maya with basic datatypes
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichVerbesserung der Fehlermeldungen
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichImprove encoding: CATS/basic_encode.sml (3 days)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichExample of Agnes und Frank: proofs in HOL-CASL (2 days)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichExamples for cond rewriting -> Christophe
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichEncoding of structured free (3 days)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichEncoding of structured cofree (2 weeks)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichEingabesyntax als Mix zwischen CASL und HOL (3 days)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichAdapt Isabelle unions to CASL unions (1 week)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichGenerate Proof obligations (1 week)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichAdd renaming to Isabelle kernel (2 months)
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiRepository mit korrekten und fehlerhaften Specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHetCATS User manual, Doku fuer Environments (2 weeks)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichComparsion of parsers (ML-yacc parser, SDF-Parser)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichPVS anbinden (Kooperation mit Cachan?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPortations: Intel-Solaris, Mac OS-10 (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichViews on CASL specs: CATS/viewer.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModule graph CATS/module_graph.sml (1 week) -> Maya?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiATerms via XML: CATS/aterms.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLibrary management: CATS/lib_ana.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski{- This does not work due to needed ordering:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Functor Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski fmap = mapSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Monad Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski return = unitSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski m >>= k = unionManySets (setToList (fmap k m))