todo revision 63f59fcd2200f9f145c539715f7452257263cba1
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowski************************************************
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowski************************************************
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowskiremove typedecls and op decls generated for datatypes
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowskiset up default simplifier
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowskiset up default tactics using axioms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowskirename variables that conflict with operation syntax
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowski (or restrict mixfix decls for consts)
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowskidie Mixfix-Deklarationen f�hren noch zu Problemen.
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowskif�hrt dazu, dass c nicht mehr als Variable verwendet werden kann.
871c48ec491643e87526b5f24c5ba255fa025027Till MossakowskiK�nntest du diese Mixfix-Deklarationen auf die notwendigen F�lle
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowskibeschr�nken, und ggf. die Variablen umbenennen?
871c48ec491643e87526b5f24c5ba255fa025027Till MossakowskiZudem m�ssen Underscores escaped werden:
871c48ec491643e87526b5f24c5ba255fa025027Till Mossakowski C_1::t ("C'_1")
bea5761c310012308382aa6df7cd80d1f3acc0bcTill MossakowskiDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
0b54df32e275652e0d01cf0b16d2401377526539Till MossakowskiInterface Hets <-> ISabelle
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski Hets muss eine Pipe als Inode erzeugen
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski und dann auf Beweisterme warten
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski und auf "Ende" warten
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski und dann Proof_status sen proof_tree entsprechend ausf�llen
0b54df32e275652e0d01cf0b16d2401377526539Till MossakowskiIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski Beweisterme (siehe Kapitel im RefMan)
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski ML "proofs := 1" (am Anfang des .thy file)
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski am Ende jedes Theorems: Beweisterm in die Pipe schreiben
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski mit pretty_proof_of und Pretty.string_of
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski und Start- und Endmarker
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski am Schluss "Ende" ausgeben
0b54df32e275652e0d01cf0b16d2401377526539Till MossakowskiFunktion basicInferenceNode in Proofs/Proofs.hs:
0b54df32e275652e0d01cf0b16d2401377526539Till Mossakowski Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
0b54df32e275652e0d01cf0b16d2401377526539Till MossakowskiEmacs: uni/emacs, George fragen (ger@)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
8ed1701f25192197c44291a6929653bf377cba2fTill Mossakowski use save button for saving proof info
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskidevelopment graph calculus
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- Stack overflow for "show just subtree"
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- view-test7.casl should be provable with globDecomp + locDecopm
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski- fail when doing first globDecomp, then local decomp in RelationsAndOrders
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowski- correct MAYA: glob decomp: some links are not found (Jorina)
b0ff5ad663224c8d9ca6017e6d598d9bc5fdbd77Till Mossakowski- Fail: No match in record selector Static.DevGraph.dgn_sign
b0ff5ad663224c8d9ca6017e6d598d9bc5fdbd77Till Mossakowski for local subsume in RelationsAndOrders
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitype check for CASL
e927ace91d729fa35f6b1d08faf84af28cd139e9Till Mossakowski*** Error encode.casl:8.30, No correct typing for
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiport CCC to Haskell
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiFunktionen imageOfMorphism und inhabited
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski mit "cvs add SigFuns.hs" einchecken
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski"free datatypes and recursive equations are consistent"
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskicheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiJust True => Yes, is consistent
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiJust False => No, is inconsistent
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiNothing => don't know
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowskicall the symbols in the image of the signature morphism "new"
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski- each new sort must be a free type,
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski i.e. it must occur in a sort generation constraint that is marked as free
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski (Sort_gen_ax constrs True)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski if not, output "don't know"
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski and there must be one term of that sort (inhabited)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski if not, output "no"
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski- group the axioms according to their leading operation/predicate symbol,
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski i.e. the f resp. the p in
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowski forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski Implication Application Strong_equation
2d6b942b2d10709143b699783f38957d8856e67fTill Mossakowski forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till Mossakowski Implication Predication Equivalence
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski if there are axioms not being of this form, output "don't know"
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskicheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskicheck' [] = ([([],[])],emptyUniqSet)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskicheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskicheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | all_vars ps = (pats, addOneToUniqSet indexs n)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski (pats,indexs) = check' rs
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- falls ein Konstruktor dabei ist: split_by_constructor
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskicheck' qs@((EqnInfo n ctx ps result):_)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | all_vars ps = ([], unitUniqSet n)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | constructors = split_by_constructor qs
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | only_vars = first_column_only_vars qs
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski | otherwise = panic "Check.check': Not implemented :-("
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski -- Note: RecPats will have been simplified to ConPats
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski -- at this stage.
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski constructors = or (map is_con qs)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski only_vars = and (map is_var qs)
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowskisubsort definitions: are conservative if formula is satisfiable
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowski (generate proof obligation)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
aa6f6fa09091e92016598584162b9ba909af48ccTill MossakowskiOWL-DL -> CASL
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski-------------------------------------------------------------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLaTeX pretty printer
b303a3717d229b102bca29e58d9e38c2f91fd233Christian Maedereine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskif�r die CASL Datentypen zu bekommen.
f3a84cc409ed345569be6673d05072dcb4291ebeTill MossakowskiHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskigenerate infrastructure for circular coinduction
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiCCS example: commutativity of || by coinduction
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
63f59fcd2200f9f145c539715f7452257263cba1Lutz SchröderRecursion does not compile due to clashes between built-in
63f59fcd2200f9f145c539715f7452257263cba1Lutz Schrödervariances (-->? vs. ->? in subtype declaration)
63f59fcd2200f9f145c539715f7452257263cba1Lutz Schrödernon-free/generated datatype declarations generate ga-axioms
b303a3717d229b102bca29e58d9e38c2f91fd233Christian Maederlogic coding form the comand line with printing of results
0d42a1490aa92c24b19823f745104eefbf29675dChristian MaederHaskell modules: hiding, renaming
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski- group the axioms according to their leading operation/predicate symbol,
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski i.e. the f resp. the p in
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski if there are axioms not being of this form, output error
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiMissing points for heterogeneous WADT 04 example:
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski- improve display of HasCASL sigs + mors
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis for HasCASL
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder checking class constraints of terms
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder pattern analysis for program equations
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder - for simple types (currently type synonyms)
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder symbol representation
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder symbol map analysis (hiding sub/supertypes)
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederWeak amalgamation analysis?
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederInstantiate Transformation Application system for HasCASL?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProofs in HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiCoding of subsorts as unary predicates (for ontologies)
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRecognize guarded fragment of CASL:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | exists x . At(x) /\ G
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBeweise in Isabelle
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (Vorbild: Larch-Handbuch)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiParser and static analysis for CSP-CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsaWin: support CASL-libraries
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiBuffer.het, sublogic of node Buffer:
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till MossakowskiFail: illegal node type in sublogic computation
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till MossakowskiJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowskispec VarTestIncorrect =
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowski vars x:s; y:t
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowski forall x:t; y:s
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowskispec VarTestCorrect =
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowski %% vars x:s; y:t
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowski forall x:t; y:s
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till MossakowskiIncorrect geht durch, weil die Typanalyse nicht funktioniert und Correct
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowskiwird abgelehnt, weil x und y nicht denselben Typ haben, was das richtige
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till MossakowskiVerhalten auch im ersten Fall w\x{00E4}re.
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskifor CSP-CASL example: with logic
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskiheterogeneous static ana
601f11cf0b4164a6a718038a736ae3d579f3a27cTill Mossakowskitheorem links between nodes in different libraries
7ed2a775680fb1a29e6907d372124906b7746420Till MossakowskibasicProofs: use info about used axioms
7ed2a775680fb1a29e6907d372124906b7746420Till Mossakowski ensure that axiom/thm names are unique
8980a8c8137a3a4c69bf9fdb3eca5b4b7f6e69c9Till MossakowskiOverload / inlineAxioms: injections
85ab61b931e22a72a53628b8aa5d059eeaedf1bdTill Mossakowskiremove "prove" menu in abstracted dg
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskibetter sublogic analysis in codings
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskithy files in subdir
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiadjust path for thy files, such that hets can also be started from subdirs
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiRestrict Sonjas simplifications to HasCASL
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiadd suitable axioms to simplifier and CR
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskicomputeTheory: remove double axioms
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiadd suitable axioms to simplifier and classical reasoner
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskibetter display of internal nodes (use tooltip?)
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowskiupdate Hets, CASL, daVinci on web page
60082d649e5bbb1c54f73f8921c3c390170e6c46Till MossakowskiCASL2PCFOL: x_i -> t_i, t=[inj(x_i)]
950ecce40ed5a97adf4460be07b47e3a0d0b1e56Till Mossakowskipacking of binaries: add hets-update, refer to TclTk
3e2c4de10a0eb284938b5d5307d1c1fc2f799456Till Mossakowskitest for sublogic before applying comorphism
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- coding to Isabelle: translate sort gen constraints
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowski- Improve adapation to Isabelle's lexis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle: (ask Christoph)
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski remove datatypes from sort list
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski prove local thm link (=> green)
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski "prove" menu with choice windows
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski incorporate sublogics
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowski sublogic translation table
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski better interaction between Isabelle instance (for one node)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski + selection of single goals that are proved
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski => use PGIP interface (Christoph, David)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski correct show theory
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski Keep proofs and lemmas in .thy files (kind of merge)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski CASL-like syntax
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski CASL annotation for lemmas that should be used in proof
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski inherit CASL's mixfix syntax
04d17d4f8862860f968f6b72b902163aacda6343Till MossakowskiSignatures versus theories: where to store additional infos?
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskicomp(id,x)=x for comorphism names
2d76902bf3b380a32268ccc0d2cd9e376988a060Till MossakowskiGeneralise CASL2Modal
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiMixfix analysis + typecheck for modality axiomatizations
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiModal logics: modal logic, temporal logic, mu calculus
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski+ translations (e.g. modal to FOL)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiCASL->Haskell with free DTs (mark sortgens) + recursion
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- List[Dec] wird List[Pos]
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- George wg. Schlie�en von Fenstern
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- node numbers do not match
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- thm links with external target should be provable as well
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRemove warnings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDifferent types of logic translations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImprove Static analysis of structured specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph calculus, Strategies for DG rules
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiManagement of change
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegrate provers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Otter model checker
2ee1615e999c5e0c49508ed4fcced7344b050042Till Mossakowski FOL-prover by Uli Furhbach
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
f69658e57cba7ecb37c0d84181f4c563215c2534Till Mossakowski Isabelle codings: www.inf.ethz.ch/~vigano
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Renate Schmidt, Manchester: uses FOL prover for description logic
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (as efficient as DL-specific tools!)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Look at PROSPER toolkit
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski consistency: see IJCAR-workshop on non-provability in Cork
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski IJCAR workshop about logical frameworks and meta-languages
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKlaus' wayfinding example
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till Mossakowskiask Detlef: critical pairs, Fossacs paper by Francesco
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUniForM workbench:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifirst steps towards CASL instance, using ATerms and re-using MMISS instance
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Grothendieck logic)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski + for TAS: reflection of HOL in HOL, to be composed with encodings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (i.e. signatures, axioms, signature morphisms in HOL,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski re-use ML signatures) (Einar)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDisplay Specs as daVinci subgraphs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUser interface
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski--------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogic graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInput text window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDevelopment graph window
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProver windows
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiHets 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)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPackaging of installation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGUI (vgl. VSE)
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski with Eclipse, WXHaskell or GTk?
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski how to integrate with event system of UniForM workbench?
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski this interacts with GUI!
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiData.Serizable (only when ghc supports it)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiincrease performance
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiintegrate QuickCheck: come to lecture!
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRemaining things
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski++++++++++++++++++++++++++++++++++++++++++++++++
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Coq, PTT in Maude
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiProofs with basic datatypes
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVerbesserung der Fehlermeldungen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImprove encoding: CATS/basic_encode.sml (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiExample of Agnes und Frank: proofs in HOL-CASL (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiExamples for cond rewriting -> Christophe
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncoding of structured free (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEncoding of structured cofree (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEingabesyntax als Mix zwischen CASL und HOL (3 days)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdapt Isabelle unions to CASL unions (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsaWin git/src/isa_ext/casl_thy.sml (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGenerate Proof obligations (1 week)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAdd renaming to Isabelle kernel (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRepository mit korrekten und fehlerhaften Specs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHetCATS User manual, Doku fuer Environments (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiComparsion of parsers (ML-yacc parser, SDF-Parser)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPVS anbinden (Kooperation mit Cachan?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPortations: Intel-Solaris, Mac OS-10 (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiViews on CASL specs: CATS/viewer.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModule graph CATS/module_graph.sml (1 week) -> Maya?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiATerms via XML: CATS/aterms.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLibrary management: CATS/lib_ana.sml (2 weeks)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski{- This does not work due to needed ordering:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Functor Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski fmap = mapSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiinstance Monad Set where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski return = unitSet
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski m >>= k = unionManySets (setToList (fmap k m))
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau von comptable
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski--------------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski[("normal","normal","normal"),
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski ("normal","inclusion","normal"),
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski ("inclusion","normal","normal"),
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski ("inclusion","inclusion","inclusion")]
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau von ginfo
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski--------------------
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiMit initgraphs erzeugen
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiAufbau des Graphen selbst
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski------------------------