todo revision 7b29b4b1e019e72dc7aff35c2a98eb6bad67e364
Plan and priority list for CoFI tool activities
************************************************
Immanuel
************************************************
user normann
************************************************
Razvan (Till)
************************************************
user rpascanu
************************************************
Anton (Till)
************************************************
user luecke
**************** task A ************************
user maeder
************************************************
Florian (Till)
************************************************
user fmossa
************************************************
Hendrik (Till)
************************************************
user hiben
Anzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen
************************************************
Mingyi (Till)
************************************************
user xinga
************************************************
Heng (Klaus)
************************************************
user jiang
************************************************
Ken (Till)
************************************************
user ken
************************************************
further task 1
************************************************
************************************************
further task 2
************************************************
************************************************
further task 3
************************************************
************************************************
further task 4
************************************************
done
************************************************
further task 5
************************************************
************************************************
remaining stuff
************************************************
************************************************
Daniel
************************************************
generate infrastructure for circular coinduction
CCS example: commutativity of || by coinduction
************************************************
Christian
************************************************
************************************************
Rainer (Klaus)
************************************************
for ProofManagement-GUI
mark imported theorems for selection
extend Logic.Prover SenStatus with wasTheorem
somewhere in computeTheory implement setting of wasTheorem
if wasTheorem not appears with right status in ProofManagementGUI
add wasTheorem to Common.Result.Named, as well
and adapt conversion functions of SenStatus to Named and vice
versa in Logic.Prover
Mark old theorems in "Axioms to include" Listbox with prefixed
"(Th)"
add button "Deselect former Theorems"
test all this with CASL-lib/Calculi/Space/RCCVerification.het
all nodes without incoming heterogeneous edges are provable with
SPASS
************************************************
Martin
************************************************
user mkhl
************************************************
Klaus
************************************************
for ProofManagement-GUI
provide structured (based on spec-names) selection/deselection facility
of axioms and theorems
trace if liniarity of sentences along development is given
Consistency checker interface
via global interface, accessible from global and node menus
use falseSentence from Logic.Logic (property: holds in no model)
proved -> inconsistent
disproved -> consistent (assuming completeness)
batch mode for automatic provers such as SPASS
(use automatic flag for provers)
batch interface for Isabelle
each goal is proved separatedly, with a time limit enforced
by killing the process
the tactic is
"using Ax1 ... Axn by auto"
where Ax1 ... Axn is the list of all axioms.
"auto" could be replaced with "best", "blast" etc. (user selection)
Ignore axiom selection for interactive provers
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)
last two ... partially done
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
************************************************
Till
************************************************
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
use graph grammars to model rules? transformation units?
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
BinInt.casl: revealing in Int1 does not work correctly
************************************************
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