144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

4b90c3b8ee582daeead21ce272f11c952ef1631eTill Mossakowskimost things have been moved to the new bug tracking system

cc9279b89cc62b80199696ac7e87b6d2bdd08e7aTill Mossakowski

5f40e8aa2c372040ab519c6401627d64812922ffKlaus Luettichsee http://trac.informatik.uni-bremen.de:8080/hets

c1015e823b467ffb3e58fe3eacb0db58937063baTill Mossakowski

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************

baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichKlaus

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************

aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowski

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettichfor ProofManagement-GUI

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

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich of axioms and theorems

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettichtrace if liniarity of sentences along development is given

ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich

e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiIgnore axiom selection for interactive provers

e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich((

89ee5859757b78fefccda0a582cc896bd422d006Klaus LuettichImprovements:

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

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich * add conversion of equivalent sorts into special arrow

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich * needs modification of Taxnomy Graph

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich

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

b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich last two ... partially done

89ee5859757b78fefccda0a582cc896bd422d006Klaus Luettich))

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRecognize guarded fragment of CASL:

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

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | exists x . At(x) /\ G

baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/AS_CASL_DL.der.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/PredefinedGlobalAnnos.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/PredefinedSign.inline.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/Sign.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL_DL/StatAna.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiComorphisms/CASL2SPASS.hs:{- todo

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiComorphisms/KnownProvers.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiComorphisms/Modal2CASL.inline.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiOWL_DL/Logic_OWL_DL.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiOWL_DL/Print.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiOWL_DL/ReadWrite.der.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiOWL_DL/ReadWrite.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiGUI/ProofManagement.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiSPASS/DFGParser.hs:quantification s = do (ts',t') <- parens (do ts <- squares (commaSep1 term) -- todo: var binding should allow only simple terms

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiSPASS/PrintTPTP.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiTaxonomy/MMiSSOntology.hs: todo: add a new edge type for equivalence which should be visited only once

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski************************************************

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiChristian

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski************************************************

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiComorphisms/CoCFOL2IsabelleHOL.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiHasCASL/Sublogic.hs:{- todo: test computations

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL/Sublogic.hs:-- to do: implement pr_sign

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski************************************************

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiTill

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski************************************************

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiBitte auch aus folgenden Files die todo-Listen nach Trac verschieben:

7c610eb832a4575b209fc6e6c674b99975135012Till Mossakowski

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL/Morphism.hs:todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCASL/SymbolMapAnalysis.hs:todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCoCASL/Logic_CoCASL.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCoCASL/StatAna.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiConstraintCASL/Logic_ConstraintCASL.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiConstraintCASL/StaticAna.hs:{- todo: check formulas -}

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCspCASL/Logic_CspCASL.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCspCASL/SignCSP.hs:-- todo: implement isInclusion, computeExt

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiCspCASL/StatAnaCSP.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiGUI/ConvertDevToAbstractGraph.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiGUI/hets_cgi.hs: todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiIsabelle/IsaPrint.hs: todo: brackets in (? x . p x) ==> q

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiIsabelle/IsaProve.hs: todo: thy files in subdir, check of legal changes in thy file

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiLogic/Grothendieck.hs:{- todo: somthing like the following...

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiLogic/Prover.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiModal/Logic_Modal.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiPGIP/Utils.hs:{- todo: refactor getGoalList, extractGraphEdge, extractGraphLabeledEdge

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/Automatic.hs:todo in general:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/Automatic.hs:{- todo: implement apply for GlobDecomp and Subsumption

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/EdgeUtils.hs:{- todo: also treat conservativity proof status in computation of proof basis

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/EdgeUtils.hs: _ -> Right False -- todo: also treat conservativity proof status

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/Global.hs:todo for Jorina:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/HideTheoremShift.hs: todo: use compInclusion instead of compHomInclusion

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiProofs/InferBasic.hs:todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiStatic/AnalysisArchitecture.hs:{- todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiStatic/DevGraph.hs:todo:

7c610eb832a4575b209fc6e6c674b99975135012Till MossakowskiSyntax/Parse_AS_Structured.hs: todo:

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

5210ca461d947c73189a20c7a9c909c06c5efc70Till Mossakowski