todo revision 963fd654abe69959032e5747732ec1c2f8fc9b41
Plan and priority list for CoFI tool activities
************************************************
Immanuel
************************************************
Suchfunktion f�r einen Knoten im DG:
welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
erstmal auf eine Logik (z.B. CASL) beschr�nken
- Funktion f�r Morphismus-Suche zwischen Theorien
- evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
- Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
BasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
Konfidenzgrade von Beweisen?
von Till/Jorina (jfgerken@tzi.de) zu erledigen:
Repr�sentation �ndern:
Beweisobjekte an DGs, nicht an Regeln
F�r Theoreme in Theorien an Beweisobjekte
BasicProof mit Liste von Beweisobjekten
Isabelles Beweisobjekte einbinden
Definitionen auszeichnen
************************************************
Florian (Till)
************************************************
HetCATS, uni und CASL-lib auschecken
abstrakte Syntax f�r ConstraintCASL (s. CASL-lib/ConstraintCASL/)
Parser f�r ConstraintCASL
Testen mit
Freiburger Constraint-Solver angucken
Bremer Constraint-Solver angucken
************************************************
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"
check' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
check' [] = ([([],[])],emptyUniqSet)
-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
check' [EqnInfo n ctx ps (MatchResult CanFail _)]
| all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
check' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
| all_vars ps = (pats, addOneToUniqSet indexs n)
where
(pats,indexs) = check' rs
-- falls ein Konstruktor dabei ist: split_by_constructor
-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
check' qs@((EqnInfo n ctx ps result):_)
| all_vars ps = ([], unitUniqSet n)
| constructors = split_by_constructor qs
| only_vars = first_column_only_vars qs
| otherwise = panic "Check.check': Not implemented :-("
where
-- Note: RecPats will have been simplified to ConPats
-- at this stage.
constructors = or (map is_con qs)
only_vars = and (map is_var qs)
subsort definitions: are conservative if formula is satisfiable
(generate proof obligation)
************************************************
Heng (Klaus)
************************************************
OWL-DL logic
OWL-DL (<)-> CASL-DL
emacs mode:
highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
some operation symbols
show hets output immediately
C-c C-g for hets -g
when hets terminates abnormally (e.g. with a fail), emacs loops
C-n jumps to the next error, but the message windows is not always scrolled
in such a way that the error is at the top (for long error lists)
Version for XEamcs?
should work with parser error messages as well (adapt these?)
************************************************
Hilfskraft 1
************************************************
Modal-CASL <-> CASL-DL
see Chapter 4 of "The Description Logic Handbook"
and ask Klaus for a print out of it
************************************************
Hilfskraft 2
************************************************
Uni-Refactoring,
make modules hierarchical, change scoped type variables for ghc-6.5
(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),
use HaXml as a cabalized library, provide uni as (one?) cabal
package(s), uni used to work under windows as well, watch the
i.e. FilePath, Process discussions (libraries@haskell.org)
possibly switch to a subversion repository, talk to Achim
(amahnke@tzi.de)
************************************************
Ken (Till)
************************************************
development graph calculus
(see Sect. IV:4.4 of the CASL Reference Manual)
look at Static/DevGraph.hs
implement simplified rule Theorem-Hide-Shift
try out examples
conservativity calculus
weakly amalgamable cocones
************************************************
Zheng (Till)
************************************************
look at Static/DevGraph.hs
look at translation to OMDoc
change management via translation to OMDoc
einfaches Merge von lokalen Beweisen eines abgespeichteren DG
in aktuellen DG
************************************************
Hilfskraft 4
************************************************
port hets to windows.
If hets should become successful then requests for support under
windows will surely follow.
Ghc, uni and uDrawGraph should work under windows. Only Isabelle does
not exist for windows, but SPASS does. Probably only a few path
computations need to be adapted (made modular) within hets. Also
position computations (of Parsec) should be checked under windows.
************************************************
Hilfskraft 5
************************************************
refactor pretty printing
eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex
und andere Formate besser zu unterst�tzen und einheitlichen PP code
(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)
Datentypen (particularly for HasCASL data types) zu bekommen.
LaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)
************************************************
remaining stuff
************************************************
set up a ticket and tracking systems (for bugs and features) instead
of this messy todo list
--> sourceforge???
refactoring of dgraphs: add unique tags (but no table)
display library graph
unify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs (make
it really abstract), possibly contact amahnke@tzi.de regarding
Taxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
set up default simplifier
set up default tactics using axioms
(see DOLCE sample files)
improve efficiency (e.g. of UserManual/Sbcs.casl), using profiling
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)
- Fail: No match in record selector Static.DevGraph.dgn_sign
for local subsume in RelationsAndOrders
************************************************
Daniel
************************************************
generate infrastructure for circular coinduction
CCS example: commutativity of || by coinduction
************************************************
Christian
************************************************
collect the patches for programatica (or create a package)
- conv (SN i p) = PN i (S p)
+ conv (SN i p) = PN i (Sn (show i) p)
fixes translation error of Pair
simplification of HasCASL sentences (omit types)
Logic COL is a ruin (with wrongly qualified module names)
logic coding from the comand line with printing of results
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
************************************************
Rainer (Klaus)
************************************************
Connecting Hets with MathServ
Either use
pros: * relies not on external tool
* light weight call
cons: * code is not well maintained
* a lot of the deserialization of the answer must be done
in Haskell
- call a java program included in MathServ distrib
pros: * works imediately
* deserilisation is mostly done in java
cons: * use of external tool
Use modified dfg2tptp to translate SPASS theories into TPTP problems
(ask Klaus for sources)
Add possibility to choose a prover out of a list of available provers
(similar to "More fine grained..." and behind more fine grained)
Adapt Comorphisms.KnownProvers to select a certain prover at the end of a
comorphism automatically
Adapt existing SPASS GUI to cover call of the MathServ broker
by - transforming the grid layout packer into the packer
used in GUI.ProofManagement (easier to maintain and to extend)
- abstraction of certain parts of the GUI into helper functions
forms a new generic Prover-GUI toolkit
- on top of this GUI toolkit
Write a GUI based on the generic Prover-GUI
to call MathServ's Vampire service directly
with additional parameters
************************************************
Klaus
************************************************
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
allgemeine Hets-GUI
f�r Anzeige von (un)bewiesenen Goals, ... done
bewiesene Goals als Axioms mit ausgeben ... was ist das ???
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
************************************************
Regulate concurrent proving
.dg files: store only current library; import .dg files for other libraries
Markus' Bsp:
Isabelle: use meta-quantifiers
local subsumption ?
better syntax (Tina)
check for proved theorems
AbstractGraphView: switch to Result monad
unite or rename consCheck and cons_checkers
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
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
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
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