2N/APlan and priority list for CoFI tool activities
2N/A************************************************
2N/A************************************************
2N/AInterface Hets <-> ISabelle
2N/A Hets muss eine Pipe als Inode erzeugen
2N/A und dann auf Beweisterme warten
2N/A und auf "Ende" warten
2N/A und dann Proof_status sen proof_tree entsprechend ausf�llen
58N/A Beweisterme (siehe Kapitel im RefMan)
2N/A ML "proofs := 1" (am Anfang des .thy file)
2N/A am Ende jedes Theorems: Beweisterm in die Pipe schreiben
2N/A (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
23N/A und Start- und Endmarker
23N/A am Schluss "Ende" ausgeben
32N/A Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
32N/A************************************************
32N/A************************************************
58N/Adevelopment graph calculus
32N/A- Stack overflow for "show just subtree"
225N/A- fail when doing first globDecomp, then local decomp in RelationsAndOrders
225N/A- correct MAYA: glob decomp: some links are not found (Jorina)
225N/A for local subsume in RelationsAndOrders
225N/A************************************************
225N/A************************************************
38N/A************************************************
83N/A************************************************
92N/AFunktionen imageOfMorphism und inhabited
34N/A"free datatypes and recursive equations are consistent"
313N/AcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
313N/AJust True => Yes, is consistent
313N/AJust False => No, is inconsistent
34N/ANothing => don't know
313N/Acall the symbols in the image of the signature morphism "new"
34N/A- each new sort must be a free type,
70N/A i.e. it must occur in a sort generation constraint that is marked as free
2N/A (Sort_gen_ax constrs True)
2N/A such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
2N/A if not, output "don't know"
2N/A and there must be one term of that sort (inhabited)
70N/A if not, output "no"
2N/A forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
70N/A forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
70N/A Implication Application Strong_equation
70N/A forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
70N/A forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
70N/A Implication Predication Equivalence
70N/A if there are axioms not being of this form, output "don't know"
6N/Acheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
6N/Acheck' [] = ([([],[])],emptyUniqSet)
34N/A-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
34N/Acheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
34N/A | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
34N/A-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
34N/Acheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
34N/A | all_vars ps = (pats, addOneToUniqSet indexs n)
38N/A (pats,indexs) = check' rs
38N/A-- falls ein Konstruktor dabei ist: split_by_constructor
34N/A-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
92N/Acheck' qs@((EqnInfo n ctx ps result):_)
145N/A | all_vars ps = ([], unitUniqSet n)
500N/A | constructors = split_by_constructor qs
500N/A | only_vars = first_column_only_vars qs
500N/A -- Note: RecPats will have been simplified to ConPats
500N/A constructors = or (map is_con qs)
92N/A only_vars = and (map is_var qs)
92N/A************************************************
92N/A************************************************
-------------------------------------------------------------------
eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
und andere Formate besser zu unterst�tzen und einheitlichen PP code
f�r die CASL Datentypen zu bekommen.
HasCASL hat auch noch keine Mixfix- und Latex Ausgabe.
************************************************
************************************************
logic coding form the comand line with printing of results
Haskell modules: hiding, renaming
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
checking class constraints of terms
pattern analysis for program equations
- for simple types (currently type synonyms)
Weak amalgamation analysis?
Instantiate Transformation Application system for HasCASL?
Automatic generation of Haskell (for a HasCASL subset)
************************************************
************************************************
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
Joost Visser wg. ATerms in Haskell => neues Repository
************************************************
************************************************
Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
(Vorbild: Larch-Handbuch)
Parser and static analysis for CSP-CASL
************************************************
************************************************
IsaWin: support CASL-libraries
************************************************
************************************************
theorem links between nodes in different libraries
basicProofs: use info about used axioms
Overload / inlineAxioms: injections
GUI: use daVinci close button;
use Workbench tool registration for central shutdown
use save button for saving proof info
remove "prove" menu in abstracted dg
better sublogic analysis in codings
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
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
sublogic translation table
better interaction between Isabelle instance (for one node)
+ selection of single goals that are proved
=> use PGIP interface (Christoph, David)
Keep proofs and lemmas in .thy files (kind of merge)
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
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
Different types of logic translations
Improve Static analysis of structured specs
Development graph calculus, Strategies for DG rules
FOL-prover by Uli Furhbach
modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
Renate Schmidt, Manchester: uses FOL prover for description logic
(as efficient as DL-specific tools!)
consistency: see IJCAR-workshop on non-provability in Cork
IJCAR workshop about logical frameworks and meta-languages
Klaus' wayfinding example
ask Detlef: critical pairs, Fossacs paper by Francesco
first steps towards CASL instance, using ATerms and re-using MMISS instance
variants for specs (needed for DOLCE: CASL variant, DL variant, ...)
+ 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
************************************************
************************************************
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
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...?)
integrate QuickCheck: come to lecture!
++++++++++++++++++++++++++++++++++++++++++++++++
++++++++++++++++++++++++++++++++++++++++++++++++
Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
Proofs with basic datatypes
Verbesserung der Fehlermeldungen
Example of Agnes und Frank: proofs in HOL-CASL (2 days)
Examples for cond rewriting -> Christophe
Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?
Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS
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)
Generate Proof obligations (1 week)
Add renaming to Isabelle kernel (2 months)
Repository mit korrekten und fehlerhaften Specs
HetCATS User manual, Doku fuer Environments (2 weeks)
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
Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
Neues Tool-Schaubild auf Web-Seiten ver�ffentlichen
{- This does not work due to needed ordering:
instance Functor Set where
m >>= k = unionManySets (setToList (fmap k m))
[("normal","normal","normal"),
("normal","inclusion","normal"),
("inclusion","normal","normal"),
("inclusion","inclusion","inclusion")]
Aufbau des Graphen selbst