todo revision 2b9290308115cc5bda1684b07348f25e2b39ed50
97a9a944b5887e91042b019776c41d5dd74557aferikabelePlan and priority list for CoFI tool activities
97a9a944b5887e91042b019776c41d5dd74557aferikabele************************************************
a945f35eff8b6a88009ce73de6d4c862ce58de3cslive************************************************
a945f35eff8b6a88009ce73de6d4c862ce58de3csliveSuchfunktion f�r einen Knoten im DG:
b686b6a420bde7f78c416b90be11db94cb789979nd welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
b686b6a420bde7f78c416b90be11db94cb789979nd erstmal auf eine Logik (z.B. CASL) beschr�nken
b686b6a420bde7f78c416b90be11db94cb789979nd - Funktion f�r Morphismus-Suche zwischen Theorien
b686b6a420bde7f78c416b90be11db94cb789979nd - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
b686b6a420bde7f78c416b90be11db94cb789979nd RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
b686b6a420bde7f78c416b90be11db94cb789979nd - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
b686b6a420bde7f78c416b90be11db94cb789979ndBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
b686b6a420bde7f78c416b90be11db94cb789979ndKonfidenzgrade von Beweisen?
b686b6a420bde7f78c416b90be11db94cb789979ndvon Till/Jorina (jfgerken@tzi.de) zu erledigen:
b686b6a420bde7f78c416b90be11db94cb789979ndRepr�sentation �ndern:
b686b6a420bde7f78c416b90be11db94cb789979nd Beweisobjekte an DGs, nicht an Regeln
4b5981e276e93df97c34e4da05ca5cf8bbd937dand F�r Theoreme in Theorien an Beweisobjekte
b686b6a420bde7f78c416b90be11db94cb789979nd BasicProof mit Liste von Beweisobjekten
b686b6a420bde7f78c416b90be11db94cb789979nd Isabelles Beweisobjekte einbinden
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd Definitionen auszeichnen
cc8190433d13f5e9de618c5d7f10c824c0c1919cgryzor************************************************
7f5b59ccc63c0c0e3e678a168f09ee6a2f51f9d0nd************************************************
b686b6a420bde7f78c416b90be11db94cb789979ndeinfaches Merge von lokalen Beweisen eines abgespeichteren DG
b686b6a420bde7f78c416b90be11db94cb789979nd in aktuellen DG
b686b6a420bde7f78c416b90be11db94cb789979nd************************************************
b686b6a420bde7f78c416b90be11db94cb789979ndMingyi (Till)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive************************************************
06ba4a61654b3763ad65f52283832ebf058fdf1csliveport CCC to Haskell
b686b6a420bde7f78c416b90be11db94cb789979ndFunktionen imageOfMorphism und inhabited
b686b6a420bde7f78c416b90be11db94cb789979nd von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
b686b6a420bde7f78c416b90be11db94cb789979nd mit "cvs add SigFuns.hs" einchecken
b686b6a420bde7f78c416b90be11db94cb789979nd"free datatypes and recursive equations are consistent"
69d3d5f6232f961fd77392db8a975a346fd9cff6ndcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
b686b6a420bde7f78c416b90be11db94cb789979ndJust True => Yes, is consistent
b686b6a420bde7f78c416b90be11db94cb789979ndJust False => No, is inconsistent
b686b6a420bde7f78c416b90be11db94cb789979ndNothing => don't know
b686b6a420bde7f78c416b90be11db94cb789979ndcall the symbols in the image of the signature morphism "new"
c3a3c963ad3f5b4d816b66117406d4e793049119slive- each new sort must be a free type,
c3a3c963ad3f5b4d816b66117406d4e793049119slive i.e. it must occur in a sort generation constraint that is marked as free
c3a3c963ad3f5b4d816b66117406d4e793049119slive (Sort_gen_ax constrs True)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
c3a3c963ad3f5b4d816b66117406d4e793049119slive if not, output "don't know"
c3a3c963ad3f5b4d816b66117406d4e793049119slive and there must be one term of that sort (inhabited)
20e951959be9ae3d183d42bfce4d8a35b8efc154jim if not, output "no"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive- group the axioms according to their leading operation/predicate symbol,
3b58542e01ec69422f3086db5825a12fc77b726end i.e. the f resp. the p in
3b58542e01ec69422f3086db5825a12fc77b726end forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
3b58542e01ec69422f3086db5825a12fc77b726end forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
3b58542e01ec69422f3086db5825a12fc77b726end Implication Application Strong_equation
06ba4a61654b3763ad65f52283832ebf058fdf1cslive forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
3b58542e01ec69422f3086db5825a12fc77b726end forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
3b58542e01ec69422f3086db5825a12fc77b726end Implication Predication Equivalence
b686b6a420bde7f78c416b90be11db94cb789979nd if there are axioms not being of this form, output "don't know"
3e78df7c8027de6e02326dff46742413de0bfc03covenercheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
69d3d5f6232f961fd77392db8a975a346fd9cff6ndcheck' [] = ([([],[])],emptyUniqSet)
69d3d5f6232f961fd77392db8a975a346fd9cff6nd-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
69d3d5f6232f961fd77392db8a975a346fd9cff6ndcheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
69d3d5f6232f961fd77392db8a975a346fd9cff6nd | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
69d3d5f6232f961fd77392db8a975a346fd9cff6nd-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
69d3d5f6232f961fd77392db8a975a346fd9cff6ndcheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
69d3d5f6232f961fd77392db8a975a346fd9cff6nd | all_vars ps = (pats, addOneToUniqSet indexs n)
69d3d5f6232f961fd77392db8a975a346fd9cff6nd (pats,indexs) = check' rs
69d3d5f6232f961fd77392db8a975a346fd9cff6nd-- falls ein Konstruktor dabei ist: split_by_constructor
69d3d5f6232f961fd77392db8a975a346fd9cff6nd-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
69d3d5f6232f961fd77392db8a975a346fd9cff6ndcheck' qs@((EqnInfo n ctx ps result):_)
69d3d5f6232f961fd77392db8a975a346fd9cff6nd | all_vars ps = ([], unitUniqSet n)
69d3d5f6232f961fd77392db8a975a346fd9cff6nd | constructors = split_by_constructor qs
b686b6a420bde7f78c416b90be11db94cb789979nd | only_vars = first_column_only_vars qs
06ba4a61654b3763ad65f52283832ebf058fdf1cslive | otherwise = panic "Check.check': Not implemented :-("
3b58542e01ec69422f3086db5825a12fc77b726end -- Note: RecPats will have been simplified to ConPats
3b58542e01ec69422f3086db5825a12fc77b726end -- at this stage.
3b58542e01ec69422f3086db5825a12fc77b726end constructors = or (map is_con qs)
3b58542e01ec69422f3086db5825a12fc77b726end only_vars = and (map is_var qs)
3b58542e01ec69422f3086db5825a12fc77b726endsubsort definitions: are conservative if formula is satisfiable
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (generate proof obligation)
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endHeng (Klaus)
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endOWL-DL logic
3b58542e01ec69422f3086db5825a12fc77b726endOWL-DL -> CASL
3b58542e01ec69422f3086db5825a12fc77b726endemacs mode:
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
3b58542e01ec69422f3086db5825a12fc77b726end some operation symbols
06ba4a61654b3763ad65f52283832ebf058fdf1cslive show hets output immediately
3b58542e01ec69422f3086db5825a12fc77b726end C-c C-g for hets -g
3b58542e01ec69422f3086db5825a12fc77b726end when hets terminates abnormally (e.g. with a fail), emacs loops
3b58542e01ec69422f3086db5825a12fc77b726end C-n jumps to the next error, but the message windows is not always scrolled
3b58542e01ec69422f3086db5825a12fc77b726end in such a way that the error is at the top (for long error lists)
3b58542e01ec69422f3086db5825a12fc77b726end Version for XEamcs?
06ba4a61654b3763ad65f52283832ebf058fdf1cslive should work with parser error messages as well (adapt these?)
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endHilfskraft 1
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endModal-CASL <-> CASL-DL <-> OWL-DL
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endHilfskraft 2
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endMathServ-Anbindung
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endHilfskraft 3
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endUni-Refactoring
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd************************************************
3b58542e01ec69422f3086db5825a12fc77b726endHilfskraft 4
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726endEntwicklungsgraph-Kalk�l
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd************************************************
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdHilfskraft 5
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdLaTeX pretty printer
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdeine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdund andere Formate besser zu unterst�tzen und einheitlichen PP code
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdf�r die CASL Datentypen zu bekommen.
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd************************************************
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdremaining stuff
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd************************************************
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdset up default simplifier
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisdset up default tactics using axioms
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisd (see DOLCE sample files)
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdrename variables that conflict with operation syntax
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd (or restrict mixfix decls for consts)
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisddie Mixfix-Deklarationen f�hren noch zu Problemen.
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdf�hrt dazu, dass c nicht mehr als Variable verwendet werden kann.
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdK�nntest du diese Mixfix-Deklarationen auf die notwendigen F�lle
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdbeschr�nken, und ggf. die Variablen umbenennen?
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdZudem m�ssen Underscores escaped werden:
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd C_1::t ("C'_1")
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdInterface Hets <-> ISabelle
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd Hets muss eine Pipe als Inode erzeugen
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jim und dann auf Beweisterme warten
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jim und auf "Ende" warten
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jim und dann Proof_status sen proof_tree entsprechend ausf�llen
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Beweisterme (siehe Kapitel im RefMan)
b686b6a420bde7f78c416b90be11db94cb789979nd ML "proofs := 1" (am Anfang des .thy file)
b686b6a420bde7f78c416b90be11db94cb789979nd am Ende jedes Theorems: Beweisterm in die Pipe schreiben
b686b6a420bde7f78c416b90be11db94cb789979nd (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
b686b6a420bde7f78c416b90be11db94cb789979nd mit pretty_proof_of und Pretty.string_of
b686b6a420bde7f78c416b90be11db94cb789979nd und Start- und Endmarker
8de9acdcea53109461287090fe0069a665352833rbowen am Schluss "Ende" ausgeben
b686b6a420bde7f78c416b90be11db94cb789979ndFunktion basicInferenceNode in Proofs/Proofs.hs:
b686b6a420bde7f78c416b90be11db94cb789979nd Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
e0fe7c83f67461f3dc676d90661551edfa111be0covenerimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
06ba4a61654b3763ad65f52283832ebf058fdf1cslivedevelopment graph calculus
06ba4a61654b3763ad65f52283832ebf058fdf1cslive- Stack overflow for "show just subtree"
06ba4a61654b3763ad65f52283832ebf058fdf1cslive- view-test7.casl should be provable with globDecomp + locDecopm
f55f04901f45165baa5c10f49c35702cb6e5d520nd- fail when doing first globDecomp, then local decomp in RelationsAndOrders
f55f04901f45165baa5c10f49c35702cb6e5d520nd- correct MAYA: glob decomp: some links are not found (Jorina)
e0fe7c83f67461f3dc676d90661551edfa111be0covener- Fail: No match in record selector Static.DevGraph.dgn_sign
e0fe7c83f67461f3dc676d90661551edfa111be0covener for local subsume in RelationsAndOrders
e0fe7c83f67461f3dc676d90661551edfa111be0covener************************************************
e0fe7c83f67461f3dc676d90661551edfa111be0covener************************************************
e0fe7c83f67461f3dc676d90661551edfa111be0covenergenerate infrastructure for circular coinduction
e0fe7c83f67461f3dc676d90661551edfa111be0covenerCCS example: commutativity of || by coinduction
4cb65c31bc681540ea623e1cb2bdd09749fb8d7esf************************************************
e0fe7c83f67461f3dc676d90661551edfa111be0covener************************************************
e0fe7c83f67461f3dc676d90661551edfa111be0covenercollect the patches for programatica (or create a package)
e0fe7c83f67461f3dc676d90661551edfa111be0covener- conv (SN i p) = PN i (S p)
e0fe7c83f67461f3dc676d90661551edfa111be0covener+ conv (SN i p) = PN i (Sn (show i) p)
e0fe7c83f67461f3dc676d90661551edfa111be0covenerfixes translation error of Pair
e0fe7c83f67461f3dc676d90661551edfa111be0covenersimplification of HasCASL sentences (omit types)
e0fe7c83f67461f3dc676d90661551edfa111be0covenerLogic COL is a ruin (with wrongly qualified module names)
e0fe7c83f67461f3dc676d90661551edfa111be0covenerpretty printing mangles trailing and preceding annotations
a89e5b3f7630ff342d5e1e9a5d28c07ce1d0029bcovenerlogic coding from the comand line with printing of results
e71a4cb937081adb50d5673a1c083a5a7b1a1ab1poirier(started -v5)
e71a4cb937081adb50d5673a1c083a5a7b1a1ab1poirierHaskell modules: hiding, renaming
3b58542e01ec69422f3086db5825a12fc77b726end- group the axioms according to their leading operation/predicate symbol,
8de9acdcea53109461287090fe0069a665352833rbowen i.e. the f resp. the p in
8de9acdcea53109461287090fe0069a665352833rbowen forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
8de9acdcea53109461287090fe0069a665352833rbowen forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
8de9acdcea53109461287090fe0069a665352833rbowen if there are axioms not being of this form, output error
3b58542e01ec69422f3086db5825a12fc77b726endMissing points for heterogeneous WADT 04 example:
3b58542e01ec69422f3086db5825a12fc77b726end- improve display of HasCASL sigs + mors
3b58542e01ec69422f3086db5825a12fc77b726endStatic analysis for HasCASL
3b58542e01ec69422f3086db5825a12fc77b726end pattern analysis for program equations
3b58542e01ec69422f3086db5825a12fc77b726end implemented only atomic subtyping
8de9acdcea53109461287090fe0069a665352833rbowenWeak amalgamation analysis?
8de9acdcea53109461287090fe0069a665352833rbowenInstantiate Transformation Application system for HasCASL?
8de9acdcea53109461287090fe0069a665352833rbowenAutomatic generation of Haskell (for a HasCASL subset)
8de9acdcea53109461287090fe0069a665352833rbowenProofs in HasCASL
8de9acdcea53109461287090fe0069a665352833rbowen************************************************
8de9acdcea53109461287090fe0069a665352833rbowen************************************************
8de9acdcea53109461287090fe0069a665352833rbowenConnecting Hets with MathServ
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd - haifa (http://www.dcs.shef.ac.uk/~simonf/HAIFA.html)
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd pros: * relies not on external tool
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd * light weight call
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd cons: * code is not well maintained
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd * a lot of the deserialization of the answer must be done
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd - call a java program included in MathServ distrib
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd pros: * works imediately
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd * deserilisation is mostly done in java
8de9acdcea53109461287090fe0069a665352833rbowen cons: * use of external tool
8de9acdcea53109461287090fe0069a665352833rbowen Use modified dfg2tptp to translate SPASS theories into TPTP problems
3b58542e01ec69422f3086db5825a12fc77b726end (ask Klaus for sources)
3b58542e01ec69422f3086db5825a12fc77b726end Add possibility to choose a prover out of a list of available provers
3b58542e01ec69422f3086db5825a12fc77b726end (similar to "More fine grained..." and behind more fine grained)
2704de98885368683621b01c8f8f4e4b01557611takashi Adapt Comorphisms.KnownProvers to select a certain prover at the end of a
3b58542e01ec69422f3086db5825a12fc77b726end comorphism automatically
06ba4a61654b3763ad65f52283832ebf058fdf1cslive Adapt existing SPASS GUI to cover call of the MathServ broker
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd by - transforming the grid layout packer into the packer
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd used in GUI.ProofManagement (easier to maintain and to extend)
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd - abstraction of certain parts of the GUI into helper functions
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd forms a new generic Prover-GUI toolkit
d1348237b33bc1755b9f1165eea52317465a7671nd - on top of this GUI toolkit
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd Write a GUI based on the generic Prover-GUI
e71a4cb937081adb50d5673a1c083a5a7b1a1ab1poirier to call MathServ's Vampire service directly
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisd with additional parameters
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
3b58542e01ec69422f3086db5825a12fc77b726end************************************************
9744ea3da59d6e7b787c47853db57c324414a9edndTranslation between Achim's ontology data structure and CASL (in Hets)
9744ea3da59d6e7b787c47853db57c324414a9edndvisualization of "taxonomy" of CASL signatures
3b58542e01ec69422f3086db5825a12fc77b726end (subsorts = inheritance, unary preds = concepts, binary preds = relations)
3b58542e01ec69422f3086db5825a12fc77b726end last two ... partially done
3b58542e01ec69422f3086db5825a12fc77b726endallgemeine Hets-GUI
3b58542e01ec69422f3086db5825a12fc77b726end f�r Anzeige von (un)bewiesenen Goals, ... done
f34ee9017606cf677db8c6dc37cb60b3a0c5f6a1poirier bewiesene Goals als Axioms mit ausgeben ... was ist das ???
1ad1c5f9a82d056966dcca9c6108c5ace8eed446rbowenRecognize guarded fragment of CASL:
3b58542e01ec69422f3086db5825a12fc77b726end G ::= forall x . At(x) => G where At is a conjunction of atoms
1ad1c5f9a82d056966dcca9c6108c5ace8eed446rbowen | exists x . At(x) /\ G
da57d338b0977cbdc021606d3230194a8ad4a56cndJoost Visser wg. ATerms in Haskell => neues Repository
9744ea3da59d6e7b787c47853db57c324414a9ednd************************************************
06ba4a61654b3763ad65f52283832ebf058fdf1csliveMarkus, Lutz
da57d338b0977cbdc021606d3230194a8ad4a56cnd************************************************
da57d338b0977cbdc021606d3230194a8ad4a56cndBeweise in Isabelle
da57d338b0977cbdc021606d3230194a8ad4a56cndCASL consistency checker
da57d338b0977cbdc021606d3230194a8ad4a56cndWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
da57d338b0977cbdc021606d3230194a8ad4a56cnd (Vorbild: Larch-Handbuch)
da57d338b0977cbdc021606d3230194a8ad4a56cndSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdParser and static analysis for CSP-CASL
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisd************************************************
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisd************************************************
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimCASL consistency checker
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimIsaWin: support CASL-libraries
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jim************************************************
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jim************************************************
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimRegulate concurrent proving
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jim.dg files: store only current library; import .dg files for other libraries
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimMarkus' Bsp:
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimIsabelle: use meta-quantifiers
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimlocal subsumption ?
06ba4a61654b3763ad65f52283832ebf058fdf1cslivebetter syntax (Tina)
69d3d5f6232f961fd77392db8a975a346fd9cff6ndcheck for proved theorems
3b58542e01ec69422f3086db5825a12fc77b726endAbstractGraphView: switch to Result monad
dd2f29c187db35e7635ce67a83dddceb75be87a4minfrinunite or rename consCheck and cons_checkers
b686b6a420bde7f78c416b90be11db94cb789979ndBinInt.casl: revealing in Int1 does not work correctly
b686b6a420bde7f78c416b90be11db94cb789979ndfrom Stefan W�lfl:
b686b6a420bde7f78c416b90be11db94cb789979ndcomputeTheory does not work across library imports
b686b6a420bde7f78c416b90be11db94cb789979ndlocal theorems
3a6ae8b015850ba60719ed97ae549e27eee84f0drbowenall nodes named
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisdhierarchical Isabelle theories
b686b6a420bde7f78c416b90be11db94cb789979nddaVinci printing is not adequate
b686b6a420bde7f78c416b90be11db94cb789979ndhiding of internal nodes does not work
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisdFOL without quantifiers and with uniform disjunctions
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (i.e. x R1 y \/ x R2 y)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive (with and without =)
06ba4a61654b3763ad65f52283832ebf058fdf1cslivealgorithmic path consistency over a relation algebra
06ba4a61654b3763ad65f52283832ebf058fdf1cslive plug in reasoner for this
06ba4a61654b3763ad65f52283832ebf058fdf1cslive develop correctness results (algorithmic path consistency=path consistency)
3b58542e01ec69422f3086db5825a12fc77b726end within CASL
8de9acdcea53109461287090fe0069a665352833rbowenCASL sublogics:
8de9acdcea53109461287090fe0069a665352833rbowen---------------
8de9acdcea53109461287090fe0069a665352833rbowenFOL without quantifiers (with and without =)
8de9acdcea53109461287090fe0069a665352833rbowenguarded fragment
3b58542e01ec69422f3086db5825a12fc77b726end[from DOLCE cooperation:
3b58542e01ec69422f3086db5825a12fc77b726endontology mediation via pushouts/pullbacks/pulations
3b58542e01ec69422f3086db5825a12fc77b726endRobinson consistency with shared theory constructed via pre-image?
3b58542e01ec69422f3086db5825a12fc77b726endshow theorem links between same instances of different parameterized
3b58542e01ec69422f3086db5825a12fc77b726end specs (where one is an extension of the other one)
3b58542e01ec69422f3086db5825a12fc77b726endlink menu for %implies, $def, %cons, even without open proof obligation
8de9acdcea53109461287090fe0069a665352833rbowenfor a proved theorem, show minimal part of DG needed for proof
3a6ae8b015850ba60719ed97ae549e27eee84f0drbowencons, def, mono for nodes
8de9acdcea53109461287090fe0069a665352833rbowenIsabelle interface: each qed should write proof info into file
8de9acdcea53109461287090fe0069a665352833rbowenglobally display nodes containing symbols mapped "twice" (i.e. via
8de9acdcea53109461287090fe0069a665352833rbowen different signature morphisms)
3a6ae8b015850ba60719ed97ae549e27eee84f0drbowen and add a menu for each node allowing for tracking the different
3a6ae8b015850ba60719ed97ae549e27eee84f0drbowentopsort coding: partial functions as relations?
8de9acdcea53109461287090fe0069a665352833rbowentheorem link menu for proof obligations
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdBuffer.het, sublogic of node Buffer:
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdFail: illegal node type in sublogic computation
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
8de9acdcea53109461287090fe0069a665352833rbowenfor CSP-CASL example: with logic
8de9acdcea53109461287090fe0069a665352833rbowenheterogeneous static ana
3b58542e01ec69422f3086db5825a12fc77b726endtheorem links between nodes in different libraries
9744ea3da59d6e7b787c47853db57c324414a9edndbasicProofs: use info about used axioms
9744ea3da59d6e7b787c47853db57c324414a9ednd ensure that axiom/thm names are unique
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisdOverload / inlineAxioms: injections
8eb7c1fd1d6abcf2529dcb265573b194aba56794chrisdremove "prove" menu in abstracted dg
3b58542e01ec69422f3086db5825a12fc77b726endbetter sublogic analysis in codings
9744ea3da59d6e7b787c47853db57c324414a9edndthy files in subdir
9744ea3da59d6e7b787c47853db57c324414a9edndadjust path for thy files, such that hets can also be started from subdirs
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisdRestrict Sonjas simplifications to HasCASL
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisdadd suitable axioms to simplifier and CR
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisdcomputeTheory: remove double axioms
4c881d2fffa365e2e0c5e25eb1cf77f4f9406e44chrisdadd suitable axioms to simplifier and classical reasoner
9744ea3da59d6e7b787c47853db57c324414a9edndbetter display of internal nodes (use tooltip?)
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimupdate Hets, CASL, daVinci on web page
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimCASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimpacking of binaries: add hets-update, refer to TclTk
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimCCC interface
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimtest for sublogic before applying comorphism
cb87a91abb4084fe5fa5a53047aeb6dcf9094115jimMissing points for heterogeneous WADT 04 example:
4ae7c4126530196ebe64b20b21ed476850d509d4nd- coding to Isabelle: translate sort gen constraints
69d3d5f6232f961fd77392db8a975a346fd9cff6nd- Improve adapation to Isabelle's lexis
06ba4a61654b3763ad65f52283832ebf058fdf1csliveIsabelle: (ask Christoph)
06ba4a61654b3763ad65f52283832ebf058fdf1cslive remove datatypes from sort list
b686b6a420bde7f78c416b90be11db94cb789979nd prove local thm link (=> green)
b686b6a420bde7f78c416b90be11db94cb789979nd "prove" menu with choice windows
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd incorporate sublogics
4aa805f8500255bc52a4c03259fe46df10a1d07cyoshiki sublogic translation table
7f5b59ccc63c0c0e3e678a168f09ee6a2f51f9d0nd better interaction between Isabelle instance (for one node)
7f5b59ccc63c0c0e3e678a168f09ee6a2f51f9d0nd + selection of single goals that are proved
3b3b7fc78d1f5bfc2769903375050048ff41ff26nd => use PGIP interface (Christoph, David)
b686b6a420bde7f78c416b90be11db94cb789979nd correct show theory
b686b6a420bde7f78c416b90be11db94cb789979nd Keep proofs and lemmas in .thy files (kind of merge)
+ translations (e.g. modal to FOL)
Isabelle codings: www.inf.ethz.ch/~vigano
Integration of MAYA and Isabelle/HOL (global HOL-Coding of
(i.e. signatures, axioms, signature morphisms in HOL,
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)
Data.Serizable (only when ghc supports it) better: rely on pointer equality
Improve encoding: CATS/basic_encode.sml (3 days)
More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
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)
IsaWin git/src/isa_ext/casl_thy.sml (1 week)
Basic datatypes CASL-lib/Basic/basic.casl
Conversion ASF/SDF-Parser -> abstract syntax (in Haskell)
Views on CASL specs: CATS/viewer.sml (2 weeks)
Module graph CATS/module_graph.sml (1 week) -> Maya?
ATerms via XML: CATS/aterms.sml (2 weeks)
Library management: CATS/lib_ana.sml (2 weeks)