todo revision ea4393779e0fd0f2cc61529fb17b12f7dfbfa3fb
Plan and priority list for CoFI tool activities
************************************************
Immanuel
************************************************
user normann
************************************************
Razvan (Till)
************************************************
user rpascanu
************************************************
Anton (Till)
************************************************
user luecke
**************** task A ************************
user maeder
************************************************
Florian (Till)
************************************************
user fmossa
************************************************
Hendrik (Till)
************************************************
user hiben
Anzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen
************************************************
Mingyi (Till)
************************************************
user xinga
************************************************
Heng (Klaus)
************************************************
user jiang
************************************************
Ken (Till)
************************************************
user ken
************************************************
further task 1
************************************************
************************************************
further task 2
************************************************
************************************************
further task 3
************************************************
************************************************
further task 4
************************************************
done
************************************************
further task 5
************************************************
************************************************
remaining stuff
************************************************
************************************************
Daniel
************************************************
generate infrastructure for circular coinduction
CCS example: commutativity of || by coinduction
************************************************
Christian
************************************************
************************************************
Rainer (Klaus)
************************************************
user rainer25
************************************************
Martin
************************************************
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
Consistency checker interface
via global interface, accessible from global and node menus
use falseSentence from Logic.Logic (property: holds in no model)
proved -> inconsistent
disproved -> consistent (assuming completeness)
batch mode for automatic provers such as SPASS
(use automatic flag for provers)
Ignore axiom selection for interactive provers
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
************************************************
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