5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsPlan and priority list for CoFI tool activities

11e9368a226272085c337e9e74b79808c16fbdbaTinderbox User

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsImmanuel

4a14ce5ba00ab7bc55c99ffdcf59c7a4ab902721Automatic Updater************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsSuchfunktion f�r einen Knoten im DG:

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews - Funktion f�r Morphismus-Suche zwischen Theorien

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsKonfidenzgrade von Beweisen?

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

ea94d370123a5892f6c47a97f21d1b28d44bb168Tinderbox Uservon Till/HiWi zu erledigen:

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsRepr�sentation �ndern:

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Beweisobjekte an DGs, nicht an Regeln -- done

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews F�r Theoreme in Theorien an Beweisobjekte -- done

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews BasicProof mit Liste von Beweisobjekten -- �berfl�ssig

e21a2904f02a03fa06b6db04d348f65fe9c67b2bMark Andrews Definitionen auszeichnen -- done

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews F�r alles siehe G_theory, ThSens und SenStatus.

cd32f419a8a5432fbb139f56ee73cbf68b9350ccTinderbox User Isabelles Beweisobjekte einbinden

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

9b469e3c59015b1a4899c9d8395168126fe094fdAutomatic Updater

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsFlorian (Till)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsabstrakte Syntax f�r ConstraintCASL (s. CASL-lib/ConstraintCASL/)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews nach HetCATS/ConstraintCASL/AS_ConstraintCASL.der.hs

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Range hinzuf�gen (vgl. HetCATS/CASL/AS_Basic.der.hs)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsParser f�r ConstraintCASL

9b469e3c59015b1a4899c9d8395168126fe094fdAutomatic Updater nach HetCATS/ConstraintCASL/Parse_AS_Basic.hs

9b469e3c59015b1a4899c9d8395168126fe094fdAutomatic Updater tokens aus Common/Lexer.hs wiederverwenden

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews neuer Parser f�r Terme

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsTesten mit

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews hets -o ast.het CASL-lib/ConstraintCASL/RCC8.het

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews trace verwenden

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews einfachen Test einchecken

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsFreiburger Constraint-Solver angucken

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsBremer Constraint-Solver angucken

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsHendrik (Till)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewswerden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?

b2f07642fd712c8fda81a116bcdde229ab291f33Tinderbox User

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewswerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews sie als erstes eingef�hrt wurden?

cd32f419a8a5432fbb139f56ee73cbf68b9350ccTinderbox User

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsHiding: unterschiedlich in OMDoc und Hets

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Signaturmorphismus

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews wird �bersetzt in einen OMDoc-Theoriemorphismus

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews mit leerer/identischer Abbildung, bei dem die Symbole aus

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Sigma_2 \ Sigma_1 versteckt werden

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Wenn der Signaturmorphismus keine Inklusion ist, ist keine

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews �bersetzung m�glich -> Fehler

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews (also leere bzw. identische Abbildung) wird �bersetzt

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews der dann die Umbenennung macht, erzeugt werden

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

cd32f419a8a5432fbb139f56ee73cbf68b9350ccTinderbox UserLogiken: �ber verschiedene OMDoc-Theorien mit URI

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsMingyi (Till)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsport CCC to Haskell

71c66a876ecca77923638d3f94cc0783152b2f03Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsFunktionen imageOfMorphism und inhabited

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews mit "cvs add SigFuns.hs" einchecken

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsNew module FreeTypes.hs:

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews"free datatypes and recursive equations are consistent"

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewscheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsJust True => Yes, is consistent

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsJust False => No, is inconsistent

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsNothing => don't know

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewscall the symbols in the image of the signature morphism "new"

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews- each new sort must be a free type,

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews (Sort_gen_ax constrs True)

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews if not, output "don't know"

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews if not, output "no"

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews i.e. the f resp. the p in

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

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Implication Application Strong_equation

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

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

b2f07642fd712c8fda81a116bcdde229ab291f33Tinderbox User Implication Predication Equivalence

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

b2f07642fd712c8fda81a116bcdde229ab291f33Tinderbox User

b2f07642fd712c8fda81a116bcdde229ab291f33Tinderbox User

b2f07642fd712c8fda81a116bcdde229ab291f33Tinderbox User

b2f07642fd712c8fda81a116bcdde229ab291f33Tinderbox User

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewscheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewscheck' [] = ([([],[])],emptyUniqSet)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

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

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

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewscheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews | all_vars ps = (pats, addOneToUniqSet indexs n)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews where

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews (pats,indexs) = check' rs

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews-- falls ein Konstruktor dabei ist: split_by_constructor

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews-- wenn die ersten Argument nur Variablen sind: first_column_only_vars

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewscheck' qs@((EqnInfo n ctx ps result):_)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews | all_vars ps = ([], unitUniqSet n)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews | constructors = split_by_constructor qs

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews | only_vars = first_column_only_vars qs

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews where

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews -- Note: RecPats will have been simplified to ConPats

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews -- at this stage.

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews constructors = or (map is_con qs)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews only_vars = and (map is_var qs)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewssubsort definitions: are conservative if formula is satisfiable

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews (generate proof obligation)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsHeng (Klaus)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsOWL-DL logic

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsOWL-DL (<)-> CASL-DL

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsemacs mode:

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews some operation symbols

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews show hets output immediately

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews C-c C-g for hets -g

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

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

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Version for XEamcs?

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsHilfskraft 1

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsModal-CASL <-> CASL-DL

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews see Chapter 4 of "The Description Logic Handbook"

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews and ask Klaus for a print out of it

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsimprove Modal-CASL

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews possibly also modal logic in CoCASL

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsHilfskraft 2

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsUni-Refactoring,

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsmake modules hierarchical, change scoped type variables for ghc-6.5

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsuse HaXml as a cabalized library, provide uni as (one?) cabal

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsi.e. FilePath, Process discussions (libraries@haskell.org)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewspossibly switch to a subversion repository, talk to Achim

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews(amahnke@tzi.de)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark AndrewsKen (Till)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsdevelopment graph calculus

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

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewslook at Static/DevGraph.hs

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewslook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

cd32f419a8a5432fbb139f56ee73cbf68b9350ccTinderbox Userfix bug: when lodaing Basic/RelationsAndOrders.casl and

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews doing 4x edit - proofs - Global Decomposition, we get

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews hets: applyChangesAux2: deleted edge from 3 to 15 of type GlobalThm

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews and origin DGProof of development graph does not exist in abstraction graph

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews look at Proofs/Global.hs, GUI/ConvertAbstractToDevgraph,

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews function applyChanges

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Hint: first try to cut down the example (find out the minimal

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews subpart that still leads to the error)

cd32f419a8a5432fbb139f56ee73cbf68b9350ccTinderbox User

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewstest development grapg GUI:

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews menu edit - unnamed nodes - hide/show nodes,

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews node menu: show just subtree / undo

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews interaction with edit - proofs - automatic?

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsimplement simplified rule Theorem-Hide-Shift

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewstry out examples

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsconservativity calculus

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewsweakly amalgamable cocones

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

cd32f419a8a5432fbb139f56ee73cbf68b9350ccTinderbox User************************************************

9b469e3c59015b1a4899c9d8395168126fe094fdAutomatic UpdaterZheng (Till)

9b469e3c59015b1a4899c9d8395168126fe094fdAutomatic Updater************************************************

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewslook fgl/Data/Graph/Inductive/Graph.hs

4abdfc917e6635a7c81d1f931a0c79227e72d025Mark Andrewslook at Static/DevGraph.hs

4abdfc917e6635a7c81d1f931a0c79227e72d025Mark Andrews

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrewschange management

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

9b469e3c59015b1a4899c9d8395168126fe094fdAutomatic Updater reload macht folgendes:

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews lade CASL-Datei neu ==> neuer Entwicklungsgraph

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews vergleiche alten+neuen Entwicklungsgraph, konstruiere eine

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

30c0c7470d5bfabd8f43c563f4eca636d06cc484Tinderbox User (jeweils eine Abblidung f�r Knoten und eine f�r Kanten)

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews Kriterien f�r Finden der Knotenabbildung:

5a4557e8de2951a2796676b5ec4b6a90caa5be14Mark Andrews - Namen

- DGOrigin

- Signatur

einfaches Merge von lokalen Beweisen eines abgespeichteren DG

in aktuellen DG

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

Hilfskraft 4

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

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.

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

Hilfskraft 5

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

refactor pretty printing

eine 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

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

correct CASL2Isabelle

(inconsistency due to coding of free datatypes)

graph of Haskell module dependencies

using .import files

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 (with wrongly qualified module names)

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

Missing points for heterogeneous WADT 04 example:

- improve display of HasCASL sigs + mors

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

Integration with PGIP

display specs + proofs in one buffer

when stepping through the specs, dg calculus generates proof obligations,

which then can be discharged by Isabelle

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

Rainer (Klaus)

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

Connecting Hets with MathServ

Either use

- haifa (http://www.dcs.shef.ac.uk/~simonf/HAIFA.html)

pros: * relies not on external tool

* light weight call

cons: * code is not well maintained

* a lot of the deserialization of the answer must be done

in Haskell

- call a java program included in MathServ distrib

pros: * works imediately

* deserilisation is mostly done in java

cons: * use of external tool

Use modified dfg2tptp to translate SPASS theories into TPTP problems

(ask Klaus for sources)

Add possibility to choose a prover out of a list of available provers

(similar to "More fine grained..." and behind more fine grained)

Adapt Comorphisms.KnownProvers to select a certain prover at the end of a

comorphism automatically

Adapt existing SPASS GUI to cover call of the MathServ broker

by - transforming the grid layout packer into the packer

used in GUI.ProofManagement (easier to maintain and to extend)

- abstraction of certain parts of the GUI into helper functions

forms a new generic Prover-GUI toolkit

- on top of this GUI toolkit

Write a GUI based on the generic Prover-GUI

to call MathServ's Vampire service directly

with additional parameters

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

Klaus

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

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

allgemeine Hets-GUI

f�r Anzeige von (un)bewiesenen Goals, ... done

bewiesene Goals als Axioms mit ausgeben ... was ist das ???

das ist schon implementiert ("Theorems to include if proven")

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

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

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