todo revision 3e2c4de10a0eb284938b5d5307d1c1fc2f799456
Plan and priority list for CoFI tool activities
************************************************
Sonja (Till)
************************************************
Diplom: Encoding for HasCASL in Isabelle/HOL(CF)
************************************************
Jorina (Till)
************************************************
development graph calculus
- Stack overflow for "show just subtree"
- view-test7.casl should be provable with globDecomp + locDecopm
- fail when doing first globDecomp, then local decomp in RelationsAndOrders
- correct MAYA: glob decomp: some links are not found (Jorina)
************************************************
Martin (Till)
************************************************
type check for CASL
documentation
*** Error encode.casl:8.30, No correct typing for
************************************************
Mingyi (Till)
************************************************
port CCC to Haskell
Funktionen imageOfMorphism und inhabited
von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
mit "cvs add SigFuns.hs" einchecken
New module FreeTypes.hs:
"free datatypes and recursive equations are consistent"
checkFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
Just True => Yes, is consistent
Just False => No, is inconsistent
Nothing => don't know
call the symbols in the image of the signature morphism "new"
- each new sort must be a free type,
i.e. it must occur in a sort generation constraint that is marked as free
(Sort_gen_ax constrs True)
such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
if not, output "don't know"
and there must be one term of that sort (inhabited)
if not, output "no"
- 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 . f(t_1,...,t_m)=t
forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
Implication Application Strong_equation
forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
Implication Predication Equivalence
if there are axioms not being of this form, output "don't know"
************************************************
Zicheng (Till)
************************************************
Translation from CASL with subsorts to CASL without subsorts
see CATS/basic_encode.sml, encode SubCFOL into CFOL
encode subsorting by injection functions
1. translation of signatures (see HetCATS/CASL/Sign.hs)
2. genertion of axioms (injectivity, overloading ...)
details: see paper in Theoretical Computer Science, p. 407
Angucken:
FORMULA in CASL/AS_Basic.hs
Sign in CASL/Sign.hs
************************************************
Heng (Klaus)
************************************************
Darstellung des Logik-Graphen
dazu importieren:
-- f�r Graph-Darstellung
import DaVinciGraph
import GraphDisp
import GraphConfigure
-- f�r Erzeugen von Fenstern
import TextDisplay
import Configuration
import qualified HTk
plus unten genannte Module
Aufgabe: den Logik-Graph aus folgendem Modul:
logicGraph aus Comorphisms/LogicGraph.hs, Typ in Logic/Grothendieck.hs
aufbereiten f�r Anzeige, Vorbild ist in uni/graphs/test/GraphDispTest.hs
Aufbau von nodeTypeParams
-------------------------
Knoten (bzw. Kanten) habe Werte, in diesem Fall: AnyLogic (bzw. AnyComorphism)
nur 1 Knotentyp, rund, gr�n
Men�funktionen AnyLogic -> IO ()
ValueTitle AnyLogic -> String (= language_name aus Logic/Logic.hs)
$$$ ist Funktion zum Zusammenf�gen von Knotentyp-Parametern
Knotenmen�:
unter Men�eintrag "Info" anzeigen: Werte aus Logic/Logic.hs
erstmal AnyLogic-Wert auspacken, z.B. mit
case l of
Logic lid ->
Logik-Namen ausgbene (mit language_name lid)
Test auf Just _, dann String ausgeben
parse_basic_spec lid "Parser for basic specifications"
parse_symb_items lid "Parser for symbol lists"
parse_symb_map_items lid "Parser for symbol maps"
parse_sentence lid "Parser for sentences"
basic_analysis lid "Analysis of basic specifications"
data_logic lid "is a process logic"
Ausgaben:
map (sublogic_names lid) (all_sublogics lid)
-- sp�ter besser als eigener Men�punkt ==> eigener Graph
map prover_name (provers lid) -- aus Logic/Provers.hs
map cons_checker_name (cons_checkers lid)
Anzeigen dieser Ausgabe mit:
createTextDisplay title str [size(100,50)]
str ist der anzuzeigende Inhalt
Aufbau von arcTypeParams
-------------------------
Kantentypen:
- einen "normal" f�r "normale" Comorphismen, schwarz
- einen "inclusion" f�r Inclusions, blau
Kantenmen�: Anzeige von sourceSublogic und targetSublogic (siehe Logic/Comorphisms.hs)
mittels language_name
Aufbau des Graphen selbst
------------------------
GraphDisp.newGraph daVinciSort -- aus uni/graphs/GraphDisp.hs
-- mit leerem globalen Men�
newNode --
newArc
Anzeige des Graphen
-------------------
redraw
-------------------------------------------------------------------
LaTeX pretty printer
von Christian:
a) analysierte Formeln und Terme optimal/k�rzer ausgeben:
shorten :: Sign -> {TERM, FORMULA} -> {TERM, FORMULA}
In Abh�ngigkeit von Sign werden z.B. nicht-�berladene Funktionen
unqualifiziert ausgeben bzw. zwecks Eindeutigkeit wird (minimal) nur
mit dem Ergebnistyp qualifiziert.
((a: Nat) + (b: Nat)): Nat
b) 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.
************************************************
Christian
************************************************
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
checking class constraints of terms
pattern analysis for program equations
- for simple types (currently type synonyms)
symbol representation
symbol map analysis (hiding sub/supertypes)
Weak amalgamation analysis?
Instantiate Transformation Application system for HasCASL?
Automatic generation of Haskell (for a HasCASL subset)
Proofs in HasCASL
Case study
************************************************
Klaus
************************************************
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
************************************************
Maciek
************************************************
Static analysis of architectural specs
************************************************
Till
************************************************
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
avoid cyclic comorphisms
Missing points for heterogeneous WADT 04 example:
- coding to Isabelle: translate sort gen constraints
- extended globDecomp rule: existing local Thm links
(e.g. generated by %implied) should lead to fewer new local
links ("local composition" rule)
- Improve adapation to Isabelle's lexis
Isabelle: (ask Christoph)
free datatypes
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
Generalie 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
Coding of subsorts as unary predicates (for ontologies)
Translation between Achim's ontology data structure and CASL (in Hets)
- 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
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
************************************************
Emacs mode
Hets Web interface (cf. CATS/web_interface2.sml)
CCC ?
Packaging of installation
integrate QuickCheck
XML interface
GUI (vgl. VSE)
increase performance
++++++++++++++++++++++++++++++++++++++++++++++++
Remaining things
++++++++++++++++++++++++++++++++++++++++++++++++
Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
Coq, PTT in Maude
Proof general interface (1 day)
Test Maya 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