todo revision b021b399b59fb7009308ed7a3eda30182dea7976
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImmanuel
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSuchfunktion f�r einen Knoten im DG:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski erstmal auf eine Logik (z.B. CASL) beschr�nken
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - Funktion f�r Morphismus-Suche zwischen Theorien
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKonfidenzgrade von Beweisen?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowskivon Till/Jorina (jfgerken@tzi.de) zu erledigen:
f1ba3c4b1394e88800bece2e9067e2866015cfebTill MossakowskiRepr�sentation �ndern:
f1ba3c4b1394e88800bece2e9067e2866015cfebTill Mossakowski Beweisobjekte an DGs, nicht an Regeln
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowski F�r Theoreme in Theorien an Beweisobjekte
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski BasicProof mit Liste von Beweisobjekten
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Isabelles Beweisobjekte einbinden
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Definitionen auszeichnen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFlorian (Till)
e927ace91d729fa35f6b1d08faf84af28cd139e9Till Mossakowski************************************************
e927ace91d729fa35f6b1d08faf84af28cd139e9Till Mossakowski
e927ace91d729fa35f6b1d08faf84af28cd139e9Till Mossakowskiabstrakte Syntax f�r ConstraintCASL (s. CASL-lib/ConstraintCASL/)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski nach HetCATS/ConstraintCASL/AS_ConstraintCASL.der.hs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiParser f�r ConstraintCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski nach HetCATS/ConstraintCASL/Parse_AS_Basic.hs
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowskibeides in HetCATS/ConstraintCASL/Logic_ConstraintCASL.hs einh�ngen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (mit Till)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski************************************************
ed892c579cca270fff0aa9cc2a34351c420e3182Till MossakowskiMingyi (Till)
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski************************************************
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowskiport CCC to Haskell
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFunktionen imageOfMorphism und inhabited
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski mit "cvs add SigFuns.hs" einchecken
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiNew module FreeTypes.hs:
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski"free datatypes and recursive equations are consistent"
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskicheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiJust True => Yes, is consistent
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiJust False => No, is inconsistent
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till MossakowskiNothing => don't know
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowskicall the symbols in the image of the signature morphism "new"
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski- each new sort must be a free type,
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski i.e. it must occur in a sort generation constraint that is marked as free
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (Sort_gen_ax constrs True)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski if not, output "don't know"
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski and there must be one term of that sort (inhabited)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski if not, output "no"
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- group the axioms according to their leading operation/predicate symbol,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski i.e. the f resp. the p in
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski Implication Application Strong_equation
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski Implication Predication Equivalence
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski if there are axioms not being of this form, output "don't know"
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskicheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskicheck' [] = ([([],[])],emptyUniqSet)
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowskicheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | all_vars ps = (pats, addOneToUniqSet indexs n)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski where
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski (pats,indexs) = check' rs
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-- falls ein Konstruktor dabei ist: split_by_constructor
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maedercheck' qs@((EqnInfo n ctx ps result):_)
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder | all_vars ps = ([], unitUniqSet n)
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder | constructors = split_by_constructor qs
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder | only_vars = first_column_only_vars qs
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder | otherwise = panic "Check.check': Not implemented :-("
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder where
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski -- Note: RecPats will have been simplified to ConPats
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder -- at this stage.
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski constructors = or (map is_con qs)
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder only_vars = and (map is_var qs)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskisubsort definitions: are conservative if formula is satisfiable
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (generate proof obligation)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHeng (Klaus)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiOWL-DL logic
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiOWL-DL (<)-> CASL-DL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiemacs mode:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski some operation symbols
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski show hets output immediately
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski C-c C-g for hets -g
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski when hets terminates abnormally (e.g. with a fail), emacs loops
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski C-n jumps to the next error, but the message windows is not always scrolled
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski in such a way that the error is at the top (for long error lists)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Version for XEamcs?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski should work with parser error messages as well (adapt these?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHilfskraft 1
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModal-CASL <-> CASL-DL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski see Chapter 4 of "The Description Logic Handbook"
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski and ask Klaus for a print out of it
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHilfskraft 2
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUni-Refactoring, make modules hierarchical, change scoped type
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivariables for ghc-6.5 (and older ghcs), replace deprecated code
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(i.e. FiniteMap, hslibs), use HaXml as a cabalized library, provide
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiuni as (one?) cabal package(s), uni used to work under windows as well,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiwatch the i.e. FilePath, Process discussions (libraries@haskell.org)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill MossakowskiHilfskraft 3
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill Mossakowski************************************************
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiEntwicklungsgraph-Kalk�l
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski************************************************
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiHilfskraft 5
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski************************************************
dedca4980b2d43bc343ffcaf73e0617524f9720cTill Mossakowski
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowskirefactor pretty printing
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskieine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiund andere Formate besser zu unterst�tzen und einheitlichen PP code
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiDatentypen (particularly for HasCASL data types) zu bekommen.
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski
e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskiLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski************************************************
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiHilfskraft 6
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski************************************************
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowskieinfaches Merge von lokalen Beweisen eines abgespeichteren DG
88c65bd4e8841502546923da0e81ade9045e8fecTill Mossakowski in aktuellen DG
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski************************************************
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiremaining stuff
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski************************************************
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiset up default simplifier
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiset up default tactics using axioms
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski (see DOLCE sample files)
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiFunktion basicInferenceNode in Proofs/Proofs.hs:
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskidevelopment graph calculus
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- Stack overflow for "show just subtree"
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- view-test7.casl should be provable with globDecomp + locDecopm
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- fail when doing first globDecomp, then local decomp in RelationsAndOrders
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski- correct MAYA: glob decomp: some links are not found (Jorina)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- Fail: No match in record selector Static.DevGraph.dgn_sign
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski for local subsume in RelationsAndOrders
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiDaniel
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskigenerate infrastructure for circular coinduction
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCCS example: commutativity of || by coinduction
2ee1615e999c5e0c49508ed4fcced7344b050042Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
f69658e57cba7ecb37c0d84181f4c563215c2534Till MossakowskiChristian
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicollect the patches for programatica (or create a package)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- conv (SN i p) = PN i (S p)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski+ conv (SN i p) = PN i (Sn (show i) p)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiin programatica/tools/base/parse2/NumberNames.hs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifixes translation error of Pair
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskisimplification of HasCASL sentences (omit types)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogic COL is a ruin (with wrongly qualified module names)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilogic coding from the comand line with printing of results
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHaskell modules: hiding, renaming
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- group the axioms according to their leading operation/predicate symbol,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski i.e. the f resp. the p in
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski if there are axioms not being of this form, output error
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- improve display of HasCASL sigs + mors
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis for HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski pattern analysis for program equations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski implemented only atomic subtyping
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeak amalgamation analysis?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInstantiate Transformation Application system for HasCASL?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProofs in HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCase study
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
38f30f746aa42d4fc659a15e183801f2f74596d0Till MossakowskiNN (Klaus)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiConnecting Hets with MathServ
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Either use
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - haifa (http://www.dcs.shef.ac.uk/~simonf/HAIFA.html)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski pros: * relies not on external tool
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski * light weight call
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski cons: * code is not well maintained
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski * a lot of the deserialization of the answer must be done
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski in Haskell
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - call a java program included in MathServ distrib
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski pros: * works imediately
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski * deserilisation is mostly done in java
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski cons: * use of external tool
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Use modified dfg2tptp to translate SPASS theories into TPTP problems
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (ask Klaus for sources)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Add possibility to choose a prover out of a list of available provers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (similar to "More fine grained..." and behind more fine grained)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Adapt Comorphisms.KnownProvers to select a certain prover at the end of a
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski comorphism automatically
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Adapt existing SPASS GUI to cover call of the MathServ broker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski by - transforming the grid layout packer into the packer
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski used in GUI.ProofManagement (easier to maintain and to extend)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - abstraction of certain parts of the GUI into helper functions
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski forms a new generic Prover-GUI toolkit
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - on top of this GUI toolkit
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Write a GUI based on the generic Prover-GUI
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski to call MathServ's Vampire service directly
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski with additional parameters
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKlaus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivisualization of "taxonomy" of CASL signatures
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski last two ... partially done
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiallgemeine Hets-GUI
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski f�r Anzeige von (un)bewiesenen Goals, ... done
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski bewiesene Goals als Axioms mit ausgeben ... was ist das ???
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
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 Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMarkus, Lutz
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBeweise in Isabelle
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (Vorbild: Larch-Handbuch)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiParser and static analysis for CSP-CASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiChristoph
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsaWin: support CASL-libraries
************************************************
Till
************************************************
Regulate concurrent proving
.dg files: store only current library; import .dg files for other libraries
Markus' Bsp:
Isabelle: use meta-quantifiers
local subsumption ?
better syntax (Tina)
check for proved theorems
AbstractGraphView: switch to Result monad
unite or rename consCheck and cons_checkers
BinInt.casl: revealing in Int1 does not work correctly
from Stefan W�lfl:
computeTheory does not work across library imports
local theorems
all nodes named
hierarchical Isabelle theories
daVinci printing is not adequate
hiding of internal nodes does not work
CSPs
----
FOL without quantifiers and with uniform disjunctions
(i.e. x R1 y \/ x R2 y)
(with and without =)
algorithmic path consistency over a relation algebra
plug in reasoner for this
develop correctness results (algorithmic path consistency=path consistency)
within CASL
CASL sublogics:
---------------
FOL without quantifiers (with and without =)
guarded fragment
Prop
[from DOLCE cooperation:
quit wish!
ontology mediation via pushouts/pullbacks/pulations
Robinson consistency with shared theory constructed via pre-image?
show theorem links between same instances of different parameterized
specs (where one is an extension of the other one)
link menu for %implies, $def, %cons, even without open proof obligation
for a proved theorem, show minimal part of DG needed for proof
cons, def, mono for nodes
Isabelle interface: each qed should write proof info into file
globally display nodes containing symbols mapped "twice" (i.e. via
different signature morphisms)
and add a menu for each node allowing for tracking the different
uses of the symbols/concepts
topsort coding: partial functions as relations?
]
theorem link menu for proof obligations
UserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
in Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
correctly.
Buffer.het, sublogic of node Buffer:
Fail: illegal node type in sublogic computation
J�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
for CSP-CASL example: with logic
heterogeneous static ana
theorem links between nodes in different libraries
basicProofs: use info about used axioms
ensure that axiom/thm names are unique
Overload / inlineAxioms: injections
remove "prove" menu in abstracted dg
better sublogic analysis in codings
thy files in subdir
adjust path for thy files, such that hets can also be started from subdirs
Restrict Sonjas simplifications to HasCASL
add suitable axioms to simplifier and CR
computeTheory: remove double axioms
add suitable axioms to simplifier and classical reasoner
better display of internal nodes (use tooltip?)
update Hets, CASL, daVinci on web page
CASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
packing of binaries: add hets-update, refer to TclTk
CCC interface
test for sublogic before applying comorphism
Missing points for heterogeneous WADT 04 example:
- coding to Isabelle: translate sort gen constraints
- Improve adapation to Isabelle's lexis
Isabelle: (ask Christoph)
remove datatypes from sort list
prove local thm link (=> green)
"prove" menu with choice windows
incorporate sublogics
sublogic translation table
better interaction between Isabelle instance (for one node)
+ selection of single goals that are proved
=> use PGIP interface (Christoph, David)
correct show theory
Keep proofs and lemmas in .thy files (kind of merge)
CASL-like syntax
CASL annotation for lemmas that should be used in proof
inherit CASL's mixfix syntax
Signatures versus theories: where to store additional infos?
comp(id,x)=x for comorphism names
Generalise CASL2Modal
Mixfix analysis + typecheck for modality axiomatizations
Modal logics: modal logic, temporal logic, mu calculus
+ translations (e.g. modal to FOL)
CASL->Haskell with free DTs (mark sortgens) + recursion
- List[Dec] wird List[Pos]
- node numbers do not match
- thm links with external target should be provable as well
Remove warnings
Different types of logic translations
Improve Static analysis of structured specs
Development graph calculus, Strategies for DG rules
Management of change
Integrate provers
Otter model checker
FOL-prover by Uli Furhbach
modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
Isabelle codings: www.inf.ethz.ch/~vigano
Renate Schmidt, Manchester: uses FOL prover for description logic
(as efficient as DL-specific tools!)
Look at PROSPER toolkit
consistency: see IJCAR-workshop on non-provability in Cork
IJCAR workshop about logical frameworks and meta-languages
Integrate CCC
Encodings
Errors:
Klaus' wayfinding example
ask Detlef: critical pairs, Fossacs paper by Francesco
UniForM workbench:
first steps towards CASL instance, using ATerms and re-using MMISS instance
variants for specs (needed for DOLCE: CASL variant, DL variant, ...)
Integration of MAYA and Isabelle/HOL (global HOL-Coding of
Grothendieck logic)
+ for TAS: reflection of HOL in HOL, to be composed with encodings
(i.e. signatures, axioms, signature morphisms in HOL,
re-use ML signatures) (Einar)
Display Specs as daVinci subgraphs
User interface
--------------
Logic graph window
Input text window
Development graph window
Prover windows
************************************************
FOR STUDENTS
************************************************
Hets 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)
Packaging of installation
GUI (vgl. VSE)
with Eclipse, WXHaskell or GTk?
how to integrate with event system of UniForM workbench?
integrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
this interacts with GUI!
Data.Serizable (only when ghc supports it) better: rely on pointer equality
XML interface
increase performance
integrate QuickCheck: come to lecture!
++++++++++++++++++++++++++++++++++++++++++++++++
Remaining things
++++++++++++++++++++++++++++++++++++++++++++++++
Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
Coq, PTT in Maude
Proofs with basic datatypes
Verbesserung der Fehlermeldungen
Improve encoding: CATS/basic_encode.sml (3 days)
More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
Renamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
Example of Agnes und Frank: proofs in HOL-CASL (2 days)
Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
Examples for cond rewriting -> Christophe
Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?
Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS
HOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
HOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
HOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
Encoding of structured free (3 days)
Encoding of structured cofree (2 weeks)
Eingabesyntax als Mix zwischen CASL und HOL (3 days)
Adapt Isabelle unions to CASL unions (1 week)
IsaWin git/src/isa_ext/casl_thy.sml (1 week)
Generate Proof obligations (1 week)
Add renaming to Isabelle kernel (2 months)
Basic datatypes CASL-lib/Basic/basic.casl
Repository mit korrekten und fehlerhaften Specs
HetCATS User manual, Doku fuer Environments (2 weeks)
Conversion ASF/SDF-Parser -> abstract syntax (in Haskell)
Comparsion of parsers (ML-yacc parser, SDF-Parser)
Conversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
PVS anbinden (Kooperation mit Cachan?)
Portations: Intel-Solaris, Mac OS-10 (2 weeks)
(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
Views on CASL specs: CATS/viewer.sml (2 weeks)
Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
Module graph CATS/module_graph.sml (1 week) -> Maya?
ATerms via XML: CATS/aterms.sml (2 weeks)
Neues Tool-Schaubild auf Web-Seiten ver�ffentlichen
Library management: CATS/lib_ana.sml (2 weeks)
Version management/Uniform Workbench: CATS/lib_ana.sml (2 months)
{- This does not work due to needed ordering:
instance Functor Set where
fmap = mapSet
instance Monad Set where
return = unitSet
m >>= k = unionManySets (setToList (fmap k m))
-}
Aufbau von comptable
--------------------
[("normal","normal","normal"),
("normal","inclusion","normal"),
("inclusion","normal","normal"),
("inclusion","inclusion","inclusion")]
Aufbau von ginfo
--------------------
Mit initgraphs erzeugen
Aufbau des Graphen selbst
------------------------
addnode
addlink