f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorPlan and priority list for CoFI tool activities

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorSonja (Till)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorHaskell parser f�r XHaskell erweitern

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorDimplom: Encoding for HasCASL in Isabelle/HOL(CF)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorJorina (Till)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majordevelopment graph calculus

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major- Stack overflow for "show just subtree"

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major- view-test7.casl should be provable with globDecomp + locDecopm

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major- fail when doing first globDecomp, then local decomp in RelationsAndOrders

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorMartin (Till)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majortype check for CASL

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majordocumentation

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major*** Error encode.casl:8.30, No correct typing for

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorMingyi (Till)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major cd /home/cofi/xinga/src/uni

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major gmake packages

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major cd /home/cofi/xinga/src/HetCATS

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major make hets

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majortry out small examples, e.g.

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major export HETS_LIB=.../CASL-lib

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major hets .../CASL-lib/Basic/Algebra_I.casl

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorlook at HetCATS/README

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorTest auf Einpunkt-Modell

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major (ein Datenelement, wahre Pr�dikate, totale Funktionen)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major siehe ccc/OnePoint.hs

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorSignature morphism: just carry around the image

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majoruse three-valued logic {true, false, *}, * means "don't know"

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorequations between new sorts are true, otherwise *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majornew predicates are true, otherwise *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorand t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majort t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorf f f f

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major* * f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majoror t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majort t t t

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorf t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major* t * *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorimplies t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majort t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorf t t t

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major* t * *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorequivalent t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majort t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorf f t *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major* * * *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majornot t f *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major f t *

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major(this is just Kleene's strong three-valued logic)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorImplement it using Maybe Bool and monads

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorSort generation constraints:

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major use recover_sort_gen

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major check whether all generated sorts (when translated via the sort map) are new

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major check whether for each generated sort,

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major there is a term with generating operations

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major and variables in non-generated sorts

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major Therefore start with the empty list of sorts, and repeatedly

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major compute the one-step-closure under the generating operations

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major (ignoring argument sorts outside the generated sorts)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major stop when iteration is stable

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorport CCC to Haskell

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter MajorZicheng (Till)

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major************************************************

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorcvs -d :pserver:mnd@.... login

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Majorcvs -d :pserver:mnd@.... checkout HetCATS

f015d695b84915f1c2c3fcf81f339548af1852c4Peter Major

Translation from CASL with subsorts to CASL without subsorts

cvs -d :pserver:cvsread@.... login

cvs -d :pserver:cvsread@.... checkout CATS

see CATS/basic_encode.sml, encode SubCFOL into CFOL

encode subsorting by injection functions

1. translation of signatures (see HetCATS/CASL/Sign.hs)

2. genertion of axioms (injectivity, overloading ...)

(see HetCATS/CASL/AS_Basic_CASL.hs)

details: see paper in Theoretical Computer Science, p. 407

Angucken:

FORMULA in CASL/AS_Basic.hs

Sign in CASL/Sign.hs

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

Heng (Klaus)

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

LaTeX pretty printer

von Christian:

a) analysierte Formeln und Terme optimal/k�rzer ausgeben:

shorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}

In Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen

unqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur

mit dem Ergebnistyp qualifiziert.

((a: Nat) + (b: Nat)): Nat

b) eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex

und andere Formate besser zu unterst�tzen und einheitlichen PP code

f�r die CASL Datentypen zu bekommen.

HasCASL hat auch noch keine Mixfix- und Latex Ausgabe.

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

Christian

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

Missing points for heterogeneous WADT 04 example:

- improve display of HasCASL sigs + mors

Static analysis for HasCASL

checking class constraints of terms

pattern analysis for program equations

Sub-/Supertypes

- for simple types (currently type synonyms)

symbol representation

symbol map analysis (hiding sub/supertypes)

Weak amalgamation analysis?

Instantiate Transformation Application system for HasCASL?

Automatic generation of Haskell (for a HasCASL subset)

Proofs in HasCASL

Case study

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

Klaus

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

visualization of "taxonomy" of CASL signatures

(subsorts = inheritance, unary preds = concepts, binary preds = relations)

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

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

Markus, Lutz

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

Beweise in Isabelle

CASL consistency checker

Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen

(Vorbild: Larch-Handbuch)

Simpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln

Parser and static analysis for CSP-CASL

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

Christoph

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

CASL consistency checker

IsaWin: support CASL-libraries

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

Maciek

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

Static analysis of architectural specs

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

Till

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

Mixfix analysis + typecheck for modality axiomatizations

CCC interface

comp(id,x)=x fpr comorphism names

Generalie CASL2Modal

Comorphisms: also map of theories; with default definition

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

Coding of subsorts as unary predicates (for ontologies)

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

- List[Dec] wird List[Pos]

- George wg. Schlie�en von Fenstern

- node numbers do not match

- thm links with external target should be provable as well

Missing points for heterogeneous WADT 04 example:

- coding to Isabelle: translate sort gen constraints

- remove / in thy names (ask cxl for function)

- problem with Ids starting with __ (look at Isabelle's lexis)

- correct display of CASL sublogis

- correct MAYA: glob decomp: some links are not found (Jorina)

- extended globDecomp rule: existing local Thm links

(e.g. generated by %implied) should lead to fewer new local

links ("local composition" rule)

Modal logics: modal logic, temporal logic, mu calculus

+ translations (e.g. modal to FOL)

Isabelle: (ask Christoph)

correct show theory

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

prove local thm link (=> green)

better interaction between Isabelle instance (for one node)

+ selection of single goals that are proved

=> use PGIP interface (Christoph, David)

CASL-like syntax

CASL annotation for lemmas that should be used in proof

inherit CASL's mixfix syntax

Remove warnings

Different types of logic translations

Improve Static analysis of structured specs

Development graph calculus, Strategies for DG rules

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

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

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

FOR STUDENTS

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

Emacs mode

Hets Web interface (cf. CATS/web_interface2.sml)

CCC ?

Packaging of installation

integrate QuickCheck

XML interface

GUI (vgl. VSE)

increase performance

++++++++++++++++++++++++++++++++++++++++++++++++

Remaining things

++++++++++++++++++++++++++++++++++++++++++++++++

Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude

Coq, PTT in Maude

Proof general interface (1 day)

Test Maya 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))

-}