256N/APlan and priority list for CoFI tool activities

256N/A

256N/A************************************************

256N/AImmanuel

256N/A************************************************

256N/ASuchfunktion f�r einen Knoten im DG:

256N/A welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?

256N/A erstmal auf eine Logik (z.B. CASL) beschr�nken

256N/A - Funktion f�r Morphismus-Suche zwischen Theorien

256N/A - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty

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

256N/A - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)

256N/A

256N/ABasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?

256N/AKonfidenzgrade von Beweisen?

256N/A

256N/Avon Till/HiWi zu erledigen:

256N/ARepr�sentation �ndern:

256N/A Beweisobjekte an DGs, nicht an Regeln -- done

256N/A F�r Theoreme in Theorien an Beweisobjekte -- done

256N/A BasicProof mit Liste von Beweisobjekten -- �berfl�ssig

256N/A Definitionen auszeichnen -- done

256N/A F�r alles siehe G_theory, ThSens und SenStatus.

256N/A Isabelles Beweisobjekte einbinden

256N/A

256N/A

256N/A************************************************

256N/ARazvan (Till)

256N/A************************************************

256N/A

256N/AIntegration with PGIP

256N/A Hets needs to be equipped with a command-line interface that reads in

256N/A specification libraries and proof commands

256N/A Proof commands are special annotations in the libraries

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

256N/A when stepping through the specs, dg calculus generates proof obligations

256N/A (for the current dg node only),

256N/A which then can be discharged by Isabelle, SPASS etc.

256N/A That is, the proof commands always occur at the position in the text

256N/A that generates the dg node?!? or should they occur after each specification?

256N/A needs incremental parsing and static analysis for Hets libraries

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

256N/A more challenging: incrementally parse and analyse also individual specifications

256N/A

256N/A************************************************

256N/AAnton (Till)

256N/A************************************************

256N/A

256N/AModal-CASL <-> CASL-DL

256N/A see Chapter 4 of "The Description Logic Handbook"

256N/A and ask Klaus for a print out of it

256N/A

256N/Aimprove Modal-CASL

256N/A possibly also modal logic in CoCASL

256N/A

256N/A**************** task A ************************

256N/A

256N/AProofs with Isabelle and SPASS

256N/ACASL basic datatypes

256N/AHasCASL examples

256N/A- improve simplifier for partiality in Isabelle coding

256N/A program interaction between solver, subgoaler and simplifier in such a way

256N/A that proofs of definedness conditions are postponed

256N/A

256N/A

256N/A

256N/A

256N/A************************************************

256N/AFlorian (Till)

256N/A************************************************

256N/A

256N/ABremer Constraint-Solver angucken

256N/AShi Hui wegen Anwendungen kontaktieren 1. Juni

256N/ALiteratur �ber DCC und RCC8 lesen bis Mitte Juni

256N/AMitte/Ende Juni: Outline der Diplomarbeit

256N/A Qualitative Constraint-Kalk�le (siehe Thomas)

256N/A CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:

256N/A the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)

256N/A CASL-Formeln nur ganz kurz

256N/A ConstraintCASL

256N/A Signaturen, Signaturmorphismen (aus CASL)

256N/A Modelle (aus CASL)

256N/A Formeln

256N/A Erf�lltheit von Formeln

256N/A optional: Erf�lltheitsbedingung

256N/A M |= sigma(phi) <=> M|_sigma |= phi

256N/A f�r Signaturmorphismus sigma:Sigma_1->Sigma_2

256N/A M \in Mod(Sigma_2), phi\in Sen(Sigma_1)

256N/A Formalisierung von Kalk�len in ConstraintCASL

256N/A Constraint-Solver (auch in ihren Eigenheiten)

256N/A �bersetzungen zwischen den verschieden Formaten

256N/A praktischer Vergleich

256N/A Anwendung

256N/A�bersetzungen bis 30.Juni

256N/A ConstraintCASL -> Bremer Solver

256N/A CASL/ComputeTable

256N/A Bremer Solver -> ConstraintCASL

256N/A Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers

256N/A parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt

256N/A Das kann das als Option in Hets eingebunden werden (Christian Maeder)

256N/AFreiburger Constraint-Solver angucken im Juli

256N/A�bersetzungen bis 31. Juli

256N/A ConstraintCASL -> Freibuger Solver/XML-Format

256N/A CASL/ComputeTable

256N/A Option: comptable.xml

256N/A Freibuger Solver/XML-Format -> ConstraintCASL

256N/A

256N/A************************************************

256N/AHendrik (Till)

256N/A************************************************

256N/A

256N/Awerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der

256N/A sie als erstes eingef�hrt wurden?

256N/A checken f�r Library-Importe

256N/A

256N/AOMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden

256N/A

256N/AHiding: unterschiedlich in OMDoc und Hets

256N/Aein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als

256N/A Signaturmorphismus

256N/A wird �bersetzt in einen OMDoc-Theoriemorphismus

256N/A mit leerer/identischer Abbildung, bei dem die Symbole aus

256N/A Sigma_2 \ Sigma_1 versteckt werden

256N/A Wenn der Signaturmorphismus keine Inklusion ist, ist keine

256N/A �bersetzung m�glich -> Fehler

256N/Aein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist

256N/A (also leere bzw. identische Abbildung) wird �bersetzt

256N/A in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus

256N/A falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss

256N/A ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,

256N/A der dann die Umbenennung macht, erzeugt werden

256N/A

256N/ALogiken: �ber verschiedene OMDoc-Theorien mit URI

256N/A

256N/A

256N/A

256N/A************************************************

256N/AMingyi (Till)

256N/A************************************************

256N/A

256N/ADiplomarbeit

256N/A- CASL-Logik: "Relating CASL with other specification languages", S.401-408

256N/A- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz

256N/A siehe CASL reference manual (suche nach conservative)

256N/A- warum sind konservative Erweiterungen wichtig?

256N/A - um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert

256N/A werden k�nnen

256N/A - f�r Refinement-Beweise

256N/A- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,

256N/A definitional oder monomorph sind

256N/A - Beschreibung des Algorithmus in Pseudocode

256N/A - Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus

256N/A als konservativ erkennt, muss f�r jedes Modell der kleineren

256N/A Spezifikation eine Modellerweiterung zur gr��eren Spezifikation

256N/A gefunden werden. Z.B. im Falle von free types kann dies eine

256N/A Termalgebra-Konstruktion sein.

256N/A SP1 -- \sigma --> SP2

256N/A konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem

256N/A SP2-Modell M2 mit M2|_\sigma=M1.

256N/A

256N/Aport CCC to Haskell

256N/A

256N/AFunktionen imageOfMorphism und inhabited

256N/A von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs

256N/A mit "cvs add SigFuns.hs" einchecken

256N/A

256N/ANew module FreeTypes.hs:

256N/A

256N/A"free datatypes and recursive equations are consistent"

256N/A

256N/AcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool

256N/AJust True => Yes, is consistent

256N/AJust False => No, is inconsistent

256N/ANothing => don't know

256N/A

256N/Acall the symbols in the image of the signature morphism "new"

256N/A

256N/A- each new sort must be a free type,

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

256N/A (Sort_gen_ax constrs True)

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

256N/A if not, output "don't know"

256N/A and there must be one term of that sort (inhabited)

256N/A if not, output "no"

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

256N/A i.e. the f resp. the p in

256N/A forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t

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

256N/A Implication Application Strong_equation

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

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

256N/A Implication Predication Equivalence

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

256N/A

256N/A

256N/A

256N/A

256N/Acheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)

256N/Acheck' [] = ([([],[])],emptyUniqSet)

256N/A

256N/A-- nur ein Pattern, bestehend aus nur Variablen? fertig, True

256N/Acheck' [EqnInfo n ctx ps (MatchResult CanFail _)]

256N/A | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)

256N/A

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

256N/Acheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)

256N/A | all_vars ps = (pats, addOneToUniqSet indexs n)

256N/A where

256N/A (pats,indexs) = check' rs

256N/A

256N/A-- falls ein Konstruktor dabei ist: split_by_constructor

256N/A-- wenn die ersten Argument nur Variablen sind: first_column_only_vars

256N/Acheck' qs@((EqnInfo n ctx ps result):_)

256N/A | all_vars ps = ([], unitUniqSet n)

256N/A | constructors = split_by_constructor qs

256N/A | only_vars = first_column_only_vars qs

256N/A | otherwise = panic "Check.check': Not implemented :-("

256N/A where

256N/A -- Note: RecPats will have been simplified to ConPats

256N/A -- at this stage.

256N/A constructors = or (map is_con qs)

256N/A only_vars = and (map is_var qs)

256N/A

256N/A

256N/Asubsort definitions: are conservative if formula is satisfiable

256N/A (generate proof obligation)

256N/A

256N/A************************************************

256N/AHeng (Klaus)

256N/A************************************************

256N/A

256N/AOWL-DL logic

256N/AOWL-DL (<)-> CASL-DL

256N/A

256N/Aemacs mode:

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

256N/A some operation symbols

256N/A show hets output immediately

256N/A C-c C-g for hets -g

256N/A when hets terminates abnormally (e.g. with a fail), emacs loops

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

256N/A in such a way that the error is at the top (for long error lists)

256N/A Version for XEamcs?

256N/A

256N/A should work with parser error messages as well (adapt these?)

256N/A

256N/A************************************************

256N/AKen (Till)

256N/A************************************************

256N/A

256N/Adevelopment graph calculus

256N/A(see Sect. IV:4.4 of the CASL Reference Manual)

256N/A

256N/Alook at Static/DevGraph.hs

256N/Alook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs

256N/A

256N/Atest development graph GUI:

256N/A global decomposition

256N/A menu edit - unnamed nodes - hide/show nodes,

256N/A node menu: show just subtree / undo

256N/A interaction with edit - proofs - automatic?

256N/A

256N/Arestrict proofs: only one prove window per node at a given time

256N/A

256N/Aimplement simplified rule Theorem-Hide-Shift

256N/Atry out examples

256N/Aconservativity calculus

256N/Aweakly amalgamable cocones

256N/A

256N/A

256N/A************************************************

256N/Afurther task 1

256N/A************************************************

256N/A

256N/A

256N/A************************************************

256N/Afurther task 2

256N/A************************************************

256N/A

256N/AUni-Refactoring,

256N/A

256N/Amake modules hierarchical, change scoped type variables for ghc-6.5

256N/A(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),

256N/Ause HaXml as a cabalized library, provide uni as (one?) cabal

256N/Apackage(s), uni used to work under windows as well, watch the

256N/Ai.e. FilePath, Process discussions (libraries@haskell.org)

256N/A

256N/Apossibly switch to a subversion repository, talk to Achim

256N/A(amahnke@tzi.de)

256N/A

256N/A************************************************

256N/Afurther task 3

256N/A************************************************

256N/Alook fgl/Data/Graph/Inductive/Graph.hs

256N/Alook at Static/DevGraph.hs

256N/A

256N/Achange management

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

256N/A reload macht folgendes:

256N/A lade CASL-Datei neu ==> neuer Entwicklungsgraph

256N/A vergleiche alten+neuen Entwicklungsgraph, konstruiere eine

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

256N/A (jeweils eine Abblidung f�r Knoten und eine f�r Kanten)

256N/A Kriterien f�r Finden der Knotenabbildung:

256N/A - Namen

256N/A - DGOrigin

256N/A - Signatur

256N/A

256N/Aeinfaches Merge von lokalen Beweisen eines abgespeichteren DG

256N/A in aktuellen DG

256N/A

256N/A************************************************

256N/Afurther task 4

256N/A************************************************

256N/A

256N/Agraph of Haskell module dependencies

256N/A using .import files

256N/A

256N/A************************************************

256N/Afurther task 5

256N/A************************************************

256N/A

256N/Aport hets to windows. -- costs too much energy at this stage! Till

256N/A

256N/AIf hets should become successful then requests for support under

256N/Awindows will surely follow.

256N/A

256N/AGhc, uni and uDrawGraph should work under windows. Only Isabelle does

256N/Anot exist for windows, but SPASS does. Probably only a few path

256N/Acomputations need to be adapted (made modular) within hets. Also

256N/Aposition computations (of Parsec) should be checked under windows.

256N/A

256N/A************************************************

256N/Afurther task 6

256N/A************************************************

256N/A

256N/Arefactor pretty printing

256N/A

256N/Aeine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex

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

(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)

Datentypen (particularly for HasCASL data types) zu bekommen.

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

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

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)

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

(read documentation for XPath)

use either XPath or Haifas xmlify stuff for

full parsing of rdf-objects returned by MathServ

putting this stuff into a data-structure: MathServResponse

map/transform MathServResponse into Proof_status

(intermediate datastructure makes parser independent from Proof_status)

change proof_tree to String and save TSTP to it

SPASS proof between "^Here is a proof" and "^Formulae used"

later

SPASS Proof must be parsed and translated to TSTP

(Klaus checks for this functionallity in MathServ)

types for Service and Soap Operation instead of Strings

tactic_script activities

parser for SPASS commandline

parsed into [SPASS.Sign.SPSetting]

format of tactic_script and parser for MathServBroker and

individual MathServ reasoners

include current options into saved DFG file (saved from GUI)

(s. SPASS.CreateDFG)

include current options as comment into saved TPTP file (saved from GUI)

and also the requested prover or "[via Broker]"

Name of the real prover should be in the prover_name of Proof_status

if the Broker was used but "<name> [via MathServBroker]" should be

the end of the prover name

SPASS encoding improvements in SPASS.Conversions/Comorphisms.CASL2SPASS

- if there is only one sort in the signature eliminate it

special case: (freely) generated sorts are not eliminated

new flag in SPASS sign: singleSorted

Sentences are modified in CASL2SPASS

all variable declarations have to consider the flag

(quantified formulas) variable lists without types

Formula/Term specific

- F:sort membership ==> true

- T:explicit cast is omitted

- T:explicit typing of terms is omitted

typings in the signature have to be removed in SPASS.Conversions

empty declarations list

SPASS encoding improvements in CASL2SPASS

- if there are predicates defined upon equality substitute them with equality

and remove them from the signature

find definitions (Equivalences) where one side is a binary predicate

and the other side is a builtin equality application (Strong_equation)

return the full qualified (with type) predicate(s)

this is done before the translation of the signature/sentences happens

remove symbol from signature and mark it in the idMap as equality

(involves adding a flag to SPASS.Utils.CPred)

display of tactic_scripts in GUI.ProofManagement

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

Klaus

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

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

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

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