todo revision 5f40e8aa2c372040ab519c6401627d64812922ff
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
9da19b4cbb0a0dbc7b592e7ba05bdee0f222d208Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
9da19b4cbb0a0dbc7b592e7ba05bdee0f222d208Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
6aed82191ef8360363940356ef9f6f448e4c5b87Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski**************** task A ************************
6aed82191ef8360363940356ef9f6f448e4c5b87Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski************************************************
566b6a416bde2bc90d3aece2d992127303fb5d75Till MossakowskiFlorian (Till)
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski************************************************
b34594103c3ab68b20ef7a3fe8467d7eb5913153Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski************************************************
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiHendrik (Till)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski************************************************
6aed82191ef8360363940356ef9f6f448e4c5b87Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
cc9279b89cc62b80199696ac7e87b6d2bdd08e7aTill MossakowskiAnzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
6aed82191ef8360363940356ef9f6f448e4c5b87Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
5f40e8aa2c372040ab519c6401627d64812922ffKlaus Luettichsee http://trac.informatik.uni-bremen.de:8080/hets
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
5210ca461d947c73189a20c7a9c909c06c5efc70Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 1
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski************************************************
2468ac9eb2743941b0deb95e567adb5239a24287Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 2
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
2468ac9eb2743941b0deb95e567adb5239a24287Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 3
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
2468ac9eb2743941b0deb95e567adb5239a24287Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 4
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskifurther task 5
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder************************************************
aec579d1aff83f526013366a5250b5e2564366eaTill Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiremaining stuff
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
aec579d1aff83f526013366a5250b5e2564366eaTill Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski************************************************
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskigenerate infrastructure for circular coinduction
cb1c5be39138fb8f037dbefc121fe41adc06845dTill MossakowskiCCS example: commutativity of || by coinduction
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
7805ba9a692e55ad925baf0fca762a7ee39ea006Christian MaederIsabelle coding (let, case, etc.)
7805ba9a692e55ad925baf0fca762a7ee39ea006Christian MaederCoding out sub-types in HasCASL
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maedercollect the patches for programatica (or create a package)
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder- conv (SN i p) = PN i (S p)
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder+ conv (SN i p) = PN i (Sn (show i) p)
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maederin programatica/tools/base/parse2/NumberNames.hs
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maederfixes translation error of Pair
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskisimplification of HasCASL sentences (omit types)
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederLogic COL is a ruin
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
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis for HasCASL
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder pattern analysis for program equations
96cc01853b72b9d0fdc9e3d309a196a2216de119Christian Maeder implemented only atomic subtyping
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederWeak amalgamation analysis?
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian MaederInstantiate Transformation Application system for HasCASL?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProofs in HasCASL
04ee0d20d16836bb6e835029a807c304973dea46Till MossakowskiCoding HasCASL -> Isabelle with definedness axioms
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski only strict functions are defined
04ee0d20d16836bb6e835029a807c304973dea46Till MossakowskiIsabelle interface
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski One emacs with spec and proof buffer
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski Reload button should rebuild buffers while keeping as much as possible
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski keep structuring of Hets theories
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
69b043b647fa86377c06a8c413c8539f099d8084Till MossakowskiRainer (Klaus)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettichfor ProofManagement-GUI
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich mark imported theorems for selection
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich extend Logic.Prover SenStatus with wasTheorem
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich somewhere in computeTheory implement setting of wasTheorem
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich if wasTheorem not appears with right status in ProofManagementGUI
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich add wasTheorem to Common.Result.Named, as well
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich and adapt conversion functions of SenStatus to Named and vice
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich Mark old theorems in "Axioms to include" Listbox with prefixed
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich add button "Deselect former Theorems"
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich test all this with CASL-lib/Calculi/Space/RCCVerification.het
d03b1fd6ee49eef7fdd2397c05160d8aab6fce92Klaus Luettich all nodes without incoming heterogeneous edges are provable with
c1015e823b467ffb3e58fe3eacb0db58937063baTill Mossakowski************************************************
c1015e823b467ffb3e58fe3eacb0db58937063baTill Mossakowski************************************************
9210840ebaf01ab218cab46322014c4240205060Till Mossakowskisee http://trac.informatik.uni-bremen.de:8080/hets
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettichfor ProofManagement-GUI
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich provide structured (based on spec-names) selection/deselection facility
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettich of axioms and theorems
ed6873e3c28f11208f6873e04a65c3c3aa012ed9Klaus Luettichtrace if liniarity of sentences along development is given
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiConsistency checker interface
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski via global interface, accessible from global and node menus
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder use falseSentence from Logic.Logic (property: holds in no model)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski proved -> inconsistent
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski disproved -> consistent (assuming completeness)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski batch mode for automatic provers such as SPASS
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski (use automatic flag for provers)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskibatch interface for Isabelle
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski each goal is proved separatedly, with a time limit enforced
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski by killing the process
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski the tactic is
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski "using Ax1 ... Axn by auto"
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski where Ax1 ... Axn is the list of all axioms.
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski "auto" could be replaced with "best", "blast" etc. (user selection)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiIgnore axiom selection for interactive provers
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)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich last two ... partially done
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************************************************
ec75b50a89aea0d96fd19ce864225267d0625f25Till MossakowskiBinInt.casl: revealing in Int1 does not work correctly
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskifrom Stefan W�lfl:
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskicomputeTheory does not work across library imports
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskilocal theorems
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiall nodes named
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskihierarchical Isabelle theories
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskidaVinci printing is not adequate
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskihiding of internal nodes does not work
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiFOL without quantifiers and with uniform disjunctions
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski (i.e. x R1 y \/ x R2 y)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski (with and without =)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskialgorithmic path consistency over a relation algebra
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski plug in reasoner for this
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski develop correctness results (algorithmic path consistency=path consistency)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiCASL sublogics:
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski---------------
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiFOL without quantifiers (with and without =)
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiguarded fragment
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski[from DOLCE cooperation:
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskiontology mediation via pushouts/pullbacks/pulations
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiRobinson consistency with shared theory constructed via pre-image?
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskishow theorem links between same instances of different parameterized
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski specs (where one is an extension of the other one)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskilink menu for %implies, $def, %cons, even without open proof obligation
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskifor a proved theorem, show minimal part of DG needed for proof
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskicons, def, mono for nodes
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill MossakowskiIsabelle interface: each qed should write proof info into file
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskiglobally display nodes containing symbols mapped "twice" (i.e. via
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski different signature morphisms)
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski and add a menu for each node allowing for tracking the different
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskitopsort coding: partial functions as relations?
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowskitheorem link menu for proof obligations
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian MaederUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowskiin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
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
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
b2768faecd6610af357407a8ddfe1412a18f8ebcChristian MaederCASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
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- 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
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski use graph grammars to model rules? transformation units?
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
6a5da372804d52203a16e54cea55ee1ae6951d6dChristian Maeder (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!
cc7492cd222f08d17c994912bcb0c60083ae2bc9Till MossakowskiData.Serizable (only when ghc supports it) better: rely on pointer equality
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------------------------