1516N/APlan and priority list for CoFI tool activities

1231N/A

1231N/A************************************************

1231N/AImmanuel

1231N/A************************************************

1231N/A

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

1231N/Auser normann

1231N/A

1231N/A************************************************

1231N/ARazvan (Till)

1231N/A************************************************

1231N/A

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

1231N/Auser rpascanu

1231N/A

1231N/A************************************************

1231N/AAnton (Till)

1231N/A************************************************

1231N/A

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

1231N/Auser luecke

1231N/A

1231N/A**************** task A ************************

1231N/A

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

1516N/Auser maeder

1516N/A

1516N/A

1231N/A************************************************

1231N/AFlorian (Till)

1231N/A************************************************

1231N/A

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

1231N/Auser fmossa

1231N/A

1231N/A************************************************

1231N/AHendrik (Till)

1231N/A************************************************

1231N/A

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

1231N/Auser hiben

1231N/A

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

1231N/A

1231N/A

1231N/A************************************************

1231N/AMingyi (Till)

1231N/A************************************************

1231N/A

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

1231N/Auser xinga

1231N/A

1231N/A

1231N/A************************************************

1231N/AHeng (Klaus)

1231N/A************************************************

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

1231N/Auser jiang

1231N/A

1231N/A************************************************

1231N/AKen (Till)

1231N/A************************************************

1231N/A

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

1231N/Auser ken

1231N/A

1231N/A

1231N/A************************************************

1231N/Afurther task 1

1231N/A************************************************

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

1231N/A

1231N/A************************************************

1231N/Afurther task 2

1231N/A************************************************

1231N/A

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

1231N/A

1231N/A************************************************

1231N/Afurther task 3

1231N/A************************************************

1231N/A

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

1231N/A

1231N/A************************************************

1231N/Afurther task 4

1231N/A************************************************

1231N/A

1231N/Adone

1231N/A

1231N/A************************************************

1231N/Afurther task 5

1231N/A************************************************

1231N/A

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

1231N/A

1231N/A

1231N/A************************************************

1231N/Aremaining stuff

1231N/A************************************************

1231N/A

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

1231N/A

1231N/A************************************************

1231N/ADaniel

1231N/A************************************************

1231N/A

1231N/Agenerate infrastructure for circular coinduction

1231N/ACCS example: commutativity of || by coinduction

1231N/A

1231N/A************************************************

1231N/AChristian

1231N/A************************************************

1231N/A

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

1231N/A

1231N/A************************************************

1231N/ARainer (Klaus)

1231N/A************************************************

1231N/A

1231N/Afor ProofManagement-GUI

1231N/A mark imported theorems for selection

1231N/A extend Logic.Prover SenStatus with wasTheorem

1231N/A somewhere in computeTheory implement setting of wasTheorem

1231N/A if wasTheorem not appears with right status in ProofManagementGUI

1231N/A add wasTheorem to Common.Result.Named, as well

1231N/A and adapt conversion functions of SenStatus to Named and vice

1231N/A versa in Logic.Prover

1231N/A Mark old theorems in "Axioms to include" Listbox with prefixed

1231N/A "(Th)"

1231N/A add button "Deselect former Theorems"

1231N/A test all this with CASL-lib/Calculi/Space/RCCVerification.het

1231N/A all nodes without incoming heterogeneous edges are provable with

1231N/A SPASS

1231N/A

1231N/A************************************************

1231N/AMartin

1231N/A************************************************

1231N/A

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

1231N/Auser mkhl

1231N/A

1231N/A

1231N/A************************************************

1231N/AKlaus

1231N/A************************************************

1231N/A

1231N/Afor ProofManagement-GUI

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

1231N/A of axioms and theorems

1231N/A

1231N/Atrace if liniarity of sentences along development is given

1231N/A

1231N/AConsistency checker interface

1231N/A via global interface, accessible from global and node menus

1231N/A use falseSentence from Logic.Logic (property: holds in no model)

1231N/A proved -> inconsistent

1231N/A disproved -> consistent (assuming completeness)

1231N/A batch mode for automatic provers such as SPASS

1231N/A (use automatic flag for provers)

1231N/A

1231N/Abatch interface for Isabelle

1231N/A each goal is proved separatedly, with a time limit enforced

1231N/A by killing the process

1231N/A the tactic is

1231N/A "using Ax1 ... Axn by auto"

1231N/A where Ax1 ... Axn is the list of all axioms.

1231N/A "auto" could be replaced with "best", "blast" etc. (user selection)

1231N/A

1231N/AIgnore axiom selection for interactive provers

1231N/A

1231N/ATranslation between Achim's ontology data structure and CASL (in Hets)

1231N/A

1231N/Avisualization of "taxonomy" of CASL signatures

1231N/A (subsorts = inheritance, unary preds = concepts, binary preds = relations)

1231N/A

1231N/A last two ... partially done

1231N/A

1231N/ARecognize guarded fragment of CASL:

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

1231N/A | exists x . At(x) /\ G

1231N/A

1231N/AJoost Visser wg. ATerms in Haskell => neues Repository

1231N/A

1231N/A

1231N/A

1231N/A************************************************

1231N/ATill

1231N/A************************************************

1231N/A

1231N/ABinInt.casl: revealing in Int1 does not work correctly

1231N/A

1231N/Afrom Stefan W�lfl:

1231N/AcomputeTheory does not work across library imports

1231N/Alocal theorems

1231N/Aall nodes named

1231N/Ahierarchical Isabelle theories

1231N/AdaVinci printing is not adequate

1231N/Ahiding of internal nodes does not work

1231N/A

1231N/ACSPs

1231N/A----

1231N/AFOL without quantifiers and with uniform disjunctions

1231N/A (i.e. x R1 y \/ x R2 y)

1231N/A (with and without =)

1231N/Aalgorithmic path consistency over a relation algebra

1231N/A plug in reasoner for this

1231N/A develop correctness results (algorithmic path consistency=path consistency)

1231N/A within CASL

1231N/A

1231N/ACASL sublogics:

1231N/A---------------

1231N/AFOL without quantifiers (with and without =)

1231N/Aguarded fragment

1231N/AProp

1231N/A

1231N/A

1231N/A[from DOLCE cooperation:

1231N/Aquit wish!

1231N/Aontology mediation via pushouts/pullbacks/pulations

1231N/ARobinson consistency with shared theory constructed via pre-image?

1231N/Ashow theorem links between same instances of different parameterized

1231N/A specs (where one is an extension of the other one)

1231N/Alink menu for %implies, $def, %cons, even without open proof obligation

1231N/Afor a proved theorem, show minimal part of DG needed for proof

1231N/Acons, def, mono for nodes

1231N/AIsabelle interface: each qed should write proof info into file

1231N/Aglobally display nodes containing symbols mapped "twice" (i.e. via

1231N/A different signature morphisms)

1231N/A and add a menu for each node allowing for tracking the different

1231N/A uses of the symbols/concepts

1231N/Atopsort coding: partial functions as relations?

1231N/A]

1231N/A

1231N/Atheorem link menu for proof obligations

1231N/A

1231N/AUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error

1231N/Ain Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms

1231N/Acorrectly.

1231N/A

1231N/ABuffer.het, sublogic of node Buffer:

1231N/AFail: illegal node type in sublogic computation

1231N/A

1231N/A

1231N/AJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb

1231N/A

1231N/Afor CSP-CASL example: with logic

1231N/Aheterogeneous static ana

1231N/A

1231N/Atheorem links between nodes in different libraries

1231N/A

1231N/AbasicProofs: use info about used axioms

1231N/A ensure that axiom/thm names are unique

1231N/A

1231N/AOverload / inlineAxioms: injections

1231N/A

1231N/A

1231N/Aremove "prove" menu in abstracted dg

1231N/A

1231N/Abetter sublogic analysis in codings

1231N/A

1231N/Athy files in subdir

1231N/Aadjust path for thy files, such that hets can also be started from subdirs

1231N/A

1231N/ARestrict Sonjas simplifications to HasCASL

1231N/Aadd suitable axioms to simplifier and CR

1231N/AcomputeTheory: remove double axioms

1231N/Aadd suitable axioms to simplifier and classical reasoner

1231N/A

1231N/Abetter display of internal nodes (use tooltip?)

1231N/A

1231N/Aupdate Hets, CASL, daVinci on web page

1231N/A

1231N/A

1231N/ACASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)

1231N/A

1231N/Apacking of binaries: add hets-update, refer to TclTk

1231N/A

1231N/ACCC interface

1231N/A

1231N/Atest for sublogic before applying comorphism

1231N/A

1231N/AMissing points for heterogeneous WADT 04 example:

1231N/A- coding to Isabelle: translate sort gen constraints

1231N/A

1231N/A- Improve adapation to Isabelle's lexis

1231N/A

1231N/AIsabelle: (ask Christoph)

1231N/A remove datatypes from sort list

1231N/A prove local thm link (=> green)

1231N/A

1231N/A "prove" menu with choice windows

1231N/A incorporate sublogics

1231N/A sublogic translation table

1231N/A

1231N/A better interaction between Isabelle instance (for one node)

1231N/A + selection of single goals that are proved

1231N/A => use PGIP interface (Christoph, David)

1231N/A

1231N/A correct show theory

1516N/A Keep proofs and lemmas in .thy files (kind of merge)

1516N/A CASL-like syntax

1231N/A CASL annotation for lemmas that should be used in proof

1516N/A inherit CASL's mixfix syntax

1516N/A

1516N/ASignatures versus theories: where to store additional infos?

1231N/A

1231N/Acomp(id,x)=x for comorphism names

1231N/A

1231N/AGeneralise CASL2Modal

1231N/AMixfix analysis + typecheck for modality axiomatizations

1231N/AModal logics: modal logic, temporal logic, mu calculus

1231N/A+ translations (e.g. modal to FOL)

1231N/A

1231N/ACASL->Haskell with free DTs (mark sortgens) + recursion

1231N/A

1231N/A

1516N/A- List[Dec] wird List[Pos]

1231N/A

1516N/A- node numbers do not match

1231N/A- thm links with external target should be provable as well

1231N/A

1231N/A

1231N/ARemove warnings

1516N/A

1231N/ADifferent types of logic translations

1516N/AImprove Static analysis of structured specs

1231N/ADevelopment graph calculus, Strategies for DG rules

1231N/A use graph grammars to model rules? transformation units?

1231N/AManagement of change

1231N/A

1231N/AIntegrate provers

1231N/A Otter model checker

1231N/A FOL-prover by Uli Furhbach

1231N/A modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig

1231N/A Isabelle codings: www.inf.ethz.ch/~vigano

1231N/A Renate Schmidt, Manchester: uses FOL prover for description logic

1231N/A (as efficient as DL-specific tools!)

1231N/A Look at PROSPER toolkit

1231N/A consistency: see IJCAR-workshop on non-provability in Cork

1231N/A IJCAR workshop about logical frameworks and meta-languages

1231N/AIntegrate CCC

1231N/AEncodings

1231N/A

1231N/A

1231N/AErrors:

1231N/AKlaus' wayfinding example

1231N/A

1231N/Aask Detlef: critical pairs, Fossacs paper by Francesco

1231N/A

1231N/AUniForM workbench:

1231N/Afirst steps towards CASL instance, using ATerms and re-using MMISS instance

1231N/Avariants for specs (needed for DOLCE: CASL variant, DL variant, ...)

1231N/A

1231N/AIntegration of MAYA and Isabelle/HOL (global HOL-Coding of

1231N/A Grothendieck logic)

1231N/A + for TAS: reflection of HOL in HOL, to be composed with encodings

1231N/A (i.e. signatures, axioms, signature morphisms in HOL,

1231N/A re-use ML signatures) (Einar)

1231N/A

1231N/ADisplay Specs as daVinci subgraphs

1231N/A

1231N/AUser interface

1231N/A--------------

1231N/ALogic graph window

1231N/AInput text window

1231N/ADevelopment graph window

1231N/AProver windows

1231N/A

1231N/A

1231N/A************************************************

1231N/AFOR STUDENTS

1231N/A************************************************

1231N/A

1231N/AHets interactive (provide cmd line interface, but hold loaded libraries in memory, provide switch to context of spec, and type checking of expressions, interaction with emacs mode)

1231N/APackaging of installation

1231N/A

1231N/AGUI (vgl. VSE)

1231N/A with Eclipse, WXHaskell or GTk?

1231N/A how to integrate with event system of UniForM workbench?

1231N/Aintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)

1231N/A this interacts with GUI!

1231N/A

1231N/AData.Serizable (only when ghc supports it) better: rely on pointer equality

1231N/AXML interface

1231N/Aincrease performance

1231N/A

1231N/Aintegrate QuickCheck: come to lecture!

1231N/A

1231N/A++++++++++++++++++++++++++++++++++++++++++++++++

1231N/ARemaining things

1231N/A++++++++++++++++++++++++++++++++++++++++++++++++

1231N/A

1231N/AMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude

1231N/A Coq, PTT in Maude

1231N/A

1231N/A

1231N/AProofs with basic datatypes

1231N/A

1231N/AVerbesserung der Fehlermeldungen

1231N/A

1231N/AImprove encoding: CATS/basic_encode.sml (3 days)

1231N/AMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)

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

1231N/AExample of Agnes und Frank: proofs in HOL-CASL (2 days)

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

1231N/AExamples for cond rewriting -> Christophe

1231N/ADoku: VSE-Prover, VSE-Method VSE-demo in Bremen?

1231N/AAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)

1231N/AEigene IsaWin-Instanz mit CASL-RS statt HOL-RS

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

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

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

1231N/AEncoding of structured free (3 days)

1231N/AEncoding of structured cofree (2 weeks)

1231N/AEingabesyntax als Mix zwischen CASL und HOL (3 days)

1231N/AAdapt Isabelle unions to CASL unions (1 week)

1231N/AIsaWin git/src/isa_ext/casl_thy.sml (1 week)

1231N/AGenerate Proof obligations (1 week)

1231N/AAdd renaming to Isabelle kernel (2 months)

1231N/A

1231N/ABasic datatypes CASL-lib/Basic/basic.casl

1231N/ARepository mit korrekten und fehlerhaften Specs

1231N/A

1231N/AHetCATS User manual, Doku fuer Environments (2 weeks)

1231N/A

1231N/AConversion ASF/SDF-Parser -> abstract syntax (in Haskell)

1231N/AComparsion of parsers (ML-yacc parser, SDF-Parser)

1231N/A

1231N/AConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren

1231N/APVS anbinden (Kooperation mit Cachan?)

1231N/A

1231N/APortations: Intel-Solaris, Mac OS-10 (2 weeks)

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

1231N/A

1231N/AViews on CASL specs: CATS/viewer.sml (2 weeks)

1231N/AUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII

1231N/AModule graph CATS/module_graph.sml (1 week) -> Maya?

1231N/AATerms via XML: CATS/aterms.sml (2 weeks)

1231N/A

1231N/ANeues Tool-Schaubild auf Web-Seiten ver�ffentlichen

1231N/A

1231N/ALibrary management: CATS/lib_ana.sml (2 weeks)

1231N/AVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)

1231N/A

1231N/A

1231N/A

1231N/A

1231N/A{- This does not work due to needed ordering:

1231N/Ainstance Functor Set where

1231N/A fmap = mapSet

1231N/Ainstance Monad Set where

1231N/A return = unitSet

1231N/A m >>= k = unionManySets (setToList (fmap k m))

1231N/A-}

1231N/A

1231N/A

1231N/A

1231N/A

1231N/AAufbau von comptable

1231N/A--------------------

1231N/A[("normal","normal","normal"),

1231N/A ("normal","inclusion","normal"),

1231N/A ("inclusion","normal","normal"),

1231N/A ("inclusion","inclusion","inclusion")]

1231N/A

1231N/AAufbau von ginfo

1231N/A--------------------

1231N/AMit initgraphs erzeugen

1231N/A

1231N/AAufbau des Graphen selbst

1231N/A------------------------

1231N/Aaddnode

1231N/Aaddlink

1231N/A

1231N/A

1231N/A

1231N/A