2N/APlan and priority list for CoFI tool activities

2N/A

2N/A************************************************

2N/AImmanuel

2N/A************************************************

2N/A

2N/Asee http://trac.informatik.uni-bremen.de:8080/hets

2N/Auser normann

2N/A

2N/A************************************************

2N/ARazvan (Till)

2N/A************************************************

2N/A

2N/Asee http://trac.informatik.uni-bremen.de:8080/hets

2N/Auser rpascanu

2N/A

2N/A************************************************

2N/AAnton (Till)

2N/A************************************************

2N/A

2N/Asee http://trac.informatik.uni-bremen.de:8080/hets

2N/Auser luecke

2N/A

2N/A**************** task A ************************

2N/A

2N/Asee http://trac.informatik.uni-bremen.de:8080/hets

2N/Auser maeder

2N/A

2N/A

2N/A************************************************

2N/AFlorian (Till)

2N/A************************************************

2N/A

2N/Asee http://trac.informatik.uni-bremen.de:8080/hets

2N/Auser fmossa

2N/A

2N/A************************************************

2N/AHendrik (Till)

2N/A************************************************

2N/A

2N/Asee http://trac.informatik.uni-bremen.de:8080/hets

2N/Auser hiben

2N/A

2N/AAnzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen

2N/A

2N/A

2N/A************************************************

2N/AMingyi (Till)

2N/A************************************************

2N/A

2N/Asee http://trac.informatik.uni-bremen.de:8080/hets

user xinga

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

Heng (Klaus)

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

see http://trac.informatik.uni-bremen.de:8080/hets

user jiang

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

Ken (Till)

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

see http://trac.informatik.uni-bremen.de:8080/hets

user ken

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

further task 1

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

see http://trac.informatik.uni-bremen.de:8080/hets

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

further task 2

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

see http://trac.informatik.uni-bremen.de:8080/hets

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

further task 3

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

see http://trac.informatik.uni-bremen.de:8080/hets

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

further task 4

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

done

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

further task 5

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

see http://trac.informatik.uni-bremen.de:8080/hets

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

remaining stuff

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

see http://trac.informatik.uni-bremen.de:8080/hets

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

Daniel

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

generate infrastructure for circular coinduction

CCS example: commutativity of || by coinduction

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

Christian

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

see http://trac.informatik.uni-bremen.de:8080/hets

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

Rainer (Klaus)

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

see http://trac.informatik.uni-bremen.de:8080/hets

user rainer25

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

Martin

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

see http://trac.informatik.uni-bremen.de:8080/hets

user mkhl

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

Klaus

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

for ProofManagement-GUI

provide structured (based on spec-names) selection/deselection facility

of axioms and theorems

trace if liniarity of sentences along development is given

Ignore axiom selection for interactive provers

((

Improvements:

* display node name (instead of number) in uDrawGraph widow title

* add conversion of equivalent sorts into special arrow

* needs modification of Taxnomy Graph

Translation between Achim's ontology data structure and CASL (in Hets)

visualization of "taxonomy" of CASL signatures

(subsorts = inheritance, unary preds = concepts, binary preds = relations)

last two ... partially done

))

Recognize guarded fragment of CASL:

G ::= forall x . At(x) => G where At is a conjunction of atoms

| exists x . At(x) /\ G

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

Till

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

see http://trac.informatik.uni-bremen.de:8080/hets

user till

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

FOR STUDENTS

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

Data.Serizable (only when ghc supports it) better: rely on pointer equality

XML interface

increase performance

integrate QuickCheck: come to lecture!

++++++++++++++++++++++++++++++++++++++++++++++++

Remaining things

++++++++++++++++++++++++++++++++++++++++++++++++

Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude

Coq, PTT in Maude

Proofs with basic datatypes

Verbesserung der Fehlermeldungen

Improve encoding: CATS/basic_encode.sml (3 days)

More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)

Renamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)

Example of Agnes und Frank: proofs in HOL-CASL (2 days)

Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day)

Examples for cond rewriting -> Christophe

Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?

Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)

Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS

HOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)

HOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)

HOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)

Encoding of structured free (3 days)

Encoding of structured cofree (2 weeks)

Eingabesyntax als Mix zwischen CASL und HOL (3 days)

Adapt Isabelle unions to CASL unions (1 week)

IsaWin git/src/isa_ext/casl_thy.sml (1 week)

Generate Proof obligations (1 week)

Add renaming to Isabelle kernel (2 months)

Basic datatypes CASL-lib/Basic/basic.casl

Repository mit korrekten und fehlerhaften Specs

HetCATS User manual, Doku fuer Environments (2 weeks)

Conversion ASF/SDF-Parser -> abstract syntax (in Haskell)

Comparsion of parsers (ML-yacc parser, SDF-Parser)

Conversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren

PVS anbinden (Kooperation mit Cachan?)

Portations: Intel-Solaris, Mac OS-10 (2 weeks)

(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm

Views on CASL specs: CATS/viewer.sml (2 weeks)

Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII

Module graph CATS/module_graph.sml (1 week) -> Maya?

ATerms via XML: CATS/aterms.sml (2 weeks)

Neues Tool-Schaubild auf Web-Seiten ver�ffentlichen

Library management: CATS/lib_ana.sml (2 weeks)

Version management/Uniform Workbench: CATS/lib_ana.sml (2 months)

{- This does not work due to needed ordering:

instance Functor Set where

fmap = mapSet

instance Monad Set where

return = unitSet

m >>= k = unionManySets (setToList (fmap k m))

-}

Aufbau von comptable

--------------------

[("normal","normal","normal"),

("normal","inclusion","normal"),

("inclusion","normal","normal"),

("inclusion","inclusion","inclusion")]

Aufbau von ginfo

--------------------

Mit initgraphs erzeugen

Aufbau des Graphen selbst

------------------------

addnode

addlink