Plan and priority list for CoFI tool activities

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

Immanuel

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

Suchfunktion f�r einen Knoten im DG:

welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?

erstmal auf eine Logik (z.B. CASL) beschr�nken

- Funktion f�r Morphismus-Suche zwischen Theorien

- evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty

RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme

- Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)

BasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?

Konfidenzgrade von Beweisen?

von Till/HiWi zu erledigen:

Repr�sentation �ndern:

Beweisobjekte an DGs, nicht an Regeln -- done

F�r Theoreme in Theorien an Beweisobjekte -- done

BasicProof mit Liste von Beweisobjekten -- �berfl�ssig

Definitionen auszeichnen -- done

F�r alles siehe G_theory, ThSens und SenStatus.

Isabelles Beweisobjekte einbinden

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

Razvan (Till)

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

Integration with PGIP

Hets needs to be equipped with a command-line interface that reads in

specification libraries and proof commands

Proof commands are special annotations in the libraries

All menu commands of the development graph interface (GUI/...) should become (proof) commands

when stepping through the specs, dg calculus generates proof obligations

(for the current dg node only),

which then can be discharged by Isabelle, SPASS etc.

That is, the proof commands always occur at the position in the text

that generates the dg node?!? or should they occur after each specification?

needs incremental parsing and static analysis for Hets libraries

easy: parse and analyse one specification at a time, and then process it with proof commands

more challenging: incrementally parse and analyse also individual specifications

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

Anton (Till)

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

Modal-CASL <-> CASL-DL

see Chapter 4 of "The Description Logic Handbook"

and ask Klaus for a print out of it

improve Modal-CASL

possibly also modal logic in CoCASL

**************** task A ************************

Proofs with Isabelle and SPASS

CASL basic datatypes

HasCASL examples

- improve simplifier for partiality in Isabelle coding

program interaction between solver, subgoaler and simplifier in such a way

that proofs of definedness conditions are postponed

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

Florian (Till)

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

Modelchecker f�r algebraische Eigenschaften

neue Hets-Option in Driver/WriteFn.hs implementieren

hets -n NonAssocRelationAlgebra

--modelSparQ=datei.lisp Calculi/Algebra/RelationAlgebra.casl

(oder -m datei.lisp)

siehe auch CASL.CompositionTable.ComputeTable

modelCheck :: SIMPLE_ID -> (Sign f e, [Named (FORMULA f)])

-> Result Bool

Warnung mit Gegenbspen ausgeben, wenn eine Eigenschaft nicht gilt

(abbrechen nach 10 Gegenbspen)

Warnungen erzeugen mit Funktion warning aus Common.Result

Range aus den CASL-FORMULAs extrahieren

Result ist eine Monade, ggf. mit do-Notation arbeiten

Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:

Allquantoren --> all, Existenzquantor --> any

CASL-Junktoren --> Haskell-Junktoren

Terme rekursiv auswerten, Operationen aus der Table nehmen

(siehe CASL.AS_CASL_Basic)

Aufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken

- ggf. Server nutzen

- Vorverarbeitung f�r Solver (z.B. Duplikate raus)

- Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)

Applikation1 ---

| | -- Freibuger Solver

XML --- |---- Franz�sischer Solver

| |-- Hets -- Bremer Solver

Applikation2 ----- |

ConstraintCASL

|

Semantische Modelle/Korrektheit (CASL, HAsCASL)

XML-Einlesen in Haskell:

HXT (siehe OMDoc.XmlHandling): kann Namespaces

(HaXML: kann Haskell-Datenypen in DTDs umwandeln)

Outline der Diplomarbeit

Qualitative Constraint-Kalk�le (siehe Thomas)

CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:

the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)

CASL-Formeln nur ganz kurz

ConstraintCASL

Signaturen, Signaturmorphismen (aus CASL)

Modelle (aus CASL)

Formeln

Erf�lltheit von Formeln

optional: Erf�lltheitsbedingung

M |= sigma(phi) <=> M|_sigma |= phi

f�r Signaturmorphismus sigma:Sigma_1->Sigma_2

M \in Mod(Sigma_2), phi\in Sen(Sigma_1)

Formalisierung von Kalk�len in ConstraintCASL

Constraint-Solver (auch in ihren Eigenheiten)

�bersetzungen zwischen den verschieden Formaten

praktischer Vergleich

Anwendung

�bersetzungen bis 30.Juni

ConstraintCASL -> Bremer Solver

CASL/ComputeTable

Bremer Solver -> ConstraintCASL

Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers

parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt

Das kann das als Option in Hets eingebunden werden (Christian Maeder)

Freiburger Constraint-Solver angucken im Juli

�bersetzungen bis 31. Juli

ConstraintCASL -> Freibuger Solver/XML-Format

CASL/ComputeTable

Option: comptable.xml

Freibuger Solver/XML-Format -> ConstraintCASL

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

Hendrik (Till)

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

OmDoc-Ausgabe konform mit RelaxNG?

OmDoc-Ausgabe Immanual zeigen

Typen von gebundenen Variablen weglassen

XML-Kataloge?

OMDoc-Datentyp einf�hren

Hets <-> Datenstruktur <-> OMDoc

Namensgenerierung/rekonstruktion auf der Seite Hets <-> Datenstruktur

Ursprung von Symbolen bei Hets -> OMDoc: irgendeins nehmen

Ausgabe als DAG, mittels OMR oder ref

Sharing-Algorithmus verwenden

Constraints mit Indizes: ggf. higher-order-Axiom erzeugen (Till fragen)

Anzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen

OMDoc-Bug melden f�r

free type Vehicle ::= sort Boat | sort Car

wobei Boat und Car aus anderen Files kommen

S. 156: Satz einfach streichen

sortdef legt bereits ein Symbol an

werden Signatur-Symbole in OMDoc mit der Theorie versehen, in der

sie als erstes eingef�hrt wurden?

checken f�r Library-Importe

OMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden

Hiding: unterschiedlich in OMDoc und Hets

ein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als

Signaturmorphismus

wird �bersetzt in einen OMDoc-Theoriemorphismus

mit leerer/identischer Abbildung, bei dem die Symbole aus

Sigma_2 \ Sigma_1 versteckt werden

Wenn der Signaturmorphismus keine Inklusion ist, ist keine

�bersetzung m�glich -> Fehler

ein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist

(also leere bzw. identische Abbildung) wird �bersetzt

in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus

falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss

ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,

der dann die Umbenennung macht, erzeugt werden

Logiken: �ber verschiedene OMDoc-Theorien mit URI

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

Mingyi (Till)

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

Diplomarbeit

- CASL-Logik: "Relating CASL with other specification languages", S.401-408

- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz

siehe CASL reference manual (suche nach conservative)

- warum sind konservative Erweiterungen wichtig?

- um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert

werden k�nnen

- f�r Refinement-Beweise

- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,

definitional oder monomorph sind

- Beschreibung des Algorithmus in Pseudocode

- Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus

als konservativ erkennt, muss f�r jedes Modell der kleineren

Spezifikation eine Modellerweiterung zur gr��eren Spezifikation

gefunden werden. Z.B. im Falle von free types kann dies eine

Termalgebra-Konstruktion sein.

SP1 -- \sigma --> SP2

konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem

SP2-Modell M2 mit M2|_\sigma=M1.

port CCC to Haskell

Funktionen imageOfMorphism und inhabited

von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs

mit "cvs add SigFuns.hs" einchecken

New module FreeTypes.hs:

"free datatypes and recursive equations are consistent"

checkFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool

Just True => Yes, is consistent

Just False => No, is inconsistent

Nothing => don't know

call the symbols in the image of the signature morphism "new"

- each new sort must be a free type,

i.e. it must occur in a sort generation constraint that is marked as free

(Sort_gen_ax constrs True)

such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs

if not, output "don't know"

and there must be one term of that sort (inhabited)

if not, output "no"

- group the axioms according to their leading operation/predicate symbol,

i.e. the f resp. the p in

forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t

forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t

Implication Application Strong_equation

forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi

forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi

Implication Predication Equivalence

if there are axioms not being of this form, output "don't know"

check' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)

check' [] = ([([],[])],emptyUniqSet)

-- nur ein Pattern, bestehend aus nur Variablen? fertig, True

check' [EqnInfo n ctx ps (MatchResult CanFail _)]

| all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)

-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!

check' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)

| all_vars ps = (pats, addOneToUniqSet indexs n)

where

(pats,indexs) = check' rs

-- falls ein Konstruktor dabei ist: split_by_constructor

-- wenn die ersten Argument nur Variablen sind: first_column_only_vars

check' qs@((EqnInfo n ctx ps result):_)

| all_vars ps = ([], unitUniqSet n)

| constructors = split_by_constructor qs

| only_vars = first_column_only_vars qs

| otherwise = panic "Check.check': Not implemented :-("

where

-- Note: RecPats will have been simplified to ConPats

-- at this stage.

constructors = or (map is_con qs)

only_vars = and (map is_var qs)

subsort definitions: are conservative if formula is satisfiable

(generate proof obligation)

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

Heng (Klaus)

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

OWL-DL logic

OWL-DL (<)-> CASL-DL

emacs mode:

highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl

some operation symbols

show hets output immediately

C-c C-g for hets -g

when hets terminates abnormally (e.g. with a fail), emacs loops

C-n jumps to the next error, but the message windows is not always scrolled

in such a way that the error is at the top (for long error lists)

Version for XEamcs?

should work with parser error messages as well (adapt these?)

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

Ken (Till)

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

look at command line interface (just call hets)

implement simplified rule Theorem-Hide-Shift

If there is an open global theorem link sigma:N1->N2 and

a hiding definition link theta:N3->N2 (i.e. the signature

morphism theta is from Sig(N2) to Sig(N3)), then prove

this theorem link by inserting a new global theorem link

theta o sigma : N1->N3.

use functions from Proofs.TheoremHideShift

test file: see CASL-lib/test_TheoremHideShift.casl

error in test_HideTheoremShift.casl

(when doing Automatic, HideTheoremShift, Automatic, and then

local proof in Target')

issue warning whne displaing theories (or performing proofs) of

nodes with ingoing hiding links.

improve dependency tracking for development graph proofs

display proved theorem links that depend on pending other proofs in yellow

display normal form of nodes with ingoing hiding links

try out examples

conservativity calculus

pushouts http://en.wikipedia.org/wiki/Pushout_%28category_theory%29

weakly amalgamable cocones

development graph calculus

(see Sect. IV:4.4 of the CASL Reference Manual)

look at Static/DevGraph.hs

look at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs

test command line interface (just call hets)

test development graph GUI:

global decomposition

menu edit - unnamed nodes - hide/show nodes,

node menu: show just subtree / undo

interaction with edit - proofs - automatic?

use update of uDrawGraph-nodes,edges instead of erasing and adding nodes

for attribute changes like color

profiling for "automatic" (look at www.haskell.org/ghc)

restrict proofs: only one prove window per node at a given time

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

further task 1

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

generate (x)html code from Doc

generate more readable LaTeX-code

see listings.sty for LaTeX generation (cf. CoSiT paper)

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

further task 2

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

Uni-Refactoring,

make modules hierarchical, replace deprecated code (i.e. FiniteMap, hslibs),

use HaXml as a cabalized library, provide uni as (one?) cabal

package(s), uni used to work under windows as well, watch the

i.e. FilePath, Process discussions (libraries@haskell.org)

possibly switch to a subversion repository, talk to Achim

(amahnke@tzi.de)

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

further task 3

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

look fgl/Data/Graph/Inductive/Graph.hs

look at Static/DevGraph.hs

change management

reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)

reload macht folgendes:

lade CASL-Datei neu ==> neuer Entwicklungsgraph

vergleiche alten+neuen Entwicklungsgraph, konstruiere eine

Abbildung (Common/Lib/Map.hs) von alt nach neu

(jeweils eine Abblidung f�r Knoten und eine f�r Kanten)

Kriterien f�r Finden der Knotenabbildung:

- Namen

- DGOrigin

- Signatur

einfaches Merge von lokalen Beweisen eines abgespeichteren DG

in aktuellen DG

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

further task 4

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

refined graph of Haskell module dependencies

using .import files

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

further task 5

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

port hets to windows. -- costs too much energy at this stage! Till

If hets should become successful then requests for support under

windows will surely follow.

Ghc, uni and uDrawGraph should work under windows. Only Isabelle does

not exist for windows, but SPASS does. Probably only a few path

computations need to be adapted (made modular) within hets. Also

position computations (of Parsec) should be checked under windows.

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

remaining stuff

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

set up a ticket and tracking systems (for bugs and features) instead

of this messy todo list

--> sourceforge???

refactoring of dgraphs: add unique tags + hashes (but no table)

how to compare complex datastructures:

tag x1==tag x2 || (hash x1==hash x2 && x1==x2)

display library graph

unify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs

and uni/appl/ontologytool/AbstractGraphView.hs

(make it really abstract), possibly contact amahnke@tzi.de regarding

Taxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!

set up default simplifier

set up default tactics using axioms

(see DOLCE sample files)

improve efficiency (e.g. of UserManual/Sbcs.casl), using profiling

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

Daniel

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

generate infrastructure for circular coinduction

CCS example: commutativity of || by coinduction

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

Christian

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

Isabelle coding

- improve display syntax in HasCASL-Isabelle coding

- identifiers in mixfix templates must be excluded as ordinary

identifiers (i.e. as quantified variables)

more abstract datatypes?

collect the patches for programatica (or create a package)

- conv (SN i p) = PN i (S p)

+ conv (SN i p) = PN i (Sn (show i) p)

in programatica/tools/base/parse2/NumberNames.hs

fixes translation error of Pair

simplification of HasCASL sentences (omit types)

Logic COL is a ruin

logic coding from the comand line with printing of results

Haskell modules: hiding, renaming

- group the axioms according to their leading operation/predicate symbol,

i.e. the f resp. the p in

forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t

forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi

if there are axioms not being of this form, output error

Static analysis for HasCASL

pattern analysis for program equations

implemented only atomic subtyping

Weak amalgamation analysis?

Instantiate Transformation Application system for HasCASL?

Automatic generation of Haskell (for a HasCASL subset)

Proofs in HasCASL

Case study

Coding HasCASL -> Isabelle with definedness axioms

only strict functions are defined

Isabelle interface

One emacs with spec and proof buffer

Reload button should rebuild buffers while keeping as much as possible

keep structuring of Hets theories

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

Rainer (Klaus)

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

implement a catch for calling MathServ based on the catch in runSpass

- a "connection refused" error should be handled differently:

"MathServ not running! Please contact

<hets-devel@informatik.uni-bremen.de>"

for the transition to ghc-6.6 spassProve must be corrected

- the regexp library changed in functionality

maybe the parse of the proof tree should be done without regular

expressions

performance improvements

- use seq to force the evaluation of the proof trees while in

GenericATP window otherwise "Exit prover" takes a long time

Example: seq (length $ show $ prooftree proofStatus) proofStatus

in GenericATP

usability improvements

- forceFocus to read-only textedit widgets in textSaveDisplay windows

upon left mouse click

also add for Details window

- update of goal list-boxes should not longer move visible

area of the list

involves getting and setting of visible area

code cleanup and documentation where necessary and possilbe

in SPASS/* and GUI/GenericATP*, GUI/Proofmanagement.hs

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

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

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

for consistency checking with Isabelle, look at the following SAT-Solvers:

MChaff, ZChaff, Berkmin

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

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

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

Integration with generic prover interface?

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

Till

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

duplicate referenced node in SimpleDatatypes.casl

enhance Web interface with SPASS (%implied, consistency)

translation of proofs along comorphisms (it this necessary at all???)

use inverse morphism?

leads to translation of G_theory along comorphism that also

keeps proof status info

this may be used in GUI prover interfaces for recovering old proof attempts

and offering them as default

proveCMDLinteractive (PGIP)

Model expansion flag for comorphisms

Umlaute in daVinci anzeigen

Fragen an Michael:

werden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?

was ist dort eigentlich das Problem?

Codierung von Subsorten?

paper with Paolo

semantic adequecy of HOL translation

Regulate concurrent proving

.dg files: store only current library; import .dg files for other libraries

Markus' Bsp:

Isabelle: use meta-quantifiers

local subsumption ?

better syntax (Tina)

check for proved theorems

AbstractGraphView: switch to Result monad

unite or rename consCheck and cons_checkers

BinInt.casl: revealing in Int1 does not work correctly

from Stefan W�lfl:

computeTheory does not work across library imports

local theorems

all nodes named

hierarchical Isabelle theories

daVinci printing is not adequate

hiding of internal nodes does not work

CSPs

----

FOL without quantifiers and with uniform disjunctions

(i.e. x R1 y \/ x R2 y)

(with and without =)

algorithmic path consistency over a relation algebra

plug in reasoner for this

develop correctness results (algorithmic path consistency=path consistency)

within CASL

CASL sublogics:

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

FOL without quantifiers (with and without =)

guarded fragment

Prop

[from DOLCE cooperation:

quit wish!

ontology mediation via pushouts/pullbacks/pulations

Robinson consistency with shared theory constructed via pre-image?

show theorem links between same instances of different parameterized

specs (where one is an extension of the other one)

link menu for %implies, $def, %cons, even without open proof obligation

for a proved theorem, show minimal part of DG needed for proof

cons, def, mono for nodes

Isabelle interface: each qed should write proof info into file

globally display nodes containing symbols mapped "twice" (i.e. via

different signature morphisms)

and add a menu for each node allowing for tracking the different

uses of the symbols/concepts

topsort coding: partial functions as relations?

]

theorem link menu for proof obligations

UserManual/Chapter7.casl: local thm link starting from Monoid leads to type error

in Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms

correctly.

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

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

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