todo revision dce941659526313d3e4ec7021ab76ad97995a4c3
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski************************************************
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiSuchfunktion f�r einen Knoten im DG:
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski erstmal auf eine Logik (z.B. CASL) beschr�nken
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski - Funktion f�r Morphismus-Suche zwischen Theorien
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiKonfidenzgrade von Beweisen?
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowskivon Till/HiWi zu erledigen:
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till MossakowskiRepr�sentation �ndern:
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski Beweisobjekte an DGs, nicht an Regeln -- done
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski F�r Theoreme in Theorien an Beweisobjekte -- done
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski Definitionen auszeichnen -- done
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski F�r alles siehe G_theory, ThSens und SenStatus.
0ed8d8af48a2da78b0dcd8f0728033feef767d56Till Mossakowski Isabelles Beweisobjekte einbinden
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskiIntegration with PGIP
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski Hets needs to be equipped with a command-line interface that reads in
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski specification libraries and proof commands
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski Proof commands are special annotations in the libraries
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski All menu commands of the development graph interface (GUI/...) should become (proof) commands
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski when stepping through the specs, dg calculus generates proof obligations
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski (for the current dg node only),
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski which then can be discharged by Isabelle, SPASS etc.
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski That is, the proof commands always occur at the position in the text
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski that generates the dg node?!? or should they occur after each specification?
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski needs incremental parsing and static analysis for Hets libraries
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski easy: parse and analyse one specification at a time, and then process it with proof commands
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski more challenging: incrementally parse and analyse also individual specifications
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski************************************************
0e3db835d379ceb594b0daa25a0590abb755a1acTill MossakowskiModal-CASL <-> CASL-DL
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski see Chapter 4 of "The Description Logic Handbook"
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski and ask Klaus for a print out of it
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowskiimprove Modal-CASL
0e3db835d379ceb594b0daa25a0590abb755a1acTill Mossakowski possibly also modal logic in CoCASL
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till Mossakowski**************** task A ************************
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till MossakowskiProofs with Isabelle and SPASS
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till MossakowskiCASL basic datatypes
e2143dde7e5adcc35f1587e94c9279d8cbe3cbd5Till MossakowskiHasCASL examples
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski- improve simplifier for partiality in Isabelle coding
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski program interaction between solver, subgoaler and simplifier in such a way
4a573a1ca4f8556b77e3467e6c2b261ba03e3036Till Mossakowski that proofs of definedness conditions are postponed
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski************************************************
566b6a416bde2bc90d3aece2d992127303fb5d75Till MossakowskiFlorian (Till)
db373255bd95ce4de47dde876c3a3bfc49c22a97Till Mossakowski************************************************
2b60e1b81de56782be899de982c0908696f3530dTill MossakowskiModelchecker f�r algebraische Eigenschaften
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski neue Hets-Option in Driver/WriteFn.hs implementieren
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski hets -n NonAssocRelationAlgebra
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski --modelSparQ=datei.lisp Calculi/Algebra/RelationAlgebra.casl
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski siehe auch CASL.CompositionTable.ComputeTable
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski modelCheck :: SIMPLE_ID -> (Sign f e, [Named (FORMULA f)])
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski -> Result Bool
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski Warnung mit Gegenbspen ausgeben, wenn eine Eigenschaft nicht gilt
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski (abbrechen nach 10 Gegenbspen)
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski Warnungen erzeugen mit Funktion warning aus Common.Result
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski Range aus den CASL-FORMULAs extrahieren
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski Result ist eine Monade, ggf. mit do-Notation arbeiten
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski Allquantoren --> all, Existenzquantor --> any
3c8c05dc3358d217513d8e0e8e32ccd3e4947c05Florian Mossakowski CASL-Junktoren --> Haskell-Junktoren
db808015f92d8fbee41ddedd34a78f6d5ac70cfcTill Mossakowski Terme rekursiv auswerten, Operationen aus der Table nehmen
677a642991937d4bcf24dd30ef54328a9197fc86Till MossakowskiAufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski - ggf. Server nutzen
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski - Vorverarbeitung f�r Solver (z.B. Duplikate raus)
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski - Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiApplikation1 ---
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowski | | -- Freibuger Solver
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowski XML --- |---- Franz�sischer Solver
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski | |-- Hets -- Bremer Solver
82e53ddd36b012552278c1d02b7ea2e786fc375aTill MossakowskiApplikation2 ----- |
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski ConstraintCASL
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski Semantische Modelle/Korrektheit (CASL, HAsCASL)
82e53ddd36b012552278c1d02b7ea2e786fc375aTill MossakowskiXML-Einlesen in Haskell:
82e53ddd36b012552278c1d02b7ea2e786fc375aTill MossakowskiHXT (siehe OMDoc.XmlHandling): kann Namespaces
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski(HaXML: kann Haskell-Datenypen in DTDs umwandeln)
82e53ddd36b012552278c1d02b7ea2e786fc375aTill MossakowskiOutline der Diplomarbeit
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski Qualitative Constraint-Kalk�le (siehe Thomas)
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski CASL-Formeln nur ganz kurz
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski ConstraintCASL
82e53ddd36b012552278c1d02b7ea2e786fc375aTill Mossakowski Signaturen, Signaturmorphismen (aus CASL)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski Modelle (aus CASL)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Erf�lltheit von Formeln
38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski optional: Erf�lltheitsbedingung
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski M |= sigma(phi) <=> M|_sigma |= phi
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski f�r Signaturmorphismus sigma:Sigma_1->Sigma_2
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski M \in Mod(Sigma_2), phi\in Sen(Sigma_1)
ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski Formalisierung von Kalk�len in ConstraintCASL
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Constraint-Solver (auch in ihren Eigenheiten)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski �bersetzungen zwischen den verschieden Formaten
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski praktischer Vergleich
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski�bersetzungen bis 30.Juni
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski ConstraintCASL -> Bremer Solver
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Bremer Solver -> ConstraintCASL
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Das kann das als Option in Hets eingebunden werden (Christian Maeder)
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiFreiburger Constraint-Solver angucken im Juli
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski�bersetzungen bis 31. Juli
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski ConstraintCASL -> Freibuger Solver/XML-Format
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Freibuger Solver/XML-Format -> ConstraintCASL
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiHendrik (Till)
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski************************************************
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiOmDoc-Ausgabe konform mit RelaxNG?
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiOmDoc-Ausgabe Immanual zeigen
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till MossakowskiTypen von gebundenen Variablen weglassen
19de92371ac1cc5d71e4ca0a1f4aaf5dba9b1ad8Till MossakowskiOMDoc-Datentyp einf�hren
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Hets <-> Datenstruktur <-> OMDoc
cc5d60d23c401752ba8a931756546a6c86519d9dTill Mossakowski Namensgenerierung/rekonstruktion auf der Seite Hets <-> Datenstruktur
cc5d60d23c401752ba8a931756546a6c86519d9dTill MossakowskiUrsprung von Symbolen bei Hets -> OMDoc: irgendeins nehmen
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiAusgabe als DAG, mittels OMR oder ref
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski Sharing-Algorithmus verwenden
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiConstraints mit Indizes: ggf. higher-order-Axiom erzeugen (Till fragen)
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiAnzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiOMDoc-Bug melden f�r
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski free type Vehicle ::= sort Boat | sort Car
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski wobei Boat und Car aus anderen Files kommen
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski S. 156: Satz einfach streichen
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskisortdef legt bereits ein Symbol an
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskiwerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski sie als erstes eingef�hrt wurden?
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski checken f�r Library-Importe
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiOMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill MossakowskiHiding: unterschiedlich in OMDoc und Hets
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowskiein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski Signaturmorphismus
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski wird �bersetzt in einen OMDoc-Theoriemorphismus
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski mit leerer/identischer Abbildung, bei dem die Symbole aus
5f96ebe3a06b74faaf2860af09b722d006a82cbcTill Mossakowski Sigma_2 \ Sigma_1 versteckt werden
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowski Wenn der Signaturmorphismus keine Inklusion ist, ist keine
a1bb9f8f9143aa2d84dfab69ed988d94f7e3b196Till Mossakowski �bersetzung m�glich -> Fehler
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (also leere bzw. identische Abbildung) wird �bersetzt
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich der dann die Umbenennung macht, erzeugt werden
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till MossakowskiLogiken: �ber verschiedene OMDoc-Theorien mit URI
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski************************************************
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski************************************************
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski- CASL-Logik: "Relating CASL with other specification languages", S.401-408
87268d03b727bc9091716644fcf4048379accf02Till Mossakowski- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz
1604c7123ebd603b2ca3eb6d2bd325cbdb23ee99Till Mossakowski siehe CASL reference manual (suche nach conservative)
aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowski- warum sind konservative Erweiterungen wichtig?
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski - um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski werden k�nnen
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski - f�r Refinement-Beweise
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski definitional oder monomorph sind
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski - Beschreibung des Algorithmus in Pseudocode
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till Mossakowski - Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski als konservativ erkennt, muss f�r jedes Modell der kleineren
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski Spezifikation eine Modellerweiterung zur gr��eren Spezifikation
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski gefunden werden. Z.B. im Falle von free types kann dies eine
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski Termalgebra-Konstruktion sein.
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski SP1 -- \sigma --> SP2
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski SP2-Modell M2 mit M2|_\sigma=M1.
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskiport CCC to Haskell
1a58edf41188c6928c65f0b071f4357450e23c1eTill MossakowskiFunktionen imageOfMorphism und inhabited
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski mit "cvs add SigFuns.hs" einchecken
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski"free datatypes and recursive equations are consistent"
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till MossakowskicheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till MossakowskiJust True => Yes, is consistent
4b03f31b4401e4e9f36e92c461f82acb8e67b5c3Till MossakowskiJust False => No, is inconsistent
2b9290308115cc5bda1684b07348f25e2b39ed50Till MossakowskiNothing => don't know
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowskicall the symbols in the image of the signature morphism "new"
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski- each new sort must be a free type,
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski i.e. it must occur in a sort generation constraint that is marked as free
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski (Sort_gen_ax constrs True)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski if not, output "don't know"
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski and there must be one term of that sort (inhabited)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski if not, output "no"
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski- group the axioms according to their leading operation/predicate symbol,
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski i.e. the f resp. the p in
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski Implication Application Strong_equation
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski Implication Predication Equivalence
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski if there are axioms not being of this form, output "don't know"
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskicheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskicheck' [] = ([([],[])],emptyUniqSet)
180139f7c23c592aa6d4fe82ea5d15832ed25a84Till Mossakowski-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskicheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowskicheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski | all_vars ps = (pats, addOneToUniqSet indexs n)
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski (pats,indexs) = check' rs
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski-- falls ein Konstruktor dabei ist: split_by_constructor
677a642991937d4bcf24dd30ef54328a9197fc86Till Mossakowski-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowskicheck' qs@((EqnInfo n ctx ps result):_)
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski | all_vars ps = ([], unitUniqSet n)
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski | constructors = split_by_constructor qs
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski | only_vars = first_column_only_vars qs
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder | otherwise = panic "Check.check': Not implemented :-("
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski -- Note: RecPats will have been simplified to ConPats
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski -- at this stage.
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski constructors = or (map is_con qs)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski only_vars = and (map is_var qs)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskisubsort definitions: are conservative if formula is satisfiable
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder (generate proof obligation)
180139f7c23c592aa6d4fe82ea5d15832ed25a84Till Mossakowski************************************************
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder************************************************
420440d8d1a274241aae513044f0f9a0bc691985Christian MaederOWL-DL (<)-> CASL-DL
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
420440d8d1a274241aae513044f0f9a0bc691985Christian Maeder some operation symbols
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski show hets output immediately
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski C-c C-g for hets -g
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski when hets terminates abnormally (e.g. with a fail), emacs loops
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski C-n jumps to the next error, but the message windows is not always scrolled
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder in such a way that the error is at the top (for long error lists)
b303a3717d229b102bca29e58d9e38c2f91fd233Christian Maeder should work with parser error messages as well (adapt these?)
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder easier setup of emacs mode
6c82551a9e6a38aa7c774db95ee957379f03df75Christian Maeder by just loading one file
f3a84cc409ed345569be6673d05072dcb4291ebeTill Mossakowski integration into installer
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski checking for emacs and offer adaption of ~/.emacs
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski Version for XEamcs?
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski************************************************
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maeder************************************************
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowskilook at command line interface (just call hets)
9a9a05b15ab416d7d84fdb9115023e9136666304Till Mossakowskiimplement simplified rule Theorem-Hide-Shift
963fd654abe69959032e5747732ec1c2f8fc9b41Till MossakowskiIf there is an open global theorem link sigma:N1->N2 and
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowskia hiding definition link theta:N3->N2 (i.e. the signature
963fd654abe69959032e5747732ec1c2f8fc9b41Till Mossakowskimorphism theta is from Sig(N2) to Sig(N3)), then prove
0ef6fed7a5d52b1f791926bd8a432723ffd28767Christian Maederthis theorem link by inserting a new global theorem link
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowskitheta o sigma : N1->N3.
0317c2ef1c222f6664e9b494d10c68ee2114475eTill Mossakowski test file: see CASL-lib/test_TheoremHideShift.casl
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski (when doing Automatic, HideTheoremShift, Automatic, and then
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowski local proof in Target')
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiissue warning whne displaing theories (or performing proofs) of
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskinodes with ingoing hiding links.
2b9290308115cc5bda1684b07348f25e2b39ed50Till Mossakowskiimprove dependency tracking for development graph proofs
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski display proved theorem links that depend on pending other proofs in yellow
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskidisplay normal form of nodes with ingoing hiding links
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskitry out examples
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskiconservativity calculus
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowskipushouts http://en.wikipedia.org/wiki/Pushout_%28category_theory%29
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiweakly amalgamable cocones
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskidevelopment graph calculus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(see Sect. IV:4.4 of the CASL Reference Manual)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskilook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowskitest command line interface (just call hets)
198093ec9afd8b459087dc30c94347bb7eeaa282Till Mossakowskitest development graph GUI:
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski global decomposition
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder menu edit - unnamed nodes - hide/show nodes,
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder node menu: show just subtree / undo
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder interaction with edit - proofs - automatic?
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder use update of uDrawGraph-nodes,edges instead of erasing and adding nodes
a50b65fa19134fd10a653b8f8160b830a4d489d7Christian Maeder for attribute changes like color
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiprofiling for "automatic" (look at www.haskell.org/ghc)
4dcd2d1b64ccc7f705f2ce10d129ef9304ae413bChristian Maederrestrict proofs: only one prove window per node at a given time
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski************************************************
0d42a1490aa92c24b19823f745104eefbf29675dChristian Maederfurther task 1
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowski************************************************
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowskigenerate (x)html code from Doc
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowskigenerate more readable LaTeX-code
827a44bf2f3c22355f28dd83ec4511ea9e655dbdTill Mossakowskisee listings.sty for LaTeX generation (cf. CoSiT paper)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifurther task 2
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maeder************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUni-Refactoring,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskimake modules hierarchical, replace deprecated code (i.e. FiniteMap, hslibs),
99dc2aa6d6b19e22c508bdb45942ce85e9137fcfChristian Maederuse HaXml as a cabalized library, provide uni as (one?) cabal
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipackage(s), uni used to work under windows as well, watch the
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskii.e. FilePath, Process discussions (libraries@haskell.org)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipossibly switch to a subversion repository, talk to Achim
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski(amahnke@tzi.de)
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski************************************************
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowskifurther task 3
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski************************************************
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowskichange management
04ee0d20d16836bb6e835029a807c304973dea46Till Mossakowski reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski reload macht folgendes:
69b043b647fa86377c06a8c413c8539f099d8084Till Mossakowski lade CASL-Datei neu ==> neuer Entwicklungsgraph
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski vergleiche alten+neuen Entwicklungsgraph, konstruiere eine
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Abbildung (Common/Lib/Map.hs) von alt nach neu
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich (jeweils eine Abblidung f�r Knoten und eine f�r Kanten)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich Kriterien f�r Finden der Knotenabbildung:
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luetticheinfaches Merge von lokalen Beweisen eines abgespeichteren DG
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich in aktuellen DG
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichfurther task 4
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichrefined graph of Haskell module dependencies
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich using .import files
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichfurther task 5
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichport hets to windows. -- costs too much energy at this stage! Till
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichIf hets should become successful then requests for support under
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichwindows will surely follow.
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichGhc, uni and uDrawGraph should work under windows. Only Isabelle does
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichnot exist for windows, but SPASS does. Probably only a few path
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichcomputations need to be adapted (made modular) within hets. Also
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichposition computations (of Parsec) should be checked under windows.
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichremaining stuff
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichset up a ticket and tracking systems (for bugs and features) instead
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichof this messy todo list
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich--> sourceforge???
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowskirefactoring of dgraphs: add unique tags + hashes (but no table)
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski how to compare complex datastructures:
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski tag x1==tag x2 || (hash x1==hash x2 && x1==x2)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskidisplay library graph
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskiunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskiand uni/appl/ontologytool/AbstractGraphView.hs
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski(make it really abstract), possibly contact amahnke@tzi.de regarding
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiTaxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskiset up default simplifier
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskiset up default tactics using axioms
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski (see DOLCE sample files)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowskiimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
e0eee2b8144337bb54feb78d5a8b043041c9e028Till Mossakowski************************************************
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski************************************************
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskigenerate infrastructure for circular coinduction
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCCS example: commutativity of || by coinduction
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettich************************************************
baac12e7dd41b6e250e753c88ee0d40505509104Klaus LuettichIsabelle coding (let, case, etc.)
e0eee2b8144337bb54feb78d5a8b043041c9e028Till MossakowskiCoding out sub-types in HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicollect the patches for programatica (or create a package)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- conv (SN i p) = PN i (S p)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski+ conv (SN i p) = PN i (Sn (show i) p)
baac12e7dd41b6e250e753c88ee0d40505509104Klaus Luettichin programatica/tools/base/parse2/NumberNames.hs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifixes translation error of Pair
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskisimplification of HasCASL sentences (omit types)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogic COL is a ruin
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHaskell modules: hiding, renaming
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- group the axioms according to their leading operation/predicate symbol,
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski i.e. the f resp. the p in
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski if there are axioms not being of this form, output error
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiStatic analysis for HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski pattern analysis for program equations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski implemented only atomic subtyping
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiWeak amalgamation analysis?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiInstantiate Transformation Application system for HasCASL?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAutomatic generation of Haskell (for a HasCASL subset)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProofs in HasCASL
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiCoding HasCASL -> Isabelle with definedness axioms
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowski only strict functions are defined
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till MossakowskiIsabelle interface
05f44ad3061b64dbaafa801efdcac79d7abe38a9Till Mossakowski One emacs with spec and proof buffer
ce507cba25d24cfbb7c13f51bd67c4462862c2d1Till Mossakowski Reload button should rebuild buffers while keeping as much as possible
ce507cba25d24cfbb7c13f51bd67c4462862c2d1Till Mossakowski keep structuring of Hets theories
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till Mossakowski************************************************
42e6f81f0794a7b6bc8e29e97c55668abe96da59Till MossakowskiRainer (Klaus)
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski************************************************
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskiimplement a catch for calling MathServ based on the catch in runSpass
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski - a "connection refused" error should be handled differently:
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski "MathServ not running! Please contact
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski <hets-devel@informatik.uni-bremen.de>"
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowskifor the transition to ghc-6.6 spassProve must be corrected
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski - the regexp library changed in functionality
601e0da2d33c7b4ce6ece02a24ca52a88c5ccfa4Till Mossakowski maybe the parse of the proof tree should be done without regular
ec75b50a89aea0d96fd19ce864225267d0625f25Till Mossakowski performance improvements
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski - use seq to force the evaluation of the proof trees while in
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski GenericATP window otherwise "Exit prover" takes a long time
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski Example: seq (length $ show $ prooftree proofStatus) proofStatus
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski in GenericATP
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskiusability improvements
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski - forceFocus to read-only textedit widgets in textSaveDisplay windows
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski upon left mouse click
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski also add for Details window
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski - update of goal list-boxes should not longer move visible
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski area of the list
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski involves getting and setting of visible area
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskicode cleanup and documentation where necessary and possilbe
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski in SPASS/* and GUI/GenericATP*, GUI/Proofmanagement.hs
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowskifor ProofManagement-GUI
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski mark imported theorems for selection
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski extend Logic.Prover SenStatus with wasTheorem
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski somewhere in computeTheory implement setting of wasTheorem
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski if wasTheorem not appears with right status in ProofManagementGUI
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski add wasTheorem to Common.Result.Named, as well
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski and adapt conversion functions of SenStatus to Named and vice
9d927ffea9c067afe6187dfceb39359e7d7aacd3Till Mossakowski Mark old theorems in "Axioms to include" Listbox with prefixed
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski add button "Deselect former Theorems"
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski test all this with CASL-lib/Calculi/Space/RCCVerification.het
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski all nodes without incoming heterogeneous edges are provable with
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski************************************************
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski************************************************
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskifor ProofManagement-GUI
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski provide structured (based on spec-names) selection/deselection facility
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowski of axioms and theorems
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskitrace if liniarity of sentences along development is given
877db3191b09306a5f22df63cf1e9e9dad9a6ddcTill Mossakowskifor consistency checking with Isabelle, look at the following SAT-Solvers:
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiMChaff, ZChaff, Berkmin
f157913a0128ce772d0acd5038f61a7a619fd707Till MossakowskiConsistency checker interface
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski via global interface, accessible from global and node menus
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski use falseSentence from Logic.Logic (property: holds in no model)
f157913a0128ce772d0acd5038f61a7a619fd707Till Mossakowski proved -> inconsistent
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski disproved -> consistent (assuming completeness)
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski batch mode for automatic provers such as SPASS
52aad0502f0ddd332a28ae3fcd3327fa66d002f7Till Mossakowski (use automatic flag for provers)
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowskibatch interface for Isabelle
21d72ad1e64e2fa6d831f9def45d6dc21f6e0bd8Till Mossakowski each goal is proved separatedly, with a time limit enforced
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski by killing the process
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski the tactic is
cb1c5be39138fb8f037dbefc121fe41adc06845dTill Mossakowski "using Ax1 ... Axn by auto"
601f11cf0b4164a6a718038a736ae3d579f3a27cTill Mossakowski where Ax1 ... Axn is the list of all axioms.
601f11cf0b4164a6a718038a736ae3d579f3a27cTill Mossakowski "auto" could be replaced with "best", "blast" etc. (user selection)
7ed2a775680fb1a29e6907d372124906b7746420Till MossakowskiIgnore axiom selection for interactive provers
8980a8c8137a3a4c69bf9fdb3eca5b4b7f6e69c9Till MossakowskiTranslation between Achim's ontology data structure and CASL (in Hets)
aa6f6fa09091e92016598584162b9ba909af48ccTill Mossakowskivisualization of "taxonomy" of CASL signatures
85ab61b931e22a72a53628b8aa5d059eeaedf1bdTill Mossakowski (subsorts = inheritance, unary preds = concepts, binary preds = relations)
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski last two ... partially done
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiRecognize guarded fragment of CASL:
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski G ::= forall x . At(x) => G where At is a conjunction of atoms
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski | exists x . At(x) /\ G
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiJoost Visser wg. ATerms in Haskell => neues Repository
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski************************************************
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowski************************************************
331ed72b03dc966e023fecae5f0116b119082ccdTill MossakowskiBeweise in Isabelle
331ed72b03dc966e023fecae5f0116b119082ccdTill MossakowskiCASL consistency checker
331ed72b03dc966e023fecae5f0116b119082ccdTill MossakowskiWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
b2768faecd6610af357407a8ddfe1412a18f8ebcChristian Maeder (Vorbild: Larch-Handbuch)
60082d649e5bbb1c54f73f8921c3c390170e6c46Till MossakowskiSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
950ecce40ed5a97adf4460be07b47e3a0d0b1e56Till MossakowskiParser and static analysis for CSP-CASL
617a89d712d108f8d4c2bfe888a7e59566d17c0eTill Mossakowski************************************************
3e2c4de10a0eb284938b5d5307d1c1fc2f799456Till Mossakowski************************************************
dedca4980b2d43bc343ffcaf73e0617524f9720cTill MossakowskiCASL consistency checker
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIntegration with generic prover interface?
4be2c76af9603b48b147f1f369f713e78544974eTill Mossakowski************************************************
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowski************************************************
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiduplicate referenced node in SimpleDatatypes.casl
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowskienhance Web interface with SPASS (%implied, consistency)
60082d649e5bbb1c54f73f8921c3c390170e6c46Till Mossakowskitranslation of proofs along comorphisms (it this necessary at all???)
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski use inverse morphism?
e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski leads to translation of G_theory along comorphism that also
968edf72c9abb1e35ad5f41419d0399c6d9acf32Till Mossakowski keeps proof status info
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski this may be used in GUI prover interfaces for recovering old proof attempts
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski and offering them as default
e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskiproveCMDLinteractive (PGIP)
88c65bd4e8841502546923da0e81ade9045e8fecTill MossakowskiModel expansion flag for comorphisms
04d17d4f8862860f968f6b72b902163aacda6343Till MossakowskiUmlaute in daVinci anzeigen
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiFragen an Michael:
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskiwerden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?
2d76902bf3b380a32268ccc0d2cd9e376988a060Till Mossakowski was ist dort eigentlich das Problem?
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiCodierung von Subsorten?
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskipaper with Paolo
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski semantic adequecy of HOL translation
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiRegulate concurrent proving
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowski.dg files: store only current library; import .dg files for other libraries
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till MossakowskiIsabelle: use meta-quantifiers
d4f60a7dc41e0430d16c79f0d156e556d6d1ba37Till Mossakowskilocal subsumption ?
331ed72b03dc966e023fecae5f0116b119082ccdTill Mossakowskibetter syntax (Tina)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck for proved theorems
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiAbstractGraphView: switch to Result monad
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiunite or rename consCheck and cons_checkers
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBinInt.casl: revealing in Int1 does not work correctly
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifrom Stefan W�lfl:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskicomputeTheory does not work across library imports
2ee1615e999c5e0c49508ed4fcced7344b050042Till Mossakowskilocal theorems
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiall nodes named
f69658e57cba7ecb37c0d84181f4c563215c2534Till Mossakowskihierarchical Isabelle theories
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskidaVinci printing is not adequate
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskihiding of internal nodes does not work
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFOL without quantifiers and with uniform disjunctions
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (i.e. x R1 y \/ x R2 y)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (with and without =)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskialgorithmic path consistency over a relation algebra
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski plug in reasoner for this
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski develop correctness results (algorithmic path consistency=path consistency)
31c49f2fa23d4ac089f35145d80a224deb6ea7e4Till MossakowskiCASL sublogics:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski---------------
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFOL without quantifiers (with and without =)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiguarded fragment
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski[from DOLCE cooperation:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiontology mediation via pushouts/pullbacks/pulations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRobinson consistency with shared theory constructed via pre-image?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskishow theorem links between same instances of different parameterized
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski specs (where one is an extension of the other one)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilink menu for %implies, $def, %cons, even without open proof obligation
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifor a proved theorem, show minimal part of DG needed for proof
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicons, def, mono for nodes
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle interface: each qed should write proof info into file
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiglobally display nodes containing symbols mapped "twice" (i.e. via
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski different signature morphisms)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski and add a menu for each node allowing for tracking the different
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitopsort coding: partial functions as relations?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitheorem link menu for proof obligations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskiin Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiBuffer.het, sublogic of node Buffer:
b172714c339053a40393dc0cf4f9151c97695e01Till MossakowskiFail: illegal node type in sublogic computation
cc7492cd222f08d17c994912bcb0c60083ae2bc9Till MossakowskiJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifor CSP-CASL example: with logic
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiheterogeneous static ana
b172714c339053a40393dc0cf4f9151c97695e01Till Mossakowskitheorem links between nodes in different libraries
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskibasicProofs: use info about used axioms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski ensure that axiom/thm names are unique
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiOverload / inlineAxioms: injections
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiremove "prove" menu in abstracted dg
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskibetter sublogic analysis in codings
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskithy files in subdir
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiadjust path for thy files, such that hets can also be started from subdirs
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRestrict Sonjas simplifications to HasCASL
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiadd suitable axioms to simplifier and CR
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskicomputeTheory: remove double axioms
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiadd suitable axioms to simplifier and classical reasoner
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskibetter display of internal nodes (use tooltip?)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiupdate Hets, CASL, daVinci on web page
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipacking of binaries: add hets-update, refer to TclTk
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitest for sublogic before applying comorphism
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMissing points for heterogeneous WADT 04 example:
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- coding to Isabelle: translate sort gen constraints
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- Improve adapation to Isabelle's lexis
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiIsabelle: (ask Christoph)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski remove datatypes from sort list
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski prove local thm link (=> green)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski "prove" menu with choice windows
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski incorporate sublogics
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski sublogic translation table
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski better interaction between Isabelle instance (for one node)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski + selection of single goals that are proved
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski => use PGIP interface (Christoph, David)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski correct show theory
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Keep proofs and lemmas in .thy files (kind of merge)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski CASL-like syntax
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski CASL annotation for lemmas that should be used in proof
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski inherit CASL's mixfix syntax
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSignatures versus theories: where to store additional infos?
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicomp(id,x)=x for comorphism names
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiGeneralise CASL2Modal
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMixfix analysis + typecheck for modality axiomatizations
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModal logics: modal logic, temporal logic, mu calculus
144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski+ translations (e.g. modal to FOL)
144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL->Haskell with free DTs (mark sortgens) + recursion
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski- List[Dec] wird List[Pos]
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski- node numbers do not match
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski- thm links with external target should be provable as well
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiRemove warnings
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiDifferent types of logic translations
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiImprove Static analysis of structured specs
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiDevelopment graph calculus, Strategies for DG rules
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski use graph grammars to model rules? transformation units?
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiManagement of change
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill MossakowskiIntegrate provers
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski Otter model checker
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski FOL-prover by Uli Furhbach
2a6ba30d215dbf048c6cfee7f816d0eb0392aa6dTill Mossakowski modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
bd30fb0b81a1095db5b28d6dd7b294d8e8c9a0bfTill Mossakowski Isabelle codings: www.inf.ethz.ch/~vigano
Integration of MAYA and Isabelle/HOL (global HOL-Coding of
(i.e. signatures, axioms, signature morphisms in HOL,
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)
Data.Serizable (only when ghc supports it) better: rely on pointer equality
Improve encoding: CATS/basic_encode.sml (3 days)
More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
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)
IsaWin git/src/isa_ext/casl_thy.sml (1 week)
Basic datatypes CASL-lib/Basic/basic.casl
Conversion ASF/SDF-Parser -> abstract syntax (in Haskell)
Views on CASL specs: CATS/viewer.sml (2 weeks)
Module graph CATS/module_graph.sml (1 week) -> Maya?
ATerms via XML: CATS/aterms.sml (2 weeks)
Library management: CATS/lib_ana.sml (2 weeks)