todo revision 96cc01853b72b9d0fdc9e3d309a196a2216de119
71092d70af35567dd154d3de2ce04ce62e157a7cLennart PoetteringPlan and priority list for CoFI tool activities
d086fe4e085d216652b70e575e59302810035989Kay Sievers************************************************
d086fe4e085d216652b70e575e59302810035989Kay Sievers************************************************
d086fe4e085d216652b70e575e59302810035989Kay SieversList.casl should go through
9cb48731b29f508178731b45b0643c816800c05eKay Sieversremove typedecls and op decls generated for datatypes
9cb48731b29f508178731b45b0643c816800c05eKay Sieversset up default simplifier
9cb48731b29f508178731b45b0643c816800c05eKay Sieversset up default tactics using axioms
9cb48731b29f508178731b45b0643c816800c05eKay Sievers************************************************
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay Sievers************************************************
05677bb78079c3fa0283101aac2c07581f4873f1Lennart Poetteringrename variables that conflict with operation syntax
73090dc815390f4fca4e3ed8a7e1d3806605daaaLennart Poettering (or restrict mixfix decls for consts)
f957632b960a0a42999b38ded7089fa602b41745Kay Sieversdie Mixfix-Deklarationen f�hren noch zu Problemen.
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sieversf�hrt dazu, dass c nicht mehr als Variable verwendet werden kann.
871206d340ed6119b31daeb8b13c8ef5ccf25501Kay SieversK�nntest du diese Mixfix-Deklarationen auf die notwendigen F�lle
871206d340ed6119b31daeb8b13c8ef5ccf25501Kay Sieversbeschr�nken, und ggf. die Variablen umbenennen?
825c6fe5eb362437aa46faa52b683a62eede9a13Lennart PoetteringZudem m�ssen Underscores escaped werden:
825c6fe5eb362437aa46faa52b683a62eede9a13Lennart Poettering C_1::t ("C'_1")
825c6fe5eb362437aa46faa52b683a62eede9a13Lennart PoetteringDiplom: Encoding for HasCASL in Isabelle/HOL(CF)
825c6fe5eb362437aa46faa52b683a62eede9a13Lennart PoetteringInterface Hets <-> ISabelle
825c6fe5eb362437aa46faa52b683a62eede9a13Lennart Poettering Hets muss eine Pipe als Inode erzeugen
825c6fe5eb362437aa46faa52b683a62eede9a13Lennart Poettering und dann auf Beweisterme warten
e146e4516b9ea9907852e7ad609de39dca9e8769Kay Sievers und auf "Ende" warten
e146e4516b9ea9907852e7ad609de39dca9e8769Kay Sievers und dann Proof_status sen proof_tree entsprechend ausf�llen
e146e4516b9ea9907852e7ad609de39dca9e8769Kay SieversIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering Beweisterme (siehe Kapitel im RefMan)
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart Poettering ML "proofs := 1" (am Anfang des .thy file)
7560fffcd2531786b9c1ca657667a43e90331326Lennart Poettering am Ende jedes Theorems: Beweisterm in die Pipe schreiben
7560fffcd2531786b9c1ca657667a43e90331326Lennart Poettering (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering mit pretty_proof_of und Pretty.string_of
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering und Start- und Endmarker
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering am Schluss "Ende" ausgeben
5a7e959984788cf89719dec31999409b63bb802bLennart PoetteringFunktion basicInferenceNode in Proofs/Proofs.hs:
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart PoetteringEmacs: uni/emacs, George fragen (ger@)
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering************************************************
0790b9fed42eefc4e22dbbe2337cba9713b7848cLennart Poettering************************************************
d7535514c39b2245e1651dc4b08bdec230e05f36Lennart Poettering use save button for saving proof info
5aea932fd54db835b77709ddeba30732648aae53Lennart Poetteringimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
918943c75fbd9dee87ff396de3a7c63a8d228433Lennart Poetteringdevelopment graph calculus
918943c75fbd9dee87ff396de3a7c63a8d228433Lennart Poettering- Stack overflow for "show just subtree"
fd4d89b2c0b31da01d134301e30916931ae3c7d9Lennart Poettering- view-test7.casl should be provable with globDecomp + locDecopm
fd4d89b2c0b31da01d134301e30916931ae3c7d9Lennart Poettering- fail when doing first globDecomp, then local decomp in RelationsAndOrders
8230e26dc954a40d8c9dbc8ddd9376117021f9d2Lennart Poettering- correct MAYA: glob decomp: some links are not found (Jorina)
8230e26dc954a40d8c9dbc8ddd9376117021f9d2Lennart Poettering- Fail: No match in record selector Static.DevGraph.dgn_sign
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart Poettering for local subsume in RelationsAndOrders
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart Poettering************************************************
73fcda2737ac607a265b3e1382e9d4fb4607c20fKay Sievers************************************************
919a7f39e6aa4a93b8348ec2586e313c40f49e52Lennart Poetteringtype check for CASL
4d9909c93e9c58789c71b34555a1908307c6849eLennart Poettering*** Error encode.casl:8.30, No correct typing for
47ae7201b1df43bd3da83a19e38483b0e5694c99Lennart Poettering************************************************
941e990db1f2682abaa2966b1c48602901d0c599Lennart Poettering************************************************
decab96090593d617bfd576cb68253a6e082309bLennart Poetteringport CCC to Haskell
919a7f39e6aa4a93b8348ec2586e313c40f49e52Lennart PoetteringFunktionen imageOfMorphism und inhabited
919a7f39e6aa4a93b8348ec2586e313c40f49e52Lennart Poettering von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
88a6c5894c9d3f85d63b87b040c130366b4006ceKay Sievers mit "cvs add SigFuns.hs" einchecken
6b78f9b4354010f8af2fe48c783ffd52b2db8f57Lennart Poettering"free datatypes and recursive equations are consistent"
9f8d29834ba97052403e50ec9b358c0470fa4cebLennart PoetteringcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
9f8d29834ba97052403e50ec9b358c0470fa4cebLennart PoetteringJust True => Yes, is consistent
9f8d29834ba97052403e50ec9b358c0470fa4cebLennart PoetteringJust False => No, is inconsistent
9f8d29834ba97052403e50ec9b358c0470fa4cebLennart PoetteringNothing => don't know
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poetteringcall the symbols in the image of the signature morphism "new"
b7def684941808600c344f0be7a2b9fcdda97e0fLennart Poettering- each new sort must be a free type,
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering i.e. it must occur in a sort generation constraint that is marked as free
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering (Sort_gen_ax constrs True)
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering if not, output "don't know"
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering and there must be one term of that sort (inhabited)
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering if not, output "no"
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering- group the axioms according to their leading operation/predicate symbol,
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering i.e. the f resp. the p in
49f43d5f91a99b23f745726aa351d8f159774357Ville Skyttä forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
d246fbb054974af4c78e0cf298e031291475cbc1Lennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
be0aa78406c73a6625308dc0672b5ff27ec6f9a8Lennart Poettering Implication Application Strong_equation
be0aa78406c73a6625308dc0672b5ff27ec6f9a8Lennart Poettering forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
461b1822321d6be0d7fd8be29bf3b4993ebd1b85Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
461b1822321d6be0d7fd8be29bf3b4993ebd1b85Lennart Poettering Implication Predication Equivalence
9946996cda11a18b44d82344676e5a0e96339408Lennart Poettering if there are axioms not being of this form, output "don't know"
b4efdf97203ddf781c17f77be84cc61516a077d2Lennart Poetteringcheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
b4efdf97203ddf781c17f77be84cc61516a077d2Lennart Poetteringcheck' [] = ([([],[])],emptyUniqSet)
3471bedc005fab03f40b99bf6599645330adcd9eLennart Poettering-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
3471bedc005fab03f40b99bf6599645330adcd9eLennart Poetteringcheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
5231084b479455e6cc892ec3c37c9f599c5bea58Lennart Poettering | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
eeb875144e5a80d0521461a139f13fc8014d77d8Lennart Poettering-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
eeb875144e5a80d0521461a139f13fc8014d77d8Lennart Poetteringcheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering | all_vars ps = (pats, addOneToUniqSet indexs n)
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering (pats,indexs) = check' rs
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering-- falls ein Konstruktor dabei ist: split_by_constructor
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sieverscheck' qs@((EqnInfo n ctx ps result):_)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers | all_vars ps = ([], unitUniqSet n)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers | constructors = split_by_constructor qs
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers | only_vars = first_column_only_vars qs
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers | otherwise = panic "Check.check': Not implemented :-("
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers -- Note: RecPats will have been simplified to ConPats
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers -- at this stage.
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers constructors = or (map is_con qs)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers only_vars = and (map is_var qs)
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sieverssubsort definitions: are conservative if formula is satisfiable
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers (generate proof obligation)
59cea26a349cfa8db906b520dac72563dd773ff2Lennart Poettering************************************************
9473414219330b9febc1d0712bbf49ad74cf962fLennart Poettering************************************************
24f3a374b9588a6e409ba58b40bdd684050decf3Lennart Poettering highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
24f3a374b9588a6e409ba58b40bdd684050decf3Lennart Poettering some operation symbols
24f3a374b9588a6e409ba58b40bdd684050decf3Lennart Poettering show hets output immediately
88f8ffbd63d09b0f2899a8d45fc82e22839aeb81Lennart Poettering C-c C-g for hets -g
88f8ffbd63d09b0f2899a8d45fc82e22839aeb81Lennart Poettering when hets terminates abnormally (e.g. with a fail), emacs loops
069cfc85f876bb6966cb5a9bbe0235f5064622cdLennart Poettering C-n jumps to the next error, but the message windows is not always scrolled
069cfc85f876bb6966cb5a9bbe0235f5064622cdLennart Poettering in such a way that the error is at the top (for long error lists)
7b63bde1ed0d4f30c799c9b4737fa926465929f9Lennart Poettering Version for XEamcs?
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart Poettering-------------------------------------------------------------------
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart PoetteringLaTeX pretty printer
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poetteringeine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poetteringund andere Formate besser zu unterst�tzen und einheitlichen PP code
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart Poetteringf�r die CASL Datentypen zu bekommen.
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart PoetteringHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
a26336da875a6657d404d1e44b86ae067c34b110Kay Sievers************************************************
e85647f73e235c2a6ea412cb8d841e092c373501Lennart Poettering************************************************
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringgenerate infrastructure for circular coinduction
14038c2e83001abfbcdc3f9f2402189a9b3d2f0cLennart PoetteringCCS example: commutativity of || by coinduction
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering************************************************
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering************************************************
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poetteringnon-free/generated datatype declarations generate ga-axioms
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poettering(this is indented)
d889a2069a87e4617b32ddbdeace5a53a12c699dLennart Poetteringpretty printing mangles trailing and preceding annotations
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringallow more annotations in structured specs
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringthe type FIT_ARG should be changed to
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart Poetteringdata FIT_ARG = Fit_spec (Annoted SPEC) [G_mapping] [Pos]
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart Poettering -- pos: opt "fit"
7e2668c6fd5720ae4d2d55eb8a062739687516afLennart Poettering | Fit_view VIEW_NAME [Annoted FIT_ARG] [Pos]
7e2668c6fd5720ae4d2d55eb8a062739687516afLennart Poettering -- annotations before view are stored elsewhere
e85647f73e235c2a6ea412cb8d841e092c373501Lennart PoetteringhomogenizeGM should be moved to Static.AnalysisStructured
a888b352eb53b07daa24fa859ceeb254336b293dLennart Poetteringlogic coding form the comand line with printing of results
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart PoetteringHaskell modules: hiding, renaming
3d9a412243035beeaaf3465a62065444a5adf21cLennart Poettering- group the axioms according to their leading operation/predicate symbol,
3d9a412243035beeaaf3465a62065444a5adf21cLennart Poettering i.e. the f resp. the p in
88f642c00b1708c5e0203c1753a9ef91d1de5442Kay Sievers forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
88f642c00b1708c5e0203c1753a9ef91d1de5442Kay Sievers forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay Sievers if there are axioms not being of this form, output error
a0a3844815b0f346dba03f41245c620f432e462fLennart PoetteringMissing points for heterogeneous WADT 04 example:
9efaf380a7c7fa16f44b1aa15b967e99f331203aLennart Poettering- improve display of HasCASL sigs + mors
4ee717820208a4c8e92383d0dbefa401827fab38Kay SieversStatic analysis for HasCASL
4ee717820208a4c8e92383d0dbefa401827fab38Kay Sievers pattern analysis for program equations
5ba2dc259f3cdd8fddef68cfd28380a32534e49aKay Sievers implemented only atomic subtyping
5ba2dc259f3cdd8fddef68cfd28380a32534e49aKay SieversWeak amalgamation analysis?
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay SieversInstantiate Transformation Application system for HasCASL?
762f91fa600b3b2887e3b088cd700216a85e3c81Kay SieversAutomatic generation of Haskell (for a HasCASL subset)
762f91fa600b3b2887e3b088cd700216a85e3c81Kay SieversProofs in HasCASL
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sievers************************************************
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sievers************************************************
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay SieversCASL -> SPASS
08f23fd29c9df9c8b4e874933eb39711f069754bLennart PoetteringCoding of subsorts as unary predicates (for ontologies)
08f23fd29c9df9c8b4e874933eb39711f069754bLennart PoetteringTranslation between Achim's ontology data structure and CASL (in Hets)
068665b6fd9839f27bcace7e8f56c0baa6935272Lennart Poetteringvisualization of "taxonomy" of CASL signatures
b070e7f3c9ed680c821bd89d42506695f2438506Lennart Poettering (subsorts = inheritance, unary preds = concepts, binary preds = relations)
b070e7f3c9ed680c821bd89d42506695f2438506Lennart PoetteringRecognize guarded fragment of CASL:
231931ffba1bca9d8759bbd6f797e56f8c6971faLennart Poettering G ::= forall x . At(x) => G where At is a conjunction of atoms
231931ffba1bca9d8759bbd6f797e56f8c6971faLennart Poettering | exists x . At(x) /\ G
169c4f65131fbc7bcb51e7d5487a715cdcd0e0ebLennart PoetteringJoost Visser wg. ATerms in Haskell => neues Repository
bd08f2422491169e92dc0899d5ba848fcae4c15cLennart Poettering************************************************
fb0864e7b9c6d26269ccea6ec5c0fd921c029781Lennart Poettering************************************************
18da49531e4c6b31bd2439b4d738dc1bb9660af1Lennart PoetteringBeweise in Isabelle
18da49531e4c6b31bd2439b4d738dc1bb9660af1Lennart PoetteringCASL consistency checker
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart PoetteringWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart Poettering (Vorbild: Larch-Handbuch)
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart PoetteringSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart PoetteringParser and static analysis for CSP-CASL
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart Poettering************************************************
101f077676e9fbe1a66c8b2dc4864a8d7a94c372Lennart Poettering************************************************
f7f964eb3625e4cca7f16377fa12aa7a760243e7Lennart PoetteringCASL consistency checker
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart PoetteringIsaWin: support CASL-libraries
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering************************************************
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering************************************************
15e9fbd851c15ecaad4888932584f37dcd26111aLennart Poetteringtheorem link menu for proof obligations
680a1dbc354b2f437b4e06e27d4c43217977efdfLennart PoetteringUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
680a1dbc354b2f437b4e06e27d4c43217977efdfLennart Poetteringin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
c4aa65e7147dc742886edf25593e10466b02fc3aLennart PoetteringBuffer.het, sublogic of node Buffer:
7e64c73a93cdcc7068280f3e3ba8adbd6c6f8f84Lennart PoetteringFail: illegal node type in sublogic computation
a558d00381291afd6a81f7df07269fe76eeae556Lennart PoetteringJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poetteringspec VarTestIncorrect =
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poettering forall x:t; y:s
05aa9edde0f9f4077b8120389c93cb0134eda9c5Lennart Poetteringspec VarTestCorrect =
62f21ec91ad8e7e24079962f4df066b0094fe68dLennart Poettering %% vars x:s; y:t
f7357f59c3d4de8080fa78f8aa5fa6dbf1afc8dcLennart Poettering forall x:t; y:s
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart PoetteringIncorrect geht durch, weil die Typanalyse nicht funktioniert und Correct
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poetteringwird abgelehnt, weil x und y nicht denselben Typ haben, was das richtige
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart PoetteringVerhalten auch im ersten Fall w\x{00E4}re.
b3fa47e0819b08ea32e69e19e6d88ce2daca069dLennart Poetteringfor CSP-CASL example: with logic
b3fa47e0819b08ea32e69e19e6d88ce2daca069dLennart Poetteringheterogeneous static ana
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart Poetteringtheorem links between nodes in different libraries
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart PoetteringbasicProofs: use info about used axioms
4cbd9ecf45f64c3a9acc99d473fbf3be3687ae24Lennart Poettering ensure that axiom/thm names are unique
b011116d1829bde044a638cbabfb070a7e0e8fa7Kay SieversOverload / inlineAxioms: injections
65c0cf7108ae3537a357c74b4586a783baba82f9Lennart Poetteringremove "prove" menu in abstracted dg
f957632b960a0a42999b38ded7089fa602b41745Kay Sieversbetter sublogic analysis in codings
f957632b960a0a42999b38ded7089fa602b41745Kay Sieversthy files in subdir
a2f5666d06fe8233025738047115bb9e3959df3eLennart Poetteringadjust path for thy files, such that hets can also be started from subdirs
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart PoetteringRestrict Sonjas simplifications to HasCASL
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart Poetteringadd suitable axioms to simplifier and CR
c821bd28c2ecce8d35248d61949fe1c0c3030b6cLennart PoetteringcomputeTheory: remove double axioms
c821bd28c2ecce8d35248d61949fe1c0c3030b6cLennart Poetteringadd suitable axioms to simplifier and classical reasoner
7d441ddb5ca090b5a97f58ac4b4d97b3e84fa81eLennart Poetteringbetter display of internal nodes (use tooltip?)
14e639ae7a1dbf156273ce697d30fbc6c6594209Lennart Poetteringupdate Hets, CASL, daVinci on web page
d3c7d7dd77b2b72315164b672462825cef6c0f9aKay SieversCASL2PCFOL: x_i -> t_i, t=[inj(x_i)]
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poetteringpacking of binaries: add hets-update, refer to TclTk
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poetteringtest for sublogic before applying comorphism
0a55b298d930543c8065bb9e708dd112562b1736Lennart PoetteringMissing points for heterogeneous WADT 04 example:
97f73ffb04947acf0a5854e3a7bdbb7a0105f6faLennart Poettering- coding to Isabelle: translate sort gen constraints
85f248b26653f5322c26735661d63d4e8460c30eLennart Poettering- Improve adapation to Isabelle's lexis
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart PoetteringIsabelle: (ask Christoph)
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering remove datatypes from sort list
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart Poettering prove local thm link (=> green)
a4c279f87451186b8beb1b8cc21c7cad561ecf4bLennart Poettering "prove" menu with choice windows
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart Poettering incorporate sublogics
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart Poettering sublogic translation table
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart Poettering better interaction between Isabelle instance (for one node)
7c697168102cb64c5cb65a542959684014da99c7Lennart Poettering + selection of single goals that are proved
253ee27a0c7a410d27d490bb79ea97caed6a2b68Lennart Poettering => use PGIP interface (Christoph, David)
8d0e38a2b966799af884e78a54fd6a2dffa44788Lennart Poettering correct show theory
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering Keep proofs and lemmas in .thy files (kind of merge)
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering CASL-like syntax
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering CASL annotation for lemmas that should be used in proof
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart Poettering inherit CASL's mixfix syntax
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart PoetteringSignatures versus theories: where to store additional infos?
916abb21d0a6653e0187b91591e492026886b0a4Lennart Poetteringcomp(id,x)=x for comorphism names
71092d70af35567dd154d3de2ce04ce62e157a7cLennart PoetteringGeneralise CASL2Modal
916abb21d0a6653e0187b91591e492026886b0a4Lennart PoetteringMixfix analysis + typecheck for modality axiomatizations
b23de6af893c11da4286bc416455cd0926d1532eLennart PoetteringModal logics: modal logic, temporal logic, mu calculus
b23de6af893c11da4286bc416455cd0926d1532eLennart Poettering+ translations (e.g. modal to FOL)
21bdae12e11ae20460715475d8a0c991f15464acLennart PoetteringCASL->Haskell with free DTs (mark sortgens) + recursion
c798c40ec957a35cd4b7d04a196a9e58880c6ff3Lennart Poettering- List[Dec] wird List[Pos]
c798c40ec957a35cd4b7d04a196a9e58880c6ff3Lennart Poettering- George wg. Schlie�en von Fenstern
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering- node numbers do not match
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering- thm links with external target should be provable as well
253ee27a0c7a410d27d490bb79ea97caed6a2b68Lennart PoetteringRemove warnings
5d0fcd7c8d29340ac9425c309e8ac436a9af699cLennart PoetteringDifferent types of logic translations
acb14d318b84bda00d1e666d7dab6794d5bbeb3fLennart PoetteringImprove Static analysis of structured specs
8bbabc447b1d913bd21faf97c7b17d20d315d2b4Lennart PoetteringDevelopment graph calculus, Strategies for DG rules
8bbabc447b1d913bd21faf97c7b17d20d315d2b4Lennart PoetteringManagement of change
44143309dd0b37d61d7d842ca58f01a65646ec71Kay SieversIntegrate provers
3d57c6ab801f4437f12948e29589e3d00c3ad9dbLennart Poettering Otter model checker
b9a2a36b519ccd79c4198e7dda4e657d597a14adLennart Poettering FOL-prover by Uli Furhbach
b9a2a36b519ccd79c4198e7dda4e657d597a14adLennart Poettering modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
ba1a55152c50dfbcd3d4a64353b95f4a2f37985eLennart Poettering Isabelle codings: www.inf.ethz.ch/~vigano
9408a2d295a312a5472345090e28e0502570494bLennart Poettering Renate Schmidt, Manchester: uses FOL prover for description logic
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering (as efficient as DL-specific tools!)
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay Sievers Look at PROSPER toolkit
f9276855a1d270b6c3f857cdaf2c4b49920c2228Lennart Poettering consistency: see IJCAR-workshop on non-provability in Cork
f9276855a1d270b6c3f857cdaf2c4b49920c2228Lennart Poettering IJCAR workshop about logical frameworks and meta-languages
a8f11321c209830a35edd0357e8def5d4437d854Lennart PoetteringKlaus' wayfinding example