todo revision 0ef6fed7a5d52b1f791926bd8a432723ffd28767
71092d70af35567dd154d3de2ce04ce62e157a7cLennart PoetteringPlan and priority list for CoFI tool activities
7c66aeba0f28cb82027d6015405ed71afa3b6059Kay Sievers************************************************
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering************************************************
05677bb78079c3fa0283101aac2c07581f4873f1Lennart PoetteringSuchfunktion f�r einen Knoten im DG:
73090dc815390f4fca4e3ed8a7e1d3806605daaaLennart Poettering welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers erstmal auf eine Logik (z.B. CASL) beschr�nken
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers - Funktion f�r Morphismus-Suche zwischen Theorien
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
9a36607584bbd1d78775353e022a51794b4e27b1Lennart Poettering - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
a40593a0d0d740efa387e35411e1e456a6c5aba7Lennart PoetteringBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay SieversKonfidenzgrade von Beweisen?
4ce849853c46b1e857df3c6c9e7752159a58ddf1Lennart Poetteringvon Till/Jorina (jfgerken@tzi.de) zu erledigen:
c3090674833c8bd34fbdb0e743f1c47d85dd14fbLennart PoetteringRepr�sentation �ndern:
c3090674833c8bd34fbdb0e743f1c47d85dd14fbLennart Poettering Beweisobjekte an DGs, nicht an Regeln
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering F�r Theoreme in Theorien an Beweisobjekte
822e5dd1d6a1e9b549234281dc3a746768e7e13dLennart Poettering BasicProof mit Liste von Beweisobjekten
9b4a54740884c60e40a2643b535f197b01038850Lennart Poettering Isabelles Beweisobjekte einbinden
9b4a54740884c60e40a2643b535f197b01038850Lennart Poettering Definitionen auszeichnen
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering************************************************
e9fd44b728ff1fc0d1f24fccb87a767f6865df27Lennart Poettering************************************************
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart PoetteringHetCATS, uni und CASL-lib auschecken
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poetteringabstrakte Syntax f�r ConstraintCASL (s. CASL-lib/ConstraintCASL/)
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart Poettering nach HetCATS/ConstraintCASL/AS_ConstraintCASL.der.hs
3040728b6691ea2e9df3a2060e2d49a792bbaedaLennart PoetteringParser f�r ConstraintCASL
78db35f37172f64bfc62cbb2aa364345b7cff0a3Lennart Poettering nach HetCATS/ConstraintCASL/Parse_AS_Basic.hs
78db35f37172f64bfc62cbb2aa364345b7cff0a3Lennart Poettering hets -o ast.het CASL-lib/ConstraintCASL/RCC8.het
78db35f37172f64bfc62cbb2aa364345b7cff0a3Lennart PoetteringFreiburger Constraint-Solver angucken
8b04b925e587ff56568c62ff5ad3f2ea2b34ca7aLennart PoetteringBremer Constraint-Solver angucken
8ed206517c2be381324ac5832bf34cc14024270eLennart Poettering************************************************
8ed206517c2be381324ac5832bf34cc14024270eLennart Poettering************************************************
e6c6e7afffa80ad74efdb1ddfa815294624f1608Lennart Poetteringport CCC to Haskell
8e6054f732b4bc980d3af3e1386ca94b3a602eb8Lennart PoetteringFunktionen imageOfMorphism und inhabited
8e6054f732b4bc980d3af3e1386ca94b3a602eb8Lennart Poettering von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering mit "cvs add SigFuns.hs" einchecken
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering"free datatypes and recursive equations are consistent"
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart PoetteringcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart PoetteringJust True => Yes, is consistent
7361c3b4e1e28a7eb4354a3da354b22e79782141Lennart PoetteringJust False => No, is inconsistent
8b04b925e587ff56568c62ff5ad3f2ea2b34ca7aLennart PoetteringNothing => don't know
7361c3b4e1e28a7eb4354a3da354b22e79782141Lennart Poetteringcall the symbols in the image of the signature morphism "new"
e673ad0415d89c322e5b1a121e411f1b1d8075c0Lennart Poettering- each new sort must be a free type,
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers i.e. it must occur in a sort generation constraint that is marked as free
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers (Sort_gen_ax constrs True)
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers if not, output "don't know"
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers and there must be one term of that sort (inhabited)
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers if not, output "no"
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers- group the axioms according to their leading operation/predicate symbol,
f6113d42d015ad9f3a9e702a09eb8006511a4424Kay Sievers i.e. the f resp. the p in
f6113d42d015ad9f3a9e702a09eb8006511a4424Kay Sievers forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
7a43e910ce00eef22fd42925ae4c85cbea1b1320Kay Sievers Implication Application Strong_equation
d2e83c23f5f0cdd3b6ec05c5c40209708721e704Kay Sievers forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
c55b1b59b837dfd924b704d457ed77c55f8bfeabLennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
822e5dd1d6a1e9b549234281dc3a746768e7e13dLennart Poettering Implication Predication Equivalence
822e5dd1d6a1e9b549234281dc3a746768e7e13dLennart Poettering if there are axioms not being of this form, output "don't know"
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sieverscheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
6c1703cc35b3a5f93ad3cc813fea10cb9a636102Kay Sieverscheck' [] = ([([],[])],emptyUniqSet)
08f9588885c5d65694b324846b0ed19211d2c178Lennart Poettering-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
9ec82de1725ddaab333149171b790d62c47ae133Lennart Poetteringcheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
9ec82de1725ddaab333149171b790d62c47ae133Lennart Poettering | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poetteringcheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering | all_vars ps = (pats, addOneToUniqSet indexs n)
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering (pats,indexs) = check' rs
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering-- falls ein Konstruktor dabei ist: split_by_constructor
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poetteringcheck' qs@((EqnInfo n ctx ps result):_)
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart Poettering | all_vars ps = ([], unitUniqSet n)
220369cc0c3e167af2eee8bdac95a6157e0e2b62Lennart Poettering | constructors = split_by_constructor qs
220369cc0c3e167af2eee8bdac95a6157e0e2b62Lennart Poettering | only_vars = first_column_only_vars qs
220369cc0c3e167af2eee8bdac95a6157e0e2b62Lennart Poettering | otherwise = panic "Check.check': Not implemented :-("
54728c372afe83ad7650201ce7b61d0fa110657cLennart Poettering -- Note: RecPats will have been simplified to ConPats
a73d88fa024b5668ed7dde681e99547d41e6a864Lennart Poettering -- at this stage.
f2d433e178df7df01a836e95775261e1d85ec60dZbigniew Jędrzejewski-Szmek constructors = or (map is_con qs)
f2d433e178df7df01a836e95775261e1d85ec60dZbigniew Jędrzejewski-Szmek only_vars = and (map is_var qs)
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poetteringsubsort definitions: are conservative if formula is satisfiable
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering (generate proof obligation)
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering************************************************
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering************************************************
a19554ed92a7460b4e709cc40c558cde827ab85bLennart PoetteringOWL-DL (<)-> CASL-DL
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poettering some operation symbols
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering show hets output immediately
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering C-c C-g for hets -g
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering when hets terminates abnormally (e.g. with a fail), emacs loops
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering C-n jumps to the next error, but the message windows is not always scrolled
1cb88f2c61f590083847d65cd5a518e834da87d3Lennart Poettering in such a way that the error is at the top (for long error lists)
603cd8fe07cb03e8b11722d1a732e569e5a46347Lennart Poettering Version for XEamcs?
06bf461193b4e7f9936abf7582e8b82e39e187c8Lennart Poettering should work with parser error messages as well (adapt these?)
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart Poettering************************************************
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart Poettering************************************************
936d6fcb6c4fc8839d28f8585af6ba733a7e1a1aLennart PoetteringModal-CASL <-> CASL-DL
edca2e2348b314e2d892fe6f8ae276fdc223f014Thomas Hindoe Paaboel Andersen see Chapter 4 of "The Description Logic Handbook"
ea117d4fde8b8d0b52f9d32ebd4bc09a5bd2ca8bLennart Poettering and ask Klaus for a print out of it
6d0274f11547a0f11200bb82bf598a5a253e12cfLennart Poettering************************************************
6d0274f11547a0f11200bb82bf598a5a253e12cfLennart Poettering************************************************
a7a3f28be404875eff20443a0fa8088bcc4c18dfLennart PoetteringUni-Refactoring,
9a526a06bd22ccaf6641d11323fb04a0512a0e49Lennart Poetteringmake modules hierarchical, change scoped type variables for ghc-6.5
a8985ba3c2ad428bf572c636f9d64c4ce52bfbe7Lennart Poettering(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),
a8985ba3c2ad428bf572c636f9d64c4ce52bfbe7Lennart Poetteringuse HaXml as a cabalized library, provide uni as (one?) cabal
9b27910bb0c23e5225fc1177176e4f9bf9bf787bLennart Poetteringpackage(s), uni used to work under windows as well, watch the
9b27910bb0c23e5225fc1177176e4f9bf9bf787bLennart Poetteringi.e. FilePath, Process discussions (libraries@haskell.org)
b03bfa212dd23397871e36ea32c35cdd8fe43506Lennart Poetteringpossibly switch to a subversion repository, talk to Achim
935fb723ba7370abaf793914fb5a722f7f5e41e1Lennart Poettering(amahnke@tzi.de)
b03bfa212dd23397871e36ea32c35cdd8fe43506Lennart Poettering************************************************
08f9588885c5d65694b324846b0ed19211d2c178Lennart Poettering************************************************
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sieversdevelopment graph calculus
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sievers(see Sect. IV:4.4 of the CASL Reference Manual)
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sieversimplement simplified rule Theorem-Hide-Shift
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sieverstry out examples
7d8197d1f25c1291855bb6cffc705444978c6d8dKay Sieversconservativity calculus
9ee58bddeb6eb044753167e0047fe836479ca5dbKay Sieversweakly amalgamable cocones
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart Poettering************************************************
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart Poettering************************************************
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart Poetteringport hets to windows.
71ef24d09573874c0f7bc323c07c3aec2a458707Lennart PoetteringIf hets should become successful then requests for support under
1b89884ba31cbe98f159ce2c7d6fac5f6a57698fLennart Poetteringwindows will surely follow.
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart PoetteringGhc, uni and uDrawGraph should work under windows. Only Isabelle does
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poetteringnot exist for windows, but SPASS does. Probably only a few path
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poetteringcomputations need to be adapted (made modular) within hets. Also
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poetteringposition computations (of Parsec) should be checked under windows.
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poettering************************************************
1920e37ef9fec04a1fd882f66bfa7a9a5b91c536Lennart Poettering************************************************
a07fdfa376add41d9101d39db25fb2ecb17d5fcaLennart Poetteringrefactor pretty printing
a07fdfa376add41d9101d39db25fb2ecb17d5fcaLennart Poetteringeine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
a07fdfa376add41d9101d39db25fb2ecb17d5fcaLennart Poetteringund andere Formate besser zu unterst�tzen und einheitlichen PP code
a07fdfa376add41d9101d39db25fb2ecb17d5fcaLennart Poettering(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)
f801968466fed39d50d410b30ac828c26722cc95Lennart PoetteringDatentypen (particularly for HasCASL data types) zu bekommen.
f801968466fed39d50d410b30ac828c26722cc95Lennart PoetteringLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
f801968466fed39d50d410b30ac828c26722cc95Lennart Poettering************************************************
409133be63387fc04d927e8aecd2f6ba03d2f143Lennart Poettering************************************************
41f9172f427bdbb8221c64029f78364b8dd4e527Lennart Poetteringeinfaches Merge von lokalen Beweisen eines abgespeichteren DG
178cc7700c23ac088cd7190d7854282075028d91Lennart Poettering in aktuellen DG
de34a42bcad31f0648ac0f249801310e0dbf83f9Lennart Poettering************************************************
98a77df5fe8591034c48e5d56d903ee268de37f9Lennart Poetteringremaining stuff
41f9172f427bdbb8221c64029f78364b8dd4e527Lennart Poettering************************************************
dcf76484ec0612b909e8a160c9a1374f5a6a1cb8Lennart Poetteringset up a ticket and tracking systems (for bugs and features) instead
dcf76484ec0612b909e8a160c9a1374f5a6a1cb8Lennart Poetteringof this messy todo list
41f9172f427bdbb8221c64029f78364b8dd4e527Lennart Poetteringunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs (make
424a19f8a2061c6b058283228734010b2fa24db4Lennart Poetteringit really abstract), possibly contact amahnke@tzi.de regarding
a1cccad1fe88ddd6943e18af97cf7f466296970fLennart Poetteringset up default simplifier
a1cccad1fe88ddd6943e18af97cf7f466296970fLennart Poetteringset up default tactics using axioms
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poettering (see DOLCE sample files)
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poetteringimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poetteringdevelopment graph calculus
8556879e0d14925ce897875c6c264368e2d048c2Lennart Poettering- Stack overflow for "show just subtree"
4a30847b9d71e0381948d68279c8f775b9de7850Lennart Poettering- view-test7.casl should be provable with globDecomp + locDecopm
4a30847b9d71e0381948d68279c8f775b9de7850Lennart Poettering- fail when doing first globDecomp, then local decomp in RelationsAndOrders
b5b46d599524341ddd7407e5dff1021af8ff5089Lennart Poettering- correct MAYA: glob decomp: some links are not found (Jorina)
b5b46d599524341ddd7407e5dff1021af8ff5089Lennart Poettering- Fail: No match in record selector Static.DevGraph.dgn_sign
5e8b28838e493b59628322b69580097ef7dd9384Lennart Poettering for local subsume in RelationsAndOrders
d87be9b0af81a6e07d4fb3028e45c4409100dc26Lennart Poettering************************************************
438bacd18e0b8766c5add47f28b04876272daa97Lennart Poettering************************************************
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poetteringgenerate infrastructure for circular coinduction
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart PoetteringCCS example: commutativity of || by coinduction
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering************************************************
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering************************************************
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poetteringcollect the patches for programatica (or create a package)
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering- conv (SN i p) = PN i (S p)
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poettering+ conv (SN i p) = PN i (Sn (show i) p)
edca2e2348b314e2d892fe6f8ae276fdc223f014Thomas Hindoe Paaboel Andersenin programatica/tools/base/parse2/NumberNames.hs
88f89a9b6d25dfcb89691727c8cdaf01f4090b72Lennart Poetteringfixes translation error of Pair
38a60d7112d33ffd596b23e8df53d75a7c09e71bLennart Poetteringsimplification of HasCASL sentences (omit types)
d8b78264a5245307babbf5af8e39d6d4a1ae095fLennart PoetteringLogic COL is a ruin (with wrongly qualified module names)
d8b78264a5245307babbf5af8e39d6d4a1ae095fLennart Poetteringlogic coding from the comand line with printing of results
7560fffcd2531786b9c1ca657667a43e90331326Lennart PoetteringHaskell modules: hiding, renaming
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering- group the axioms according to their leading operation/predicate symbol,
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering i.e. the f resp. the p in
0790b9fed42eefc4e22dbbe2337cba9713b7848cLennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
5a7e959984788cf89719dec31999409b63bb802bLennart Poettering if there are axioms not being of this form, output error
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart PoetteringMissing points for heterogeneous WADT 04 example:
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering- improve display of HasCASL sigs + mors
edca2e2348b314e2d892fe6f8ae276fdc223f014Thomas Hindoe Paaboel AndersenStatic analysis for HasCASL
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering pattern analysis for program equations
0790b9fed42eefc4e22dbbe2337cba9713b7848cLennart Poettering implemented only atomic subtyping
df1c8f6ac8a45913104b5eeb44f4574689fedd50Lennart PoetteringWeak amalgamation analysis?
5aea932fd54db835b77709ddeba30732648aae53Lennart PoetteringInstantiate Transformation Application system for HasCASL?
918943c75fbd9dee87ff396de3a7c63a8d228433Lennart PoetteringAutomatic generation of Haskell (for a HasCASL subset)
918943c75fbd9dee87ff396de3a7c63a8d228433Lennart PoetteringProofs in HasCASL
8230e26dc954a40d8c9dbc8ddd9376117021f9d2Lennart Poettering************************************************
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart Poettering************************************************
dcfc4b2e5c1af6375488c00bdc6fb8122f86c4d7Lennart PoetteringConnecting Hets with MathServ
4d9909c93e9c58789c71b34555a1908307c6849eLennart Poettering - haifa (http://www.dcs.shef.ac.uk/~simonf/HAIFA.html)
4d9909c93e9c58789c71b34555a1908307c6849eLennart Poettering pros: * relies not on external tool
47ae7201b1df43bd3da83a19e38483b0e5694c99Lennart Poettering * light weight call
47ae7201b1df43bd3da83a19e38483b0e5694c99Lennart Poettering cons: * code is not well maintained
88a6c5894c9d3f85d63b87b040c130366b4006ceKay Sievers * a lot of the deserialization of the answer must be done
6a7353684b65f0107cbdfa0a16ab7717ba257b61Lennart Poettering - call a java program included in MathServ distrib
6a7353684b65f0107cbdfa0a16ab7717ba257b61Lennart Poettering pros: * works imediately
6b78f9b4354010f8af2fe48c783ffd52b2db8f57Lennart Poettering * deserilisation is mostly done in java
6b78f9b4354010f8af2fe48c783ffd52b2db8f57Lennart Poettering cons: * use of external tool
9f8d29834ba97052403e50ec9b358c0470fa4cebLennart Poettering Use modified dfg2tptp to translate SPASS theories into TPTP problems
9f8d29834ba97052403e50ec9b358c0470fa4cebLennart Poettering (ask Klaus for sources)
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering Add possibility to choose a prover out of a list of available provers
68f160039eb78fe122cfe0d4c49695ae91f6f0d1Lennart Poettering (similar to "More fine grained..." and behind more fine grained)
b7def684941808600c344f0be7a2b9fcdda97e0fLennart Poettering Adapt Comorphisms.KnownProvers to select a certain prover at the end of a
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering comorphism automatically
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering Adapt existing SPASS GUI to cover call of the MathServ broker
c66d36e5b5ae81f3c5297d6dacadc13c88c530f6Lennart Poettering by - transforming the grid layout packer into the packer
be0aa78406c73a6625308dc0672b5ff27ec6f9a8Lennart Poettering used in GUI.ProofManagement (easier to maintain and to extend)
be0aa78406c73a6625308dc0672b5ff27ec6f9a8Lennart Poettering - abstraction of certain parts of the GUI into helper functions
461b1822321d6be0d7fd8be29bf3b4993ebd1b85Lennart Poettering forms a new generic Prover-GUI toolkit
461b1822321d6be0d7fd8be29bf3b4993ebd1b85Lennart Poettering - on top of this GUI toolkit
9946996cda11a18b44d82344676e5a0e96339408Lennart Poettering Write a GUI based on the generic Prover-GUI
9946996cda11a18b44d82344676e5a0e96339408Lennart Poettering to call MathServ's Vampire service directly
d1970645411ea1cc083ea1668e0d446252dc1505Lennart Poettering with additional parameters
b4efdf97203ddf781c17f77be84cc61516a077d2Lennart Poettering************************************************
3471bedc005fab03f40b99bf6599645330adcd9eLennart Poettering************************************************
eeb875144e5a80d0521461a139f13fc8014d77d8Lennart PoetteringTranslation between Achim's ontology data structure and CASL (in Hets)
a32f224aafaf47d3489a730259a47ef45781193eLennart Poetteringvisualization of "taxonomy" of CASL signatures
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering (subsorts = inheritance, unary preds = concepts, binary preds = relations)
a32f224aafaf47d3489a730259a47ef45781193eLennart Poettering last two ... partially done
a32f224aafaf47d3489a730259a47ef45781193eLennart Poetteringallgemeine Hets-GUI
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers f�r Anzeige von (un)bewiesenen Goals, ... done
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers bewiesene Goals als Axioms mit ausgeben ... was ist das ???
347e1b6df028ebb1589146c167add8d37a3d4244Kay SieversRecognize guarded fragment of CASL:
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers G ::= forall x . At(x) => G where At is a conjunction of atoms
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers | exists x . At(x) /\ G
347e1b6df028ebb1589146c167add8d37a3d4244Kay SieversJoost Visser wg. ATerms in Haskell => neues Repository
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers************************************************
347e1b6df028ebb1589146c167add8d37a3d4244Kay Sievers************************************************
347e1b6df028ebb1589146c167add8d37a3d4244Kay SieversBeweise in Isabelle
166503dada92d7ca3570a653e07a51ed826b7c8aLennart PoetteringCASL consistency checker
59cea26a349cfa8db906b520dac72563dd773ff2Lennart PoetteringWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
35eb6b124ebdf82bd77aad6e44962a9a039c4d33Lennart Poettering (Vorbild: Larch-Handbuch)
9473414219330b9febc1d0712bbf49ad74cf962fLennart PoetteringSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
f1a8e221ecacea23883df57951e291a910463948Lennart PoetteringParser and static analysis for CSP-CASL
069cfc85f876bb6966cb5a9bbe0235f5064622cdLennart Poettering************************************************
7b63bde1ed0d4f30c799c9b4737fa926465929f9Lennart Poettering************************************************
5b40d33761376354116a8cddb9b9fbdb6c4727d6Lennart PoetteringCASL consistency checker
f7f21d33db5dfe88dc8175c61dada44013347729Lennart PoetteringIsaWin: support CASL-libraries
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart Poettering************************************************
27b5482cc08b7fac1b6b15d980d42ae04f3ae1caLennart Poettering************************************************
b86fa936ce36976cd6a96034cf14ea267695bcb2Lennart PoetteringRegulate concurrent proving
a26336da875a6657d404d1e44b86ae067c34b110Kay Sievers.dg files: store only current library; import .dg files for other libraries
eecd1362f7f4de432483b5d77c56726c3621a83aLennart PoetteringIsabelle: use meta-quantifiers
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringlocal subsumption ?
14038c2e83001abfbcdc3f9f2402189a9b3d2f0cLennart Poetteringbetter syntax (Tina)
14038c2e83001abfbcdc3f9f2402189a9b3d2f0cLennart Poetteringcheck for proved theorems
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart PoetteringAbstractGraphView: switch to Result monad
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart Poetteringunite or rename consCheck and cons_checkers
465349c06d994dd2cc6b6fc4109ac0b9952d500aLennart PoetteringBinInt.casl: revealing in Int1 does not work correctly
d889a2069a87e4617b32ddbdeace5a53a12c699dLennart Poetteringfrom Stefan W�lfl:
eecd1362f7f4de432483b5d77c56726c3621a83aLennart PoetteringcomputeTheory does not work across library imports
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringall nodes named
eecd1362f7f4de432483b5d77c56726c3621a83aLennart Poetteringhierarchical Isabelle theories
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart PoetteringdaVinci printing is not adequate
06dab8e18aebf822392c7ca66c5bf3c1200fdec8Lennart Poetteringhiding of internal nodes does not work
e85647f73e235c2a6ea412cb8d841e092c373501Lennart PoetteringFOL without quantifiers and with uniform disjunctions
e01a15b71e18bf2008aec7e75041ffa42eb80b80Kay Sievers (i.e. x R1 y \/ x R2 y)
a888b352eb53b07daa24fa859ceeb254336b293dLennart Poettering (with and without =)
3b2d5b02ae231f1d3eb0d96eb980155d7797304eLennart Poetteringalgorithmic path consistency over a relation algebra
3b2d5b02ae231f1d3eb0d96eb980155d7797304eLennart Poettering plug in reasoner for this
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering develop correctness results (algorithmic path consistency=path consistency)
3d9a412243035beeaaf3465a62065444a5adf21cLennart PoetteringCASL sublogics:
98ef27df896f36f0407eaa7ed9e295203b9c271bLennart Poettering---------------
a0a3844815b0f346dba03f41245c620f432e462fLennart PoetteringFOL without quantifiers (with and without =)
9efaf380a7c7fa16f44b1aa15b967e99f331203aLennart Poetteringguarded fragment
5ba2dc259f3cdd8fddef68cfd28380a32534e49aKay Sievers[from DOLCE cooperation:
5ba2dc259f3cdd8fddef68cfd28380a32534e49aKay Sieversontology mediation via pushouts/pullbacks/pulations
20ffc4c4a9226b0e45cc02ad9c0108981626c0bbKay SieversRobinson consistency with shared theory constructed via pre-image?
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sieversshow theorem links between same instances of different parameterized
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sievers specs (where one is an extension of the other one)
b45f770f0049fbdf3f6c9db0ab11deeff4ccd86dKay Sieverslink menu for %implies, $def, %cons, even without open proof obligation
b8217b7bd5fd171916a095b150fad4c3a37f5a41Kay Sieversfor a proved theorem, show minimal part of DG needed for proof
08f23fd29c9df9c8b4e874933eb39711f069754bLennart Poetteringcons, def, mono for nodes
08f23fd29c9df9c8b4e874933eb39711f069754bLennart PoetteringIsabelle interface: each qed should write proof info into file
18b754d345ecb0b15e369978aaffa72e9814b86aKay Sieversglobally display nodes containing symbols mapped "twice" (i.e. via
068665b6fd9839f27bcace7e8f56c0baa6935272Lennart Poettering different signature morphisms)
231931ffba1bca9d8759bbd6f797e56f8c6971faLennart Poettering and add a menu for each node allowing for tracking the different
169c4f65131fbc7bcb51e7d5487a715cdcd0e0ebLennart Poetteringtopsort coding: partial functions as relations?
bd08f2422491169e92dc0899d5ba848fcae4c15cLennart Poetteringtheorem link menu for proof obligations
fb0864e7b9c6d26269ccea6ec5c0fd921c029781Lennart PoetteringUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
18da49531e4c6b31bd2439b4d738dc1bb9660af1Lennart Poetteringin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart PoetteringBuffer.het, sublogic of node Buffer:
9586cdfab6a2638078702b7fea7e16b3a71899e2Lennart PoetteringFail: illegal node type in sublogic computation
7f110ff9b8828b477e87de7b28c708cf69a3d008Lennart PoetteringJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
101f077676e9fbe1a66c8b2dc4864a8d7a94c372Lennart Poetteringfor CSP-CASL example: with logic
f7f964eb3625e4cca7f16377fa12aa7a760243e7Lennart Poetteringheterogeneous static ana
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poetteringtheorem links between nodes in different libraries
d0e5a33374cee92962af33dfc03873e470b014f6Lennart PoetteringbasicProofs: use info about used axioms
d0e5a33374cee92962af33dfc03873e470b014f6Lennart Poettering ensure that axiom/thm names are unique
53ed2eeb2e709a6c0d152d7bdf2d9a4b9f997a16Lennart PoetteringOverload / inlineAxioms: injections
a6e87e90ede66815989ba2db92a07102a69906feLennart Poetteringremove "prove" menu in abstracted dg
c4aa65e7147dc742886edf25593e10466b02fc3aLennart Poetteringbetter sublogic analysis in codings
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poetteringthy files in subdir
a558d00381291afd6a81f7df07269fe76eeae556Lennart Poetteringadjust path for thy files, such that hets can also be started from subdirs
a558d00381291afd6a81f7df07269fe76eeae556Lennart PoetteringRestrict Sonjas simplifications to HasCASL
05aa9edde0f9f4077b8120389c93cb0134eda9c5Lennart Poetteringadd suitable axioms to simplifier and CR
05aa9edde0f9f4077b8120389c93cb0134eda9c5Lennart PoetteringcomputeTheory: remove double axioms
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poetteringadd suitable axioms to simplifier and classical reasoner
87a8baa35d6d65ac3b58ae8e26e338e67f8ae8edLennart Poetteringbetter display of internal nodes (use tooltip?)
5ba081b0fb02380cee4c2ff5bc7e05f869eb8415Lennart Poetteringupdate Hets, CASL, daVinci on web page
b3fa47e0819b08ea32e69e19e6d88ce2daca069dLennart PoetteringCASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
7f3e62571a63ac90de6ac5eefeeb8d3e9aa6f49eLennart Poetteringpacking of binaries: add hets-update, refer to TclTk
4cbd9ecf45f64c3a9acc99d473fbf3be3687ae24Lennart Poetteringtest for sublogic before applying comorphism
65c0cf7108ae3537a357c74b4586a783baba82f9Lennart PoetteringMissing points for heterogeneous WADT 04 example:
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers- coding to Isabelle: translate sort gen constraints
f957632b960a0a42999b38ded7089fa602b41745Kay Sievers- Improve adapation to Isabelle's lexis
a2f5666d06fe8233025738047115bb9e3959df3eLennart PoetteringIsabelle: (ask Christoph)
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart Poettering remove datatypes from sort list
ad740100d108282d0244d5739d4dcc86fe4c5fdeLennart Poettering prove local thm link (=> green)
c821bd28c2ecce8d35248d61949fe1c0c3030b6cLennart Poettering "prove" menu with choice windows
de6c78f8795743894431a099d26ec562a8acf3dfLennart Poettering incorporate sublogics
7d441ddb5ca090b5a97f58ac4b4d97b3e84fa81eLennart Poettering sublogic translation table
14e639ae7a1dbf156273ce697d30fbc6c6594209Lennart Poettering better interaction between Isabelle instance (for one node)
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poettering + selection of single goals that are proved
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poettering => use PGIP interface (Christoph, David)
72b9ed828bd22f3ddd74b6853c183eebf006d6d8Lennart Poettering correct show theory
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering Keep proofs and lemmas in .thy files (kind of merge)
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering CASL-like syntax
1d6702e8d3877c0bebf3ac817dc45ff72f5ecfa9Lennart Poettering CASL annotation for lemmas that should be used in proof
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering inherit CASL's mixfix syntax
97f73ffb04947acf0a5854e3a7bdbb7a0105f6faLennart PoetteringSignatures versus theories: where to store additional infos?
85f248b26653f5322c26735661d63d4e8460c30eLennart Poetteringcomp(id,x)=x for comorphism names
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart PoetteringGeneralise CASL2Modal
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart PoetteringMixfix analysis + typecheck for modality axiomatizations
1258097cd3cdbc5dd3d264850119e553a29c5068Lennart PoetteringModal logics: modal logic, temporal logic, mu calculus
a4c279f87451186b8beb1b8cc21c7cad561ecf4bLennart Poettering+ translations (e.g. modal to FOL)
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart PoetteringCASL->Haskell with free DTs (mark sortgens) + recursion
d3fc81bd6a5a046b22600ac1204df220c93d2c15Lennart Poettering- List[Dec] wird List[Pos]
253ee27a0c7a410d27d490bb79ea97caed6a2b68Lennart Poettering- node numbers do not match
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering- thm links with external target should be provable as well
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart PoetteringRemove warnings
f28f1daf754a9a07de90e6fc4ada581bf5de677dLennart PoetteringDifferent types of logic translations
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart PoetteringImprove Static analysis of structured specs
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart PoetteringDevelopment graph calculus, Strategies for DG rules
88a07670cfa974a605c7c7b520b8a3135fce37f9Lennart PoetteringManagement of change
916abb21d0a6653e0187b91591e492026886b0a4Lennart PoetteringIntegrate provers
71092d70af35567dd154d3de2ce04ce62e157a7cLennart Poettering Otter model checker
916abb21d0a6653e0187b91591e492026886b0a4Lennart Poettering FOL-prover by Uli Furhbach
b23de6af893c11da4286bc416455cd0926d1532eLennart Poettering modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
b23de6af893c11da4286bc416455cd0926d1532eLennart Poettering Isabelle codings: www.inf.ethz.ch/~vigano
21bdae12e11ae20460715475d8a0c991f15464acLennart Poettering Renate Schmidt, Manchester: uses FOL prover for description logic
21bdae12e11ae20460715475d8a0c991f15464acLennart Poettering (as efficient as DL-specific tools!)
9534ce54858c67363b841cdbdc315140437bfdb4Lennart Poettering Look at PROSPER toolkit
9534ce54858c67363b841cdbdc315140437bfdb4Lennart Poettering consistency: see IJCAR-workshop on non-provability in Cork
68c7d001f4117f0c3d0a4582e32cbb03ae5fac57Lennart Poettering IJCAR workshop about logical frameworks and meta-languages
796b06c21b62d13c9021e2fbd9c58a5c6edb2764Kay SieversIntegrate CCC
5d0fcd7c8d29340ac9425c309e8ac436a9af699cLennart PoetteringKlaus' wayfinding example
8bbabc447b1d913bd21faf97c7b17d20d315d2b4Lennart Poetteringask Detlef: critical pairs, Fossacs paper by Francesco
e707c49485b8f4f2ec040d3da232d39153e650b9Lennart PoetteringUniForM workbench:
a19554ed92a7460b4e709cc40c558cde827ab85bLennart Poetteringfirst steps towards CASL instance, using ATerms and re-using MMISS instance
a73d88fa024b5668ed7dde681e99547d41e6a864Lennart Poetteringvariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
73090dc815390f4fca4e3ed8a7e1d3806605daaaLennart PoetteringIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
44143309dd0b37d61d7d842ca58f01a65646ec71Kay Sievers Grothendieck logic)
3d57c6ab801f4437f12948e29589e3d00c3ad9dbLennart Poettering + for TAS: reflection of HOL in HOL, to be composed with encodings
935fb723ba7370abaf793914fb5a722f7f5e41e1Lennart Poettering (i.e. signatures, axioms, signature morphisms in HOL,
b9a2a36b519ccd79c4198e7dda4e657d597a14adLennart Poettering re-use ML signatures) (Einar)
9408a2d295a312a5472345090e28e0502570494bLennart PoetteringDisplay Specs as daVinci subgraphs
3f7a8c4e9f1d3ce48919e24eb2c9d56dd6fd88d8Kay SieversUser interface
f9276855a1d270b6c3f857cdaf2c4b49920c2228Lennart PoetteringLogic graph window
260abb780a135e4cae8c10715c7e85675efc345aLennart PoetteringInput text window
260abb780a135e4cae8c10715c7e85675efc345aLennart PoetteringDevelopment graph window
a8f11321c209830a35edd0357e8def5d4437d854Lennart Poettering************************************************
21bdae12e11ae20460715475d8a0c991f15464acLennart Poettering************************************************
c32e0c40f7e706e3ebcd101187d5ced96f083491Lennart PoetteringHets 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)