6185db853e024a486ff8837e6784dd290d866112dougmPlan and priority list for CoFI tool activities

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougmImmanuel

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougm

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

6185db853e024a486ff8837e6784dd290d866112dougmuser normann

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougmRazvan (Till)

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougm

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

6185db853e024a486ff8837e6784dd290d866112dougmuser rpascanu

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougmAnton (Till)

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougm

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

6185db853e024a486ff8837e6784dd290d866112dougmuser luecke

6185db853e024a486ff8837e6784dd290d866112dougm

24424a35444c8487648be681d47bee4f57af0ffcdougm**************** task A ************************

6185db853e024a486ff8837e6784dd290d866112dougm

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

6185db853e024a486ff8837e6784dd290d866112dougmuser maeder

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougmFlorian (Till)

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougm

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

6185db853e024a486ff8837e6784dd290d866112dougmuser fmossa

6185db853e024a486ff8837e6784dd290d866112dougm

24424a35444c8487648be681d47bee4f57af0ffcdougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougmHendrik (Till)

24424a35444c8487648be681d47bee4f57af0ffcdougm************************************************

24424a35444c8487648be681d47bee4f57af0ffcdougm

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

6185db853e024a486ff8837e6784dd290d866112dougmuser hiben

6185db853e024a486ff8837e6784dd290d866112dougm

1cea05af420c1992d793dc442f4e30c7269fc107dougmAnzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen

5359815feb11a102a85ff1b899512fa9553b8c25dougm

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougmMingyi (Till)

24424a35444c8487648be681d47bee4f57af0ffcdougm************************************************

24424a35444c8487648be681d47bee4f57af0ffcdougm

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

6185db853e024a486ff8837e6784dd290d866112dougmuser xinga

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougmHeng (Klaus)

24424a35444c8487648be681d47bee4f57af0ffcdougm************************************************

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

6185db853e024a486ff8837e6784dd290d866112dougmuser jiang

6185db853e024a486ff8837e6784dd290d866112dougm

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

6185db853e024a486ff8837e6784dd290d866112dougmKen (Till)

6185db853e024a486ff8837e6784dd290d866112dougm************************************************

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)

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

for ProofManagement-GUI

mark imported theorems for selection

extend Logic.Prover SenStatus with wasTheorem

somewhere in computeTheory implement setting of wasTheorem

if wasTheorem not appears with right status in ProofManagementGUI

add wasTheorem to Common.Result.Named, as well

and adapt conversion functions of SenStatus to Named and vice

versa in Logic.Prover

Mark old theorems in "Axioms to include" Listbox with prefixed

"(Th)"

add button "Deselect former Theorems"

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

all nodes without incoming heterogeneous edges are provable with

SPASS

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

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

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)

batch interface for Isabelle

each goal is proved separatedly, with a time limit enforced

by killing the process

the tactic is

"using Ax1 ... Axn by auto"

where Ax1 ... Axn is the list of all axioms.

"auto" could be replaced with "best", "blast" etc. (user selection)

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

Joost Visser wg. ATerms in Haskell => neues Repository

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

Till

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

Buffer.het, sublogic of node Buffer:

Fail: illegal node type in sublogic computation

J�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb

for CSP-CASL example: with logic

heterogeneous static ana

theorem links between nodes in different libraries

basicProofs: use info about used axioms

ensure that axiom/thm names are unique

Overload / inlineAxioms: injections

remove "prove" menu in abstracted dg

better sublogic analysis in codings

thy files in subdir

adjust path for thy files, such that hets can also be started from subdirs

Restrict Sonjas simplifications to HasCASL

add suitable axioms to simplifier and CR

computeTheory: remove double axioms

add suitable axioms to simplifier and classical reasoner

better display of internal nodes (use tooltip?)

update Hets, CASL, daVinci on web page

CASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)

packing of binaries: add hets-update, refer to TclTk

CCC interface

test for sublogic before applying comorphism

Missing points for heterogeneous WADT 04 example:

- coding to Isabelle: translate sort gen constraints

- Improve adapation to Isabelle's lexis

Isabelle: (ask Christoph)

remove datatypes from sort list

prove local thm link (=> green)

"prove" menu with choice windows

incorporate sublogics

sublogic translation table

better interaction between Isabelle instance (for one node)

+ selection of single goals that are proved

=> use PGIP interface (Christoph, David)

correct show theory

Keep proofs and lemmas in .thy files (kind of merge)

CASL-like syntax

CASL annotation for lemmas that should be used in proof

inherit CASL's mixfix syntax

Signatures versus theories: where to store additional infos?

comp(id,x)=x for comorphism names

Generalise CASL2Modal

Mixfix analysis + typecheck for modality axiomatizations

Modal logics: modal logic, temporal logic, mu calculus

+ translations (e.g. modal to FOL)

CASL->Haskell with free DTs (mark sortgens) + recursion

- List[Dec] wird List[Pos]

- node numbers do not match

- thm links with external target should be provable as well

Remove warnings

Different types of logic translations

Improve Static analysis of structured specs

Development graph calculus, Strategies for DG rules

use graph grammars to model rules? transformation units?

Management of change

Integrate provers

Otter model checker

FOL-prover by Uli Furhbach

modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig

Isabelle codings: www.inf.ethz.ch/~vigano

Renate Schmidt, Manchester: uses FOL prover for description logic

(as efficient as DL-specific tools!)

Look at PROSPER toolkit

consistency: see IJCAR-workshop on non-provability in Cork

IJCAR workshop about logical frameworks and meta-languages

Integrate CCC

Encodings

Errors:

Klaus' wayfinding example

ask Detlef: critical pairs, Fossacs paper by Francesco

UniForM workbench:

first steps towards CASL instance, using ATerms and re-using MMISS instance

variants for specs (needed for DOLCE: CASL variant, DL variant, ...)

Integration of MAYA and Isabelle/HOL (global HOL-Coding of

Grothendieck logic)

+ for TAS: reflection of HOL in HOL, to be composed with encodings

(i.e. signatures, axioms, signature morphisms in HOL,

re-use ML signatures) (Einar)

Display Specs as daVinci subgraphs

User interface

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

Logic graph window

Input text window

Development graph window

Prover windows

BinInt.casl: revealing in Int1 does not work correctly

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

FOR STUDENTS

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

Hets 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)

Packaging of installation

GUI (vgl. VSE)

with Eclipse, WXHaskell or GTk?

how to integrate with event system of UniForM workbench?

integrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)

this interacts with GUI!

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