todo revision ead55e5013b301de3b72a254a9fb347ae04ba0a4
b7ff1e47da4653d2ff1ec7b489e6067fed29d8c5Lennart PoetteringPlan and priority list for CoFI tool activities
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering************************************************
b7ff1e47da4653d2ff1ec7b489e6067fed29d8c5Lennart Poettering************************************************
b7ff1e47da4653d2ff1ec7b489e6067fed29d8c5Lennart PoetteringSuchfunktion f�r einen Knoten im DG:
c32e0c40f7e706e3ebcd101187d5ced96f083491Lennart Poettering welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
c32e0c40f7e706e3ebcd101187d5ced96f083491Lennart Poettering erstmal auf eine Logik (z.B. CASL) beschr�nken
7d640cdf66a7c032c871ccfe0ee4ad56f7e3869bLennart Poettering - Funktion f�r Morphismus-Suche zwischen Theorien
62170515a17d0771aa38c8e7711a7a60c8d14d2fLennart Poettering - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
c904f64d84db8c4eebedf210ba10893f19ba05edLennart Poettering - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
c904f64d84db8c4eebedf210ba10893f19ba05edLennart PoetteringBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
7d640cdf66a7c032c871ccfe0ee4ad56f7e3869bLennart PoetteringKonfidenzgrade von Beweisen?
34df5a34e1d0ac4bba453fb5f52f18a2f5f260f9Lennart Poetteringvon Till/HiWi zu erledigen:
34df5a34e1d0ac4bba453fb5f52f18a2f5f260f9Lennart PoetteringRepr�sentation �ndern:
7d640cdf66a7c032c871ccfe0ee4ad56f7e3869bLennart Poettering Beweisobjekte an DGs, nicht an Regeln -- done
34df5a34e1d0ac4bba453fb5f52f18a2f5f260f9Lennart Poettering F�r Theoreme in Theorien an Beweisobjekte -- done
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering Definitionen auszeichnen -- done
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering F�r alles siehe G_theory, ThSens und SenStatus.
a49408ec64063023524b964064d393c1fce36e4aKay Sievers Isabelles Beweisobjekte einbinden
e677657e8dddb33d1f1e32eda0ebc126e08a538dLennart Poettering************************************************
e677657e8dddb33d1f1e32eda0ebc126e08a538dLennart Poettering************************************************
e677657e8dddb33d1f1e32eda0ebc126e08a538dLennart PoetteringIntegration with PGIP
fc7ac59412742e2ef0638e86070c33afd579848eLennart Poettering Hets needs to be equipped with a command-line interface that reads in
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering specification libraries and proof commands
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering Proof commands are special annotations in the libraries
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering All menu commands of the development graph interface (GUI/...) should become (proof) commands
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering when stepping through the specs, dg calculus generates proof obligations
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering (for the current dg node only),
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering which then can be discharged by Isabelle, SPASS etc.
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering That is, the proof commands always occur at the position in the text
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering that generates the dg node?!? or should they occur after each specification?
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering needs incremental parsing and static analysis for Hets libraries
2791a8f8dc8764a9247cdba3562bd4c04010f144Lennart Poettering easy: parse and analyse one specification at a time, and then process it with proof commands
a49408ec64063023524b964064d393c1fce36e4aKay Sievers more challenging: incrementally parse and analyse also individual specifications
260abb780a135e4cae8c10715c7e85675efc345aLennart Poettering************************************************
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers************************************************
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay SieversModal-CASL <-> CASL-DL
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers see Chapter 4 of "The Description Logic Handbook"
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers and ask Klaus for a print out of it
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sieversimprove Modal-CASL
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers possibly also modal logic in CoCASL
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers**************** task A ************************
a49408ec64063023524b964064d393c1fce36e4aKay SieversProofs with Isabelle and SPASS
a49408ec64063023524b964064d393c1fce36e4aKay SieversCASL basic datatypes
a49408ec64063023524b964064d393c1fce36e4aKay SieversHasCASL examples
a49408ec64063023524b964064d393c1fce36e4aKay Sievers- improve simplifier for partiality in Isabelle coding
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering program interaction between solver, subgoaler and simplifier in such a way
099663ff8c117303af369a4d412dafed0c5614c2Lennart Poettering that proofs of definedness conditions are postponed
81253930180bac6b6fb372a9c7bea724bd795c86Lennart Poettering************************************************
430c18ed7f576fd9041b0a02e7c4210bdd020a25Lennart Poettering************************************************
1a6f4df6c9437ed631080b7e006f666326063d36Lennart PoetteringModelchecker f�r algebraische Eigenschaften
1a6f4df6c9437ed631080b7e006f666326063d36Lennart Poettering neue Hets-Option daf�r (Christian Maeder fragen)
a49408ec64063023524b964064d393c1fce36e4aKay Sievers hets -n NonAssocRelationAlgebra --model datei.lisp Calculi/Algebra/RelationAlgebra.casl
3db48a7850d9ceb8e81ec4ad410520c05c008763Lennart Poettering Datenstruktur zerlegen, siehe
3db48a7850d9ceb8e81ec4ad410520c05c008763Lennart Poettering http://www.informatik.uni-bremen.de/agbkb/forschung/formal_methods/CoFI/hets/debugging_e.htm
a49408ec64063023524b964064d393c1fce36e4aKay Sievers Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:
3db48a7850d9ceb8e81ec4ad410520c05c008763Lennart Poettering Allquantoren --> all, Existenzquantor --> any
2e0d98fa87a4e399763c8235abe56be4f8ac7fb8Lennart Poettering CASL-Junktoren --> Haskell-Junktoren
2e0d98fa87a4e399763c8235abe56be4f8ac7fb8Lennart Poettering Terme rekursiv auswerten, Operationen aus der Table nehmen
b5c6cf87342bedeb67fbbc4f3f512af1603a461cLennart PoetteringAufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken
b5c6cf87342bedeb67fbbc4f3f512af1603a461cLennart Poettering - ggf. Server nutzen
3185a36b05d53757a412f847d8c510978b9b00f0Lennart Poettering - Vorverarbeitung f�r Solver (z.B. Duplikate raus)
7d9e57d2cf671f7173324942e0eb9de0d030c505Kay Sievers - Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)
b8bb3e8f346468e61dcc7a6aba5e7ac9c623d964Lennart PoetteringApplikation1 ---
b8bb3e8f346468e61dcc7a6aba5e7ac9c623d964Lennart Poettering | | -- Freibuger Solver
f959c5e63a9080cbff42ac4160154f8a6b508e7aLennart Poettering XML --- |---- Franz�sischer Solver
f959c5e63a9080cbff42ac4160154f8a6b508e7aLennart Poettering | |-- Hets -- Bremer Solver
7f6d613516020bf390d8de25bbbb2551ea8dade0Lennart PoetteringApplikation2 ----- |
c32e0c40f7e706e3ebcd101187d5ced96f083491Lennart Poettering ConstraintCASL
47ae6e6760301ecae086e984b0b23f2db9663b28Lennart Poettering Semantische Modelle/Korrektheit (CASL, HAsCASL)