8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynPlan and priority list for CoFI tool activities

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynTina (Till)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynList.casl should go through

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynrename clashing names

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynset up default simplifier

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynset up default tactics using axioms

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn (see DOLCE sample files)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynSonja (Till)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynin Isabelle/IsaPrint.hs:

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynrename variables that conflict with operation syntax

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn (or restrict mixfix decls for consts)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyndie Mixfix-Deklarationen f�hren noch zu Problemen.

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

9ec45e7faa3648a36cb01aed9e230bd49b450fe0Serge Hallynconsts

9ec45e7faa3648a36cb01aed9e230bd49b450fe0Serge Hallyn c::t ("c")

9ec45e7faa3648a36cb01aed9e230bd49b450fe0Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynf�hrt dazu, dass c nicht mehr als Variable verwendet werden kann.

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynK�nntest du diese Mixfix-Deklarationen auf die notwendigen F�lle

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynbeschr�nken, und ggf. die Variablen umbenennen?

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynZudem m�ssen Underscores escaped werden:

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynconsts

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn C_1::t ("C'_1")

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynDiplom: Encoding for HasCASL in Isabelle/HOL(CF)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynInterface Hets <-> ISabelle

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynin IsaProve.hs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn Hets muss eine Pipe als Inode erzeugen

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn und dann auf Beweisterme warten

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn und auf "Ende" warten

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn und dann Proof_status sen proof_tree entsprechend ausf�llen

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn (siehe Logic/Prover.hs)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn Beweisterme (siehe Kapitel im RefMan)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn ML "proofs := 1" (am Anfang des .thy file)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn am Ende jedes Theorems: Beweisterm in die Pipe schreiben

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn mit pretty_proof_of und Pretty.string_of

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn und Start- und Endmarker

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn am Schluss "Ende" ausgeben

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynFunktion basicInferenceNode in Proofs/Proofs.hs:

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynEmacs: uni/emacs, George fragen (ger@)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynJorina (Till)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynGUI:

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn use save button for saving proof info

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyndevelopment graph calculus

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn- Stack overflow for "show just subtree"

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn- view-test7.casl should be provable with globDecomp + locDecopm

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn- fail when doing first globDecomp, then local decomp in RelationsAndOrders

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn- correct MAYA: glob decomp: some links are not found (Jorina)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn- Fail: No match in record selector Static.DevGraph.dgn_sign

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn for local subsume in RelationsAndOrders

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynMingyi (Till)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynport CCC to Haskell

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynFunktionen imageOfMorphism und inhabited

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn mit "cvs add SigFuns.hs" einchecken

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynNew module FreeTypes.hs:

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn"free datatypes and recursive equations are consistent"

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallyncheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynJust True => Yes, is consistent

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynJust False => No, is inconsistent

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynNothing => don't know

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyncall the symbols in the image of the signature morphism "new"

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn- each new sort must be a free type,

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn i.e. it must occur in a sort generation constraint that is marked as free

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn (Sort_gen_ax constrs True)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn if not, output "don't know"

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn and there must be one term of that sort (inhabited)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn if not, output "no"

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn- group the axioms according to their leading operation/predicate symbol,

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn i.e. the f resp. the p in

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn Implication Application Strong_equation

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn Implication Predication Equivalence

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn if there are axioms not being of this form, output "don't know"

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyncheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyncheck' [] = ([([],[])],emptyUniqSet)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn-- nur ein Pattern, bestehend aus nur Variablen? fertig, True

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyncheck' [EqnInfo n ctx ps (MatchResult CanFail _)]

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyncheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn | all_vars ps = (pats, addOneToUniqSet indexs n)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn where

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn (pats,indexs) = check' rs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn-- falls ein Konstruktor dabei ist: split_by_constructor

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn-- wenn die ersten Argument nur Variablen sind: first_column_only_vars

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyncheck' qs@((EqnInfo n ctx ps result):_)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn | all_vars ps = ([], unitUniqSet n)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn | constructors = split_by_constructor qs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn | only_vars = first_column_only_vars qs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn | otherwise = panic "Check.check': Not implemented :-("

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn where

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn -- Note: RecPats will have been simplified to ConPats

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn -- at this stage.

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn constructors = or (map is_con qs)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn only_vars = and (map is_var qs)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynsubsort definitions: are conservative if formula is satisfiable

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn (generate proof obligation)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynHeng (Klaus)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynLaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynemacs mode:

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn some operation symbols

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn show hets output immediately

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn C-c C-g for hets -g

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn when hets terminates abnormally (e.g. with a fail), emacs loops

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn C-n jumps to the next error, but the message windows is not always scrolled

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn in such a way that the error is at the top (for long error lists)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn Version for XEamcs?

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynOWL-DL logic

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynOWL-DL -> CASL

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn-------------------------------------------------------------------

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynLaTeX pretty printer

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyneine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynund andere Formate besser zu unterst�tzen und einheitlichen PP code

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynf�r die CASL Datentypen zu bekommen.

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynHasCASL hat auch noch keine Mixfix- und Latex Ausgabe.

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynDaniel

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyngenerate infrastructure for circular coinduction

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynCCS example: commutativity of || by coinduction

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynChristian

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn************************************************

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyncollect the patches for programatica (or create a package)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn- conv (SN i p) = PN i (S p)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn+ conv (SN i p) = PN i (Sn (show i) p)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynin programatica/tools/base/parse2/NumberNames.hs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynfixes translation error of Pair

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynsimplification of HasCASL sentences (omit types)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynanalyse the ghc-6.4 difference in Logic/Comorphism.hs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge HallynLogic COL is a ruin (with wrongly qualified module names)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynnon-free/generated datatype declarations generate ga-axioms

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn(this is indented)

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynpretty printing mangles trailing and preceding annotations

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynallow more annotations in structured specs

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallynthe type FIT_ARG should be changed to

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyndata FIT_ARG = Fit_spec (Annoted SPEC) [G_mapping] [Pos]

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn -- pos: opt "fit"

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn | Fit_view VIEW_NAME [Annoted FIT_ARG] [Pos]

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn -- annotations before view are stored elsewhere

8aa1044fd83c407e38c66a1ff46a9edfe02d7c78Serge Hallyn

homogenizeGM should be moved to Static.AnalysisStructured

logic coding from the comand line with printing of results

(started -v5)

Haskell modules: hiding, renaming

- group the axioms according to their leading operation/predicate symbol,

i.e. the f resp. the p in

forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t

forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi

if there are axioms not being of this form, output error

Missing points for heterogeneous WADT 04 example:

- improve display of HasCASL sigs + mors

Static analysis for HasCASL

pattern analysis for program equations

implemented only atomic subtyping

Weak amalgamation analysis?

Instantiate Transformation Application system for HasCASL?

Automatic generation of Haskell (for a HasCASL subset)

Proofs in HasCASL

Case study

************************************************

Klaus

************************************************

CASL -> SPASS

Coding of subsorts as unary predicates (for ontologies)

Translation between Achim's ontology data structure and CASL (in Hets)

visualization of "taxonomy" of CASL signatures

(subsorts = inheritance, unary preds = concepts, binary preds = relations)

Recognize guarded fragment of CASL:

G ::= forall x . At(x) => G where At is a conjunction of atoms

| exists x . At(x) /\ G

Joost Visser wg. ATerms in Haskell => neues Repository

************************************************

Markus, Lutz

************************************************

Beweise in Isabelle

CASL consistency checker

Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen

(Vorbild: Larch-Handbuch)

Simpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln

Parser and static analysis for CSP-CASL

************************************************

Christoph

************************************************

CASL consistency checker

IsaWin: support CASL-libraries

************************************************

Till

************************************************

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

List.casl: quantifiers in theory generated by "show theory" missing

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

spec VarTestIncorrect =

sorts s,t

vars x:s; y:t

forall x:t; y:s

. x = y

end

spec VarTestCorrect =

sorts s,t

%% vars x:s; y:t

forall x:t; y:s

. x = y

end

Incorrect geht durch, weil die Typanalyse nicht funktioniert und Correct

wird abgelehnt, weil x und y nicht denselben Typ haben, was das richtige

Verhalten auch im ersten Fall w\x{00E4}re.

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)]

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]

- George wg. Schlie�en von Fenstern

- 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