Plan and priority list for CoFI tool activities

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

Immanuel

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

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

user normann

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

Razvan (Till)

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

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

user rpascanu

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

Anton (Till)

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

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

user luecke

**************** task A ************************

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

user maeder

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

Florian (Till)

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

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

user fmossa

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

Hendrik (Till)

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

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

user hiben

Anzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen

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

Mingyi (Till)

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

see 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

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

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

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

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