304N/AModels (discuss with Razvan!)
304N/A=============================
1356N/AIntegrate (presentations of) models into Hets
304N/A For each logic, design a description language for (relative) models
1356N/A this should also capture solutions of constraints and
304N/A answer substitutions in logic programming
919N/ASignatures versus theories
919N/A==========================
919N/Aproof theoretic comorphisms (
e.g. CASL->HasCASL, sort gen axs are
919N/A only proof theoretically translatable)
919N/Ain favour of comorphisms: subinstitution Eq= -> FOL= is not a morphism
919N/ATCS-paper: based on WADT 2002 paper, all 8 forms of (co)-morphisms
919N/A (extend HetCASL summary with that)
919N/AShow that any morphism whose image is logically characterizable is
304N/Aalready weakly inducible
304N/AThe mixed Grothendieck institution is isomorphic to the
304N/Acomorphism Grothendieck institution, if every morphism is induced
493N/Aby some comorphism and the corresponding 2-cells are there
977N/ASome result of "full abstractness" here?
I.e. given
970N/Aa (2-)diagram of certain shape, everything
970N/Awhich is different at the signature morphism level in
1356N/Athe Grothendieck institution will be different at the
1356N/Acorridor level for suitably chosen institutions,
1068N/AMixed case: use 2-cells between arbitrary paths, based on
304N/A"relations". Does my Fossacs-Result generalize to the
1068N/ARelation between Grothendieck construction and (co)limits + het. borrwoing
911N/A Do the same "universal pushouts" appear?
304N/ALocalized signatures via logics with symbol functor
304N/A that is faithful and injective on objects
1124N/AAMAST 96, Fiadeiro: about parallel composition
970N/AReals in CASL (via CoCASL) (Lutz?)
970N/A - refinements between these two
970N/A - both are refinement of first-order reals
304N/ABIT-Bsp. in CASL-LTL und HasCASL
(with morphism keeping the labeled transistion system)
Bsp. von Franzosen (LeGall...)
COL / observational logic
-------------------------
specify in COL, then project to CASL (= close desgin),
add new sorts, return to COL
Gabbay: 19h inf 700 ad/356-1
a phi 551 a/387-3 a phi 551 a/387-2
tb 3925-1 a mat 038 e/593-1 a mat 038 e/593-2
-
J.J. Meyer, R. Wieringa: Book about Deontic logic, 1993
- Fiadeiro, Maibaum: Sometimes tomorrow is sometime:
Action refinement in a temporal logic of objects, LNAI 827
Modal: how to express K, S4, S5 etc.? (cf. HasCASL: extensionality etc.)
=> sublogics defined by theories (comma signature category)
Knowledge representation 89:
K + agreement of modalities (R down S = {x | forall y R(x,y)=>S(x,y)}
both decidable, but not their combination
OWL-full, 2nd-order DL = non-well-founded sets
(see Montanari, van Benthem: K + world reachability = non WF elementhood
FOL + modal logic: interface via propositions
FOL + modal logic: interface via making worlds explicit
IndexedModal --> FOL : make worlds explicit, indices -> data values
IndexedModal --> Modal: forget indices (faithful without model expansion?)
can be used for re-using modal provers
Beware: for IPM-->PM borrowing we need proof theoretic conservativity
- Maibaum: Interconnecting formalisms: supporting
modularity, reuse and incrementality. 3rd FSE, ACM press 1995
- Mainbaum: A mathematical toolbox for the software architect. 11th IWSSD
(International Workshop on SW spec + design), IEEE press, 1995
Heterogeneous refinements
--> possibility to mix specification and implementation
(only parts are implemented)
CSP: see paper by Kwietkowska about CSP + fairness
imperative, functional, non deterministic, temporal and real-time aspects
ask Gunnar Schr�ter! (viewpoint specifications, WADT 2004)
timed automata (Michel) + some modal logic?
(just to have something very different from CASL)
needed: non-artifical example involving differen kinds of arrows
+ which show that universal logic is too complex
(only a universal "coding" logic would make sense!)
Consistency / conservativity
============================
implement check for positiveness of theories
is conservative if sp |- exists f:i . phi
Consistency checker: locally + model expansion for the comorphisms
Razvan can show it for the Grothendieck institution?!
Mail Razvan, send him papers, invite him!
CR needed for intermediate lemmas (though not necessarily for completeness)
-> check Marriage example
Lemma speculation cannot be automatized and is more than CR (Dieter)
Mary Sheeran, Chalmers, G�teborg:
verfication of Haskell programs that construct hardware circuits
Dillian Girow, Stockholm:
�-calculus for concurrent aspects of Erlang
CASL methodology, 3rd volume, ccc tools (Till, Lutz, Cxl)
Modal-CASL als Anforderungssprache
div. Prozessalgebren (wir stellen den allg. Rahmen)
Management of change (bkb, Hutter, Till, cxl, Achim, Kohlhase?)
Ontologien: neuer SFB-Antrag (Fr�hjahr 2005)
Abstract robotics (cxl, paolo)
AWE II / General FM (cxl, bkb)
Datatype with abstract formatting syntax
different "style sheets" for different output formats (ASCII, HTML, LaTeX)
Priorities of line breaks?
How to handle text width in LaTeX?