todo revision 68551c69c9e6c705898bb462a3faec5d0d981417
87d944bf70927764edf8ef69e46d3b4b8fa09131pquernaPlan and priority list for CoFI tool activities
82d2a5debc5a6ed2118ac5916d9ba36ad0b5d78btrawick************************************************
87d944bf70927764edf8ef69e46d3b4b8fa09131pquerna************************************************
424c1a743525e9c5008e29b39a99363723409a1dtrawickList.casl should go through
41f2764385330bfa0eb5843aa04f4e768577e2b0trawickrename clashing names
41f2764385330bfa0eb5843aa04f4e768577e2b0trawickset up default simplifier
41f2764385330bfa0eb5843aa04f4e768577e2b0trawickset up default tactics using axioms
41f2764385330bfa0eb5843aa04f4e768577e2b0trawick (see DOLCE sample files)
4375cabac8fc22b3717687ffdbce9bbdf095f255trawick************************************************
4375cabac8fc22b3717687ffdbce9bbdf095f255trawickSonja (Till)
39dbd3f60b93f5e0fbf46d9ae237f6742e113442pquerna************************************************
79b66e55c7b1034d9fd49e1f6af6e646bbce1ab2pquernarename variables that conflict with operation syntax
79b66e55c7b1034d9fd49e1f6af6e646bbce1ab2pquerna (or restrict mixfix decls for consts)
79b66e55c7b1034d9fd49e1f6af6e646bbce1ab2pquernadie Mixfix-Deklarationen f�hren noch zu Problemen.
89211a3153be8b03353c3bfbca45fed67cb80f0bpquernaf�hrt dazu, dass c nicht mehr als Variable verwendet werden kann.
89211a3153be8b03353c3bfbca45fed67cb80f0bpquernaK�nntest du diese Mixfix-Deklarationen auf die notwendigen F�lle
89211a3153be8b03353c3bfbca45fed67cb80f0bpquernabeschr�nken, und ggf. die Variablen umbenennen?
a14ccf0f7e9b44c6848334823542a1799577f669pquernaZudem m�ssen Underscores escaped werden:
43c24b7301a9df7014ce54c0bc55ac4754cf5b0dpquerna C_1::t ("C'_1")
a2e37e48efb113e8e4f9d9ca9c8286aaac6c936cpquernaDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
007ba11dc68651df7f872f35947ae82a595d9e02pquernaInterface Hets <-> ISabelle
25059ddf3044ffa8dd3432ab8e2f941023054407trawick Hets muss eine Pipe als Inode erzeugen
25059ddf3044ffa8dd3432ab8e2f941023054407trawick und dann auf Beweisterme warten
25059ddf3044ffa8dd3432ab8e2f941023054407trawick und auf "Ende" warten
25059ddf3044ffa8dd3432ab8e2f941023054407trawick und dann Proof_status sen proof_tree entsprechend ausf�llen
44ca834b970b454b844efb96f219bdf49fee71e5trawickIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)
eb8430fd3bc941c0b3ba8bba3884b7fc464bf458pquerna Beweisterme (siehe Kapitel im RefMan)
eb8430fd3bc941c0b3ba8bba3884b7fc464bf458pquerna ML "proofs := 1" (am Anfang des .thy file)
eb8430fd3bc941c0b3ba8bba3884b7fc464bf458pquerna am Ende jedes Theorems: Beweisterm in die Pipe schreiben
1f9e65264b1ff249fa071e6aae32c0bb52f9c634trawick (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
1f9e65264b1ff249fa071e6aae32c0bb52f9c634trawick mit pretty_proof_of und Pretty.string_of
1f9e65264b1ff249fa071e6aae32c0bb52f9c634trawick und Start- und Endmarker
fde88bb682426885c679198ee130d2d5a29e8c0fbnicholes am Schluss "Ende" ausgeben
fde88bb682426885c679198ee130d2d5a29e8c0fbnicholesFunktion basicInferenceNode in Proofs/Proofs.hs:
fde88bb682426885c679198ee130d2d5a29e8c0fbnicholes Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
fde88bb682426885c679198ee130d2d5a29e8c0fbnicholesEmacs: uni/emacs, George fragen (ger@)
60e385aa992e11a6cb0504e8d4fc35186e8d848bpquerna************************************************
60e385aa992e11a6cb0504e8d4fc35186e8d848bpquernaJorina (Till)
60e385aa992e11a6cb0504e8d4fc35186e8d848bpquerna************************************************
d66ac514cc15e99228d72c56c6c3daf25da8d360niq use save button for saving proof info
e23b77006a8b079c0ad52e42ba2029e759455b8fjortonimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
e23b77006a8b079c0ad52e42ba2029e759455b8fjortondevelopment graph calculus
e23b77006a8b079c0ad52e42ba2029e759455b8fjorton- Stack overflow for "show just subtree"
b597281295360dba8ac57b7606c5f5c1ef2b69b0trawick- view-test7.casl should be provable with globDecomp + locDecopm
b597281295360dba8ac57b7606c5f5c1ef2b69b0trawick- fail when doing first globDecomp, then local decomp in RelationsAndOrders
b597281295360dba8ac57b7606c5f5c1ef2b69b0trawick- correct MAYA: glob decomp: some links are not found (Jorina)
82d2a5debc5a6ed2118ac5916d9ba36ad0b5d78btrawick- Fail: No match in record selector Static.DevGraph.dgn_sign
82d2a5debc5a6ed2118ac5916d9ba36ad0b5d78btrawick for local subsume in RelationsAndOrders
22c347c08cd77d5e2c32536b467b389fd33d631fpquerna************************************************
8c46f9f81ae6357dc97560d6d85154f19cf251aejimMingyi (Till)
b6e2b36d6972a0e243368eb567e91d511fb40b1bbnicholes************************************************
b6e2b36d6972a0e243368eb567e91d511fb40b1bbnicholesport CCC to Haskell
b6e2b36d6972a0e243368eb567e91d511fb40b1bbnicholesFunktionen imageOfMorphism und inhabited
ad4a5834dfdf9488af4ac3238ea4d8b18dce49acpquerna von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
e5882a36d7756850cc829f5f2286120b877458b1pquerna mit "cvs add SigFuns.hs" einchecken
8b7594c66e764f5cd3506b6f2459497ab65a8b03pquerna"free datatypes and recursive equations are consistent"
8c46f9f81ae6357dc97560d6d85154f19cf251aejimcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
20f1b1a67eef5ab0f3295608c89964a7dca4fdd1pquernaJust True => Yes, is consistent
20f1b1a67eef5ab0f3295608c89964a7dca4fdd1pquernaJust False => No, is inconsistent
20f1b1a67eef5ab0f3295608c89964a7dca4fdd1pquernaNothing => don't know
599c5abcc7fec60611956f56b732eca033c287d2pquernacall the symbols in the image of the signature morphism "new"
599c5abcc7fec60611956f56b732eca033c287d2pquerna- each new sort must be a free type,
e76fdcdfb8994ad70776526f50fa013b3e9a6033bnicholes i.e. it must occur in a sort generation constraint that is marked as free
e76fdcdfb8994ad70776526f50fa013b3e9a6033bnicholes (Sort_gen_ax constrs True)
e76fdcdfb8994ad70776526f50fa013b3e9a6033bnicholes such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
eb9b491d7b262dad572ec2f1f75eea592283f81apquerna if not, output "don't know"
eb9b491d7b262dad572ec2f1f75eea592283f81apquerna and there must be one term of that sort (inhabited)
eb9b491d7b262dad572ec2f1f75eea592283f81apquerna if not, output "no"
c5cb4c9e7c8696907ddebab2a0037717c710b0f6jorton- group the axioms according to their leading operation/predicate symbol,
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive i.e. the f resp. the p in
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive Implication Application Strong_equation
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive Implication Predication Equivalence
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive if there are axioms not being of this form, output "don't know"
6d00a5e2c08ddbff9614ecc17a1c085462811f89slivecheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
6d00a5e2c08ddbff9614ecc17a1c085462811f89slivecheck' [] = ([([],[])],emptyUniqSet)
6d00a5e2c08ddbff9614ecc17a1c085462811f89slive-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
4f6e78091b3f45a5782389ae25b62516a7a0c842bnicholescheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
4f6e78091b3f45a5782389ae25b62516a7a0c842bnicholes | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
4f6e78091b3f45a5782389ae25b62516a7a0c842bnicholes-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
4f6e78091b3f45a5782389ae25b62516a7a0c842bnicholescheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
7d15331eeb5429d7148d13d6fd914a641bf1c000pquerna | all_vars ps = (pats, addOneToUniqSet indexs n)
7d15331eeb5429d7148d13d6fd914a641bf1c000pquerna (pats,indexs) = check' rs
e9be3aacfd6c0a1208e6c91a133be92ed0f94fe1bnicholes-- falls ein Konstruktor dabei ist: split_by_constructor
e9be3aacfd6c0a1208e6c91a133be92ed0f94fe1bnicholes-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
e9be3aacfd6c0a1208e6c91a133be92ed0f94fe1bnicholescheck' qs@((EqnInfo n ctx ps result):_)
1d14622beee568462689b2bbc6a9e0e9b6a40583striker | all_vars ps = ([], unitUniqSet n)
1d14622beee568462689b2bbc6a9e0e9b6a40583striker | constructors = split_by_constructor qs
6e5f5644328bf50c3aa295d0ab20903369010829gregames | only_vars = first_column_only_vars qs
6e5f5644328bf50c3aa295d0ab20903369010829gregames | otherwise = panic "Check.check': Not implemented :-("
e978097e0bf2ae161b6f9dde40eaf089bf046c89ake -- Note: RecPats will have been simplified to ConPats
e978097e0bf2ae161b6f9dde40eaf089bf046c89ake -- at this stage.
e978097e0bf2ae161b6f9dde40eaf089bf046c89ake constructors = or (map is_con qs)
275419d6395e6f072962fb701b89accaff1f3690jerenkrantz only_vars = and (map is_var qs)
e777da9fa7ff3138fead7860b53ef00e67a40e26jerenkrantzsubsort definitions: are conservative if formula is satisfiable
e777da9fa7ff3138fead7860b53ef00e67a40e26jerenkrantz (generate proof obligation)
e777da9fa7ff3138fead7860b53ef00e67a40e26jerenkrantz************************************************
8bdea88407c848c1c2693655e2f8b23abde12307bnicholes************************************************
275419d6395e6f072962fb701b89accaff1f3690jerenkrantzLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
8e7fb6968047a527d1ccde25ad2aed20da5150ddjerenkrantz highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
5a9fa4d75086e942f6e850e1a2e96c4c27a845d0jerenkrantz some operation symbols
5a9fa4d75086e942f6e850e1a2e96c4c27a845d0jerenkrantz show hets output immediately
5a9fa4d75086e942f6e850e1a2e96c4c27a845d0jerenkrantz C-c C-g for hets -g
5a9fa4d75086e942f6e850e1a2e96c4c27a845d0jerenkrantz when hets terminates abnormally (e.g. with a fail), emacs loops
5a9fa4d75086e942f6e850e1a2e96c4c27a845d0jerenkrantz C-n jumps to the next error, but the message windows is not always scrolled
5a9fa4d75086e942f6e850e1a2e96c4c27a845d0jerenkrantz in such a way that the error is at the top (for long error lists)
36c8049de63c446926139936c3d195330a0539cetrawick Version for XEamcs?
36c8049de63c446926139936c3d195330a0539cetrawickOWL-DL logic
36c8049de63c446926139936c3d195330a0539cetrawickOWL-DL -> CASL
0206c121a68a63559b2e843288e81bcf16093e46jerenkrantz-------------------------------------------------------------------
8ff094bdec6a2e1c355c1e6e95e9952d4fae7766jerenkrantzLaTeX pretty printer
628cf3411e8a6d09e27b3666312e43832dda93f3jortoneine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
628cf3411e8a6d09e27b3666312e43832dda93f3jortonund andere Formate besser zu unterst�tzen und einheitlichen PP code
628cf3411e8a6d09e27b3666312e43832dda93f3jortonf�r die CASL Datentypen zu bekommen.
f0d89a5a23222e031db8113478645f28688fa748jortonHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
f0d89a5a23222e031db8113478645f28688fa748jorton************************************************
f0d89a5a23222e031db8113478645f28688fa748jorton************************************************
f0d89a5a23222e031db8113478645f28688fa748jortongenerate infrastructure for circular coinduction
f0d89a5a23222e031db8113478645f28688fa748jortonCCS example: commutativity of || by coinduction
65d743d7fbb53143636ee2dec8fe8d8a1a581a6bjerenkrantz************************************************
afc08f35f5f387896bc625cdee21b88c7fe7699djerenkrantz************************************************
a0fd132e01ab69f1c48e3d6a6791447cb6d65e51jerenkrantzsimplification of HasCASL sentences (omit types)
a6bb6f2fb734e488a9b6335fabea3431f9dcf253jerenkrantzanalyse the ghc-6.4 difference in Logic/Comorphism.hs
3ca80e703a960eca0760c23636b7fe502a8f0342bnicholes"free type Pair[S,T] ::= pair(first :S; second: T)" cannot be
3ca80e703a960eca0760c23636b7fe502a8f0342bnicholestranslated from CASL to Haskell, because generated selector variables
3ca80e703a960eca0760c23636b7fe502a8f0342bnicholesbecome identical positions and are not distinguished by programmatica
3ca80e703a960eca0760c23636b7fe502a8f0342bnicholes(letting Eq,Ord derive in base/defs/UniqueNames.hs does not work!)
5300d4a4fabe3b594da950e4b9ab0f90e076546ejerenkrantzcheck for superfluous quantifications in HasCASL's function types
5300d4a4fabe3b594da950e4b9ab0f90e076546ejerenkrantz(sonja's bug)
b1306729566b49fb30aed5c46adaf07a637115afjerenkrantzLogic COL is a ruin (with wrongly qualified module names)
b1306729566b49fb30aed5c46adaf07a637115afjerenkrantznon-free/generated datatype declarations generate ga-axioms
418ee053321d0ee451bb482a9becdfcd3344201fjim(this is indented)
418ee053321d0ee451bb482a9becdfcd3344201fjimpretty printing mangles trailing and preceding annotations
5c6cb72bfeee541644cea8177aefce1157571d3bjerenkrantzallow more annotations in structured specs
5c6cb72bfeee541644cea8177aefce1157571d3bjerenkrantzthe type FIT_ARG should be changed to
db8551deeb08fa799e7f27e8b748a9397f747bdcjortondata FIT_ARG = Fit_spec (Annoted SPEC) [G_mapping] [Pos]
db8551deeb08fa799e7f27e8b748a9397f747bdcjorton -- pos: opt "fit"
db8551deeb08fa799e7f27e8b748a9397f747bdcjorton | Fit_view VIEW_NAME [Annoted FIT_ARG] [Pos]
9e3209bc06ddf32f23e4b254faa45914bc323cc9jim -- annotations before view are stored elsewhere
9e3209bc06ddf32f23e4b254faa45914bc323cc9jimhomogenizeGM should be moved to Static.AnalysisStructured
45ed846f4ed90f05c084f6a33d688e642be4e623jerenkrantzlogic coding form the comand line with printing of results
54d22ed1c429b903b029bbd62621f11a9e286137minfrinHaskell modules: hiding, renaming
54d22ed1c429b903b029bbd62621f11a9e286137minfrin- group the axioms according to their leading operation/predicate symbol,
54d22ed1c429b903b029bbd62621f11a9e286137minfrin i.e. the f resp. the p in
54d22ed1c429b903b029bbd62621f11a9e286137minfrin forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
54d22ed1c429b903b029bbd62621f11a9e286137minfrin forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
54d22ed1c429b903b029bbd62621f11a9e286137minfrin if there are axioms not being of this form, output error
92e8e44864d94866eefcbfde0a53fa3d12855149jerenkrantzMissing points for heterogeneous WADT 04 example:
06106b6b63b112a09de1b66fa29596035c0176ffthommay- improve display of HasCASL sigs + mors
06106b6b63b112a09de1b66fa29596035c0176ffthommayStatic analysis for HasCASL
e335319a08e12eb7daff9afa80e985dc53f652b8jorton pattern analysis for program equations
e335319a08e12eb7daff9afa80e985dc53f652b8jorton implemented only atomic subtyping
e335319a08e12eb7daff9afa80e985dc53f652b8jortonWeak amalgamation analysis?
c8794ec1e4c474ae101ce3835080f638136e7860erikabeleInstantiate Transformation Application system for HasCASL?
c8794ec1e4c474ae101ce3835080f638136e7860erikabeleAutomatic generation of Haskell (for a HasCASL subset)
c8794ec1e4c474ae101ce3835080f638136e7860erikabeleProofs in HasCASL
bb07ee33bce1a448bcc60ca43720b1ab1c413f87minfrin************************************************
22dda44322067379eeba28d7ec7fc833cb04c0dfminfrin************************************************
7b6ba9c468f26bdb3492d5e8cb79628a3b04e8c8wroweCASL -> SPASS
7b6ba9c468f26bdb3492d5e8cb79628a3b04e8c8wroweCoding of subsorts as unary predicates (for ontologies)
7b6ba9c468f26bdb3492d5e8cb79628a3b04e8c8wroweTranslation between Achim's ontology data structure and CASL (in Hets)
77edcaaccc089335938f3844b752e1044f7eb278trawickvisualization of "taxonomy" of CASL signatures
77edcaaccc089335938f3844b752e1044f7eb278trawick (subsorts = inheritance, unary preds = concepts, binary preds = relations)
77edcaaccc089335938f3844b752e1044f7eb278trawickRecognize guarded fragment of CASL:
59b1b6c3fd51c83c3bb9f02a8f08751335f9fb1dminfrin G ::= forall x . At(x) => G where At is a conjunction of atoms
59b1b6c3fd51c83c3bb9f02a8f08751335f9fb1dminfrin | exists x . At(x) /\ G
59b1b6c3fd51c83c3bb9f02a8f08751335f9fb1dminfrinJoost Visser wg. ATerms in Haskell => neues Repository
9f1a88897168c3f1e5009acb585daf01e38a0299jim************************************************
9f1a88897168c3f1e5009acb585daf01e38a0299jimMarkus, Lutz
9f1a88897168c3f1e5009acb585daf01e38a0299jim************************************************
616a448c1fca1648622707df5a1aae7316bb3d5djimBeweise in Isabelle
616a448c1fca1648622707df5a1aae7316bb3d5djimCASL consistency checker
616a448c1fca1648622707df5a1aae7316bb3d5djimWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
616a448c1fca1648622707df5a1aae7316bb3d5djim (Vorbild: Larch-Handbuch)
36bfefb6940a90242290e5b5713a2d831275eef1jimSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
5a8bb5948d2a258145174320587706de3219d8a3pquernaParser and static analysis for CSP-CASL
5a8bb5948d2a258145174320587706de3219d8a3pquerna************************************************
0cba3a63e59bfa77f67955cb4e034264ed6c5523jerenkrantz************************************************
e5abee85fe751fc27c5d4fc9a8ebe3b80f3d6603trawickCASL consistency checker
e5abee85fe751fc27c5d4fc9a8ebe3b80f3d6603trawickIsaWin: support CASL-libraries
ca3a25d12c5fe0926aa97550be39f0d88d0decb1pquerna************************************************
ca3a25d12c5fe0926aa97550be39f0d88d0decb1pquerna************************************************
74def8815c725f8128a4e76ab1f5704df80b024ajerenkrantzBinInt.casl: revealing in Int1 does not work correctly
74def8815c725f8128a4e76ab1f5704df80b024ajerenkrantzfrom Stefan W�lfl:
8f868f15482c7406db01216b6e4778ddabb26898trawickcomputeTheory does not work across library imports
8f868f15482c7406db01216b6e4778ddabb26898trawicklocal theorems
8f868f15482c7406db01216b6e4778ddabb26898trawickall nodes named
8f868f15482c7406db01216b6e4778ddabb26898trawickhierarchical Isabelle theories
f902601ea431a9b56106e0f5f641dd5fd7efbc30jortondaVinci printing is not adequate
f902601ea431a9b56106e0f5f641dd5fd7efbc30jortonhiding of internal nodes does not work
1e1e4f4f810b99732f06fc05141f42ca1965a9edpquernaFOL without quantifiers and with uniform disjunctions
1e1e4f4f810b99732f06fc05141f42ca1965a9edpquerna (i.e. x R1 y \/ x R2 y)
1e1e4f4f810b99732f06fc05141f42ca1965a9edpquerna (with and without =)
5f80956ca9d98d5482f38eef0c465df0923d7781jerenkrantzalgorithmic path consistency over a relation algebra
5f80956ca9d98d5482f38eef0c465df0923d7781jerenkrantz plug in reasoner for this
78fcc425fc9fc58202a1693fe40dd0ce75c031ffjorton develop correctness results (algorithmic path consistency=path consistency)
78fcc425fc9fc58202a1693fe40dd0ce75c031ffjorton within CASL
78fcc425fc9fc58202a1693fe40dd0ce75c031ffjortonCASL sublogics:
d2ffb32434f79782ff7a364ffa31064698c5c645jorton---------------
d2ffb32434f79782ff7a364ffa31064698c5c645jortonFOL without quantifiers (with and without =)
d2ffb32434f79782ff7a364ffa31064698c5c645jortonguarded fragment
01847067cfc639c14e1aa77d3b3e98f239447a12jerenkrantz[from DOLCE cooperation:
9fe74ffcdea85800f04a7222f716f78ae60cce51jerenkrantzontology mediation via pushouts/pullbacks/pulations
9fe74ffcdea85800f04a7222f716f78ae60cce51jerenkrantzRobinson consistency with shared theory constructed via pre-image?
9fe74ffcdea85800f04a7222f716f78ae60cce51jerenkrantzshow theorem links between same instances of different parameterized
dae3cb64cc6681b5f6b0fd12e7f8f6296ffaa19abnicholes specs (where one is an extension of the other one)
dae3cb64cc6681b5f6b0fd12e7f8f6296ffaa19abnicholeslink menu for %implies, $def, %cons, even without open proof obligation
d2ffb32434f79782ff7a364ffa31064698c5c645jortonfor a proved theorem, show minimal part of DG needed for proof
9fe74ffcdea85800f04a7222f716f78ae60cce51jerenkrantzcons, def, mono for nodes
81540a0eb1da2c687e22de3367d8ded55e17e330pquernaIsabelle interface: each qed should write proof info into file
d2ffb32434f79782ff7a364ffa31064698c5c645jortonglobally display nodes containing symbols mapped "twice" (i.e. via
81540a0eb1da2c687e22de3367d8ded55e17e330pquerna different signature morphisms)
ce66c67eba79a20118d8664b65b0c9eeec1bebdabnicholes and add a menu for each node allowing for tracking the different
ce66c67eba79a20118d8664b65b0c9eeec1bebdabnicholestopsort coding: partial functions as relations?
ce66c67eba79a20118d8664b65b0c9eeec1bebdabnicholestheorem link menu for proof obligations
6cfc2ed5a8e633c5a40fec65775868d53952d992trawickList.casl: quantifiers in theory generated by "show theory" missing
6cfc2ed5a8e633c5a40fec65775868d53952d992trawickUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
6cfc2ed5a8e633c5a40fec65775868d53952d992trawickin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
e34223f72e630187c4d8ac7c22da5096c833eb20trawickBuffer.het, sublogic of node Buffer:
e34223f72e630187c4d8ac7c22da5096c833eb20trawickFail: illegal node type in sublogic computation
5159c40648868a58745aa11981f706948ff0f0d1pquernaJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
c178b761acd6bffa199c2fd28c4469492b989699ndspec VarTestIncorrect =
9c6bbd67082b5a47fb17cfa5b61b8a7e1fb01875pquerna vars x:s; y:t
9c6bbd67082b5a47fb17cfa5b61b8a7e1fb01875pquerna forall x:t; y:s
572f5b8a84bb399e51b02a562776f4aec119aa95pquernaspec VarTestCorrect =
572f5b8a84bb399e51b02a562776f4aec119aa95pquerna %% vars x:s; y:t
1b03ca18c41f51a25dcf1a623a8f558bd779e0a4jerenkrantz forall x:t; y:s
1b03ca18c41f51a25dcf1a623a8f558bd779e0a4jerenkrantzIncorrect geht durch, weil die Typanalyse nicht funktioniert und Correct
1b03ca18c41f51a25dcf1a623a8f558bd779e0a4jerenkrantzwird abgelehnt, weil x und y nicht denselben Typ haben, was das richtige
1b03ca18c41f51a25dcf1a623a8f558bd779e0a4jerenkrantzVerhalten auch im ersten Fall w\x{00E4}re.
db443e0132f14dac789ab97ec23ce124360d74c2ndfor CSP-CASL example: with logic
db443e0132f14dac789ab97ec23ce124360d74c2ndheterogeneous static ana
4ac7a7c09ac5732b09f8bf28873f7e9efcab34d5bnicholestheorem links between nodes in different libraries
4ac7a7c09ac5732b09f8bf28873f7e9efcab34d5bnicholesbasicProofs: use info about used axioms
4ac7a7c09ac5732b09f8bf28873f7e9efcab34d5bnicholes ensure that axiom/thm names are unique
4ac7a7c09ac5732b09f8bf28873f7e9efcab34d5bnicholesOverload / inlineAxioms: injections
ce8490f3812311582d1deee96b012c377311b317minfrinremove "prove" menu in abstracted dg
ce8490f3812311582d1deee96b012c377311b317minfrinbetter sublogic analysis in codings
38f6ebaca968b7b23c25c0b30d0be1c7aad7412bjortonthy files in subdir
38f6ebaca968b7b23c25c0b30d0be1c7aad7412bjortonadjust path for thy files, such that hets can also be started from subdirs
cc7d8b55b16eee88be925a090473ca94b0a6e770jortonRestrict Sonjas simplifications to HasCASL
cc7d8b55b16eee88be925a090473ca94b0a6e770jortonadd suitable axioms to simplifier and CR
f2b43354f9ac8496ab7003ae01211af739efba1atrawickcomputeTheory: remove double axioms
f2b43354f9ac8496ab7003ae01211af739efba1atrawickadd suitable axioms to simplifier and classical reasoner
2555a6b5da21d61804f47084d8fcc98eb4acbc42wrowebetter display of internal nodes (use tooltip?)
2555a6b5da21d61804f47084d8fcc98eb4acbc42wroweupdate Hets, CASL, daVinci on web page
2555a6b5da21d61804f47084d8fcc98eb4acbc42wroweCASL2PCFOL: x_i -> t_i, t=[inj(x_i)]
2555a6b5da21d61804f47084d8fcc98eb4acbc42wrowepacking of binaries: add hets-update, refer to TclTk
eb6e3a3e784021abc1e28247158db3a8b07186b9minfrinCCC interface
eb6e3a3e784021abc1e28247158db3a8b07186b9minfrintest for sublogic before applying comorphism
f5098e2eb6ed9dfd7052f25761bb5e97779b8460minfrinMissing points for heterogeneous WADT 04 example:
f5098e2eb6ed9dfd7052f25761bb5e97779b8460minfrin- coding to Isabelle: translate sort gen constraints
d86551ca954d666d5b15ad38e9daf45680516c25jerenkrantz- Improve adapation to Isabelle's lexis
c79b5caf7c5462ef707363c69cc63ea2606310abtrawickIsabelle: (ask Christoph)
c79b5caf7c5462ef707363c69cc63ea2606310abtrawick remove datatypes from sort list
1551c2366551d7a361bedbf7ae54f1abd74ef822minfrin prove local thm link (=> green)
1551c2366551d7a361bedbf7ae54f1abd74ef822minfrin "prove" menu with choice windows
f1826b4cf1fbeb049c569761cc95b04e3496efd6bnicholes incorporate sublogics
f1826b4cf1fbeb049c569761cc95b04e3496efd6bnicholes sublogic translation table
f1826b4cf1fbeb049c569761cc95b04e3496efd6bnicholes better interaction between Isabelle instance (for one node)
103a93c625bcde1a6a7a5155b64dcda36f612180pquerna + selection of single goals that are proved
103a93c625bcde1a6a7a5155b64dcda36f612180pquerna => use PGIP interface (Christoph, David)
103a93c625bcde1a6a7a5155b64dcda36f612180pquerna correct show theory
87a528a7622973988232079ba02763748c9c7071pquerna Keep proofs and lemmas in .thy files (kind of merge)
87a528a7622973988232079ba02763748c9c7071pquerna CASL-like syntax
87a528a7622973988232079ba02763748c9c7071pquerna CASL annotation for lemmas that should be used in proof
1a986bbad9314beb8739401cac822e87bb04bbfepquerna inherit CASL's mixfix syntax
1a986bbad9314beb8739401cac822e87bb04bbfepquernaSignatures versus theories: where to store additional infos?
1a986bbad9314beb8739401cac822e87bb04bbfepquernacomp(id,x)=x for comorphism names
752ec04fdfa6e936047811b9e506cf829d7a69f7pquernaGeneralise CASL2Modal
752ec04fdfa6e936047811b9e506cf829d7a69f7pquernaMixfix analysis + typecheck for modality axiomatizations
752ec04fdfa6e936047811b9e506cf829d7a69f7pquernaModal logics: modal logic, temporal logic, mu calculus
cf82d17373559b6163dbd6c844c1af82cab56883niq+ translations (e.g. modal to FOL)
cf82d17373559b6163dbd6c844c1af82cab56883niqCASL->Haskell with free DTs (mark sortgens) + recursion
c4e6f5320f87eff25838c21c107a24b688d539d0niq- List[Dec] wird List[Pos]
c4e6f5320f87eff25838c21c107a24b688d539d0niq- George wg. Schlie�en von Fenstern
c4e6f5320f87eff25838c21c107a24b688d539d0niq- node numbers do not match
c4e6f5320f87eff25838c21c107a24b688d539d0niq- thm links with external target should be provable as well
174a8f105b1c11aa50a05993ea8ba2d117d3df6endRemove warnings
174a8f105b1c11aa50a05993ea8ba2d117d3df6endDifferent types of logic translations
174a8f105b1c11aa50a05993ea8ba2d117d3df6endImprove Static analysis of structured specs
174a8f105b1c11aa50a05993ea8ba2d117d3df6endDevelopment graph calculus, Strategies for DG rules
3ad0f071604de33c0b3733b649cd0445ba00f54dakeManagement of change
3ad0f071604de33c0b3733b649cd0445ba00f54dakeIntegrate provers
c2549f0b237ac86f3623a601a766969d805dbc2and Otter model checker
c2549f0b237ac86f3623a601a766969d805dbc2and FOL-prover by Uli Furhbach
c2549f0b237ac86f3623a601a766969d805dbc2and modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
7efe7de73c89c26518714a504359244d03cfbbc5jorton Isabelle codings: www.inf.ethz.ch/~vigano
7efe7de73c89c26518714a504359244d03cfbbc5jorton Renate Schmidt, Manchester: uses FOL prover for description logic
f84d3d83a741c21154d42e0ebdec9b9b37efeedcjorton (as efficient as DL-specific tools!)
f84d3d83a741c21154d42e0ebdec9b9b37efeedcjorton Look at PROSPER toolkit
7efe7de73c89c26518714a504359244d03cfbbc5jorton consistency: see IJCAR-workshop on non-provability in Cork
d60027cde3289d3ef35bc9d815882975eb60e6abjorton IJCAR workshop about logical frameworks and meta-languages
d60027cde3289d3ef35bc9d815882975eb60e6abjortonIntegrate CCC
504498fd20729dcc29dfbfb78e64a8521c6a767ajerenkrantzKlaus' wayfinding example
d406be0d6a4f9e61bbdfa6c8cde2e09338dd650atrawickask Detlef: critical pairs, Fossacs paper by Francesco
269e0a31aa0f6aafe7292e932a182ccb535e55a9trawickUniForM workbench:
c1ba3b0ac00c4fee2f4b950dfdb167b39611b661ndfirst steps towards CASL instance, using ATerms and re-using MMISS instance
c1ba3b0ac00c4fee2f4b950dfdb167b39611b661ndvariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
b95a84193578c904426cef6dda84f7118a400a16jimIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
b95a84193578c904426cef6dda84f7118a400a16jim Grothendieck logic)
b95a84193578c904426cef6dda84f7118a400a16jim + for TAS: reflection of HOL in HOL, to be composed with encodings
b95a84193578c904426cef6dda84f7118a400a16jim (i.e. signatures, axioms, signature morphisms in HOL,
03a3ed87983471816561562f957390ed935d7b3bnd re-use ML signatures) (Einar)
03a3ed87983471816561562f957390ed935d7b3bndDisplay Specs as daVinci subgraphs
c533ecac2227dc228070e686fb14dc6860f497f8ndUser interface
56cefde0af6b8db6fda0f1d95d8cdca54f397cd0nd--------------
56cefde0af6b8db6fda0f1d95d8cdca54f397cd0ndLogic graph window
56cefde0af6b8db6fda0f1d95d8cdca54f397cd0ndInput text window
41369ed0bc7f2db6272278c27025f6aabf97fe63ndDevelopment graph window
41369ed0bc7f2db6272278c27025f6aabf97fe63ndProver windows
496f8f3966319d43455675630a849bae019d2a32nd************************************************
9e8c2603790f490398a0fabf97866b6815748a54ianhFOR STUDENTS
9e8c2603790f490398a0fabf97866b6815748a54ianh************************************************
9e8c2603790f490398a0fabf97866b6815748a54ianhHets 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)
a21b3b9d8ebb12fd51fa1d17e44d5644a35a9a5fndPackaging of installation
a21b3b9d8ebb12fd51fa1d17e44d5644a35a9a5fndGUI (vgl. VSE)
1fbcf7a8e7b18be1b0e77b7bc38b7b71f8dfb052nd with Eclipse, WXHaskell or GTk?
1fbcf7a8e7b18be1b0e77b7bc38b7b71f8dfb052nd how to integrate with event system of UniForM workbench?
1fbcf7a8e7b18be1b0e77b7bc38b7b71f8dfb052ndintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
f769c33501f474aed3e0f7c769477c8c4f478783geoff this interacts with GUI!
f769c33501f474aed3e0f7c769477c8c4f478783geoffData.Serizable (only when ghc supports it) better: rely on pointer equality
f769c33501f474aed3e0f7c769477c8c4f478783geoffXML interface
d7c7669331357296719d67d1963d40d713ed455atrawickincrease performance
d7c7669331357296719d67d1963d40d713ed455atrawickintegrate QuickCheck: come to lecture!
92d95be777d4365eb79444a7a558355a7a92081ajorton++++++++++++++++++++++++++++++++++++++++++++++++
92d95be777d4365eb79444a7a558355a7a92081ajortonRemaining things
92d95be777d4365eb79444a7a558355a7a92081ajorton++++++++++++++++++++++++++++++++++++++++++++++++
af8dee354a287249dd9f3f77bbe850108e5afe43trawickMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
af8dee354a287249dd9f3f77bbe850108e5afe43trawick Coq, PTT in Maude
af8dee354a287249dd9f3f77bbe850108e5afe43trawickProofs with basic datatypes
f78505c7d260473bf11002f5028186f27d0ed8a0geoffVerbesserung der Fehlermeldungen
f78505c7d260473bf11002f5028186f27d0ed8a0geoffImprove encoding: CATS/basic_encode.sml (3 days)
f78505c7d260473bf11002f5028186f27d0ed8a0geoffMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
f78505c7d260473bf11002f5028186f27d0ed8a0geoffRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
f78505c7d260473bf11002f5028186f27d0ed8a0geoffExample of Agnes und Frank: proofs in HOL-CASL (2 days)
ea981941b1e5ecfb1a27b9e9aff32b9c98640ed9ndTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
ea981941b1e5ecfb1a27b9e9aff32b9c98640ed9ndExamples for cond rewriting -> Christophe
ea981941b1e5ecfb1a27b9e9aff32b9c98640ed9ndDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
ea981941b1e5ecfb1a27b9e9aff32b9c98640ed9ndAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
d57b793ddd42a997c2cb3bd389bbcf1161226fd8trawickEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
d57b793ddd42a997c2cb3bd389bbcf1161226fd8trawickHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
d57b793ddd42a997c2cb3bd389bbcf1161226fd8trawickHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
d11bf78168abbb07d8ed9f54d7ea0953d46aad83ndHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
d11bf78168abbb07d8ed9f54d7ea0953d46aad83ndEncoding of structured free (3 days)
d11bf78168abbb07d8ed9f54d7ea0953d46aad83ndEncoding of structured cofree (2 weeks)
d11bf78168abbb07d8ed9f54d7ea0953d46aad83ndEingabesyntax als Mix zwischen CASL und HOL (3 days)
bf28a00d8218aa76a56eddabca308e8d0e691626ndAdapt Isabelle unions to CASL unions (1 week)
bf28a00d8218aa76a56eddabca308e8d0e691626ndGenerate Proof obligations (1 week)
bf28a00d8218aa76a56eddabca308e8d0e691626ndAdd renaming to Isabelle kernel (2 months)
70f665a8945f3bdfe8bbeaa063de2aa722fc9b29ndRepository mit korrekten und fehlerhaften Specs
c08f5a0cf2b8903255186ba998a4481dfac9c796ndHetCATS User manual, Doku fuer Environments (2 weeks)
c08f5a0cf2b8903255186ba998a4481dfac9c796ndConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
c08f5a0cf2b8903255186ba998a4481dfac9c796ndComparsion of parsers (ML-yacc parser, SDF-Parser)
5bcdf2cd27ab0c91a3c7eaffbff4cb8505389dc1ndConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
5bcdf2cd27ab0c91a3c7eaffbff4cb8505389dc1ndPVS anbinden (Kooperation mit Cachan?)
02b0660d7f44ff8106bd5095653e9c19e39ec37dndPortations: Intel-Solaris, Mac OS-10 (2 weeks)
02b0660d7f44ff8106bd5095653e9c19e39ec37dnd(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
5b8e35ad88268c0210d93288dad57c2f1d3e8811ndViews on CASL specs: CATS/viewer.sml (2 weeks)
5b8e35ad88268c0210d93288dad57c2f1d3e8811ndUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
a9ee8e9bd3dffd23ca49be8d0bdf0e33cd0bcce2jortonModule graph CATS/module_graph.sml (1 week) -> Maya?
a9ee8e9bd3dffd23ca49be8d0bdf0e33cd0bcce2jortonATerms via XML: CATS/aterms.sml (2 weeks)
3b86be5b30d5cbacc1f942b05dff8a9365449d30jortonNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
3b86be5b30d5cbacc1f942b05dff8a9365449d30jortonLibrary management: CATS/lib_ana.sml (2 weeks)
9026fcf39ea5fbacee72b6c4f68e6c778dbad478ndVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
71f3601de4983bc2a6aaffcf37dc1d35c8674a34coar{- This does not work due to needed ordering:
71f3601de4983bc2a6aaffcf37dc1d35c8674a34coarinstance Functor Set where
71f3601de4983bc2a6aaffcf37dc1d35c8674a34coar fmap = mapSet
49a82db11388cff9b29ff861b4241bbce69c76fdtrawickinstance Monad Set where
49a82db11388cff9b29ff861b4241bbce69c76fdtrawick return = unitSet
49a82db11388cff9b29ff861b4241bbce69c76fdtrawick m >>= k = unionManySets (setToList (fmap k m))
8dc154408549195c828b823e9dc7396f107f2512jortonAufbau von comptable
8dc154408549195c828b823e9dc7396f107f2512jorton--------------------
8dc154408549195c828b823e9dc7396f107f2512jorton[("normal","normal","normal"),
ca2504b59d48a926af23f6b18af550c1e892d8a6jorton ("normal","inclusion","normal"),
ca2504b59d48a926af23f6b18af550c1e892d8a6jorton ("inclusion","normal","normal"),
ca2504b59d48a926af23f6b18af550c1e892d8a6jorton ("inclusion","inclusion","inclusion")]
6126fad8adeca94e9813812c691747afeca164dftrawickAufbau von ginfo
6126fad8adeca94e9813812c691747afeca164dftrawick--------------------
7ed5992392d5babab20be4ce4029ad17ae062b5aianhMit initgraphs erzeugen
7ed5992392d5babab20be4ce4029ad17ae062b5aianhAufbau des Graphen selbst
b7973a1e572a3ff7cdedb48ed1f9481ece700bf9trawick------------------------