todo revision c1015e823b467ffb3e58fe3eacb0db58937063ba
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringPlan and priority list for CoFI tool activities
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringSuchfunktion f�r einen Knoten im DG:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering erstmal auf eine Logik (z.B. CASL) beschr�nken
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - Funktion f�r Morphismus-Suche zwischen Theorien
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringKonfidenzgrade von Beweisen?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringvon Till/HiWi zu erledigen:
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart PoetteringRepr�sentation �ndern:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Beweisobjekte an DGs, nicht an Regeln -- done
5430f7f2bc7330f3088b894166bf3524a067e3d8Lennart Poettering F�r Theoreme in Theorien an Beweisobjekte -- done
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Definitionen auszeichnen -- done
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering F�r alles siehe G_theory, ThSens und SenStatus.
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Isabelles Beweisobjekte einbinden
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringIntegration with PGIP
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Hets needs to be equipped with a command-line interface that reads in
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering specification libraries and proof commands
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Proof commands are special annotations in the libraries
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering All menu commands of the development graph interface (GUI/...) should become (proof) commands
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering when stepping through the specs, dg calculus generates proof obligations
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering (for the current dg node only),
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering which then can be discharged by Isabelle, SPASS etc.
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering That is, the proof commands always occur at the position in the text
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering that generates the dg node?!? or should they occur after each specification?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering needs incremental parsing and static analysis for Hets libraries
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering easy: parse and analyse one specification at a time, and then process it with proof commands
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering more challenging: incrementally parse and analyse also individual specifications
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringModal-CASL <-> CASL-DL
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering see Chapter 4 of "The Description Logic Handbook"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering and ask Klaus for a print out of it
1fd961211df69ce672252d543bf4777738647048Zbigniew Jędrzejewski-Szmekimprove Modal-CASL
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek possibly also modal logic in CoCASL
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek**************** task A ************************
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-SzmekProofs with Isabelle and SPASS
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-SzmekCASL basic datatypes
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek- improve simplifier for partiality in Isabelle coding
1fd961211df69ce672252d543bf4777738647048Zbigniew Jędrzejewski-Szmek program interaction between solver, subgoaler and simplifier in such a way
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering that proofs of definedness conditions are postponed
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringModelchecker f�r algebraische Eigenschaften
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering neue Hets-Option in Driver/WriteFn.hs implementieren
9f7dad774ebfad23269800b7096eaad087481debVille Skyttä hets -n NonAssocRelationAlgebra
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering --modelSparQ=datei.lisp Calculi/Algebra/RelationAlgebra.casl
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering siehe auch CASL.CompositionTable.ComputeTable
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering modelCheck :: SIMPLE_ID -> (Sign f e, [Named (FORMULA f)])
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering -> Result Bool
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Warnung mit Gegenbspen ausgeben, wenn eine Eigenschaft nicht gilt
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering (abbrechen nach 10 Gegenbspen)
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering Warnungen erzeugen mit Funktion warning aus Common.Result
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering Range aus den CASL-FORMULAs extrahieren
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering Result ist eine Monade, ggf. mit do-Notation arbeiten
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering Allquantoren --> all, Existenzquantor --> any
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering CASL-Junktoren --> Haskell-Junktoren
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Terme rekursiv auswerten, Operationen aus der Table nehmen
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringAufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - ggf. Server nutzen
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - Vorverarbeitung f�r Solver (z.B. Duplikate raus)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering - Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringApplikation1 ---
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering | | -- Freibuger Solver
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering XML --- |---- Franz�sischer Solver
04ac799283f517672a5424e7c5bf066cfa4ca020Zbigniew Jędrzejewski-Szmek | |-- Hets -- Bremer Solver
04ac799283f517672a5424e7c5bf066cfa4ca020Zbigniew Jędrzejewski-SzmekApplikation2 ----- |
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Semantische Modelle/Korrektheit (CASL, HAsCASL)
04ac799283f517672a5424e7c5bf066cfa4ca020Zbigniew Jędrzejewski-SzmekXML-Einlesen in Haskell:
4d62fb4298a5904a53f484636c91540d08f68765Lennart PoetteringHXT (siehe OMDoc.XmlHandling): kann Namespaces
4d62fb4298a5904a53f484636c91540d08f68765Lennart Poettering(HaXML: kann Haskell-Datenypen in DTDs umwandeln)
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart PoetteringOutline der Diplomarbeit
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering Qualitative Constraint-Kalk�le (siehe Thomas)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering CASL-Formeln nur ganz kurz
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering ConstraintCASL
2b583ce6576d4a074ce6f1570b3e60b65c64ae7dKay Sievers Signaturen, Signaturmorphismen (aus CASL)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Modelle (aus CASL)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Erf�lltheit von Formeln
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering optional: Erf�lltheitsbedingung
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering M |= sigma(phi) <=> M|_sigma |= phi
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering f�r Signaturmorphismus sigma:Sigma_1->Sigma_2
9f7dad774ebfad23269800b7096eaad087481debVille Skyttä M \in Mod(Sigma_2), phi\in Sen(Sigma_1)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Formalisierung von Kalk�len in ConstraintCASL
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Constraint-Solver (auch in ihren Eigenheiten)
04d39279245834494baccfdb9349db8bf80abd13Lennart Poettering �bersetzungen zwischen den verschieden Formaten
04d39279245834494baccfdb9349db8bf80abd13Lennart Poettering praktischer Vergleich
04d39279245834494baccfdb9349db8bf80abd13Lennart Poettering�bersetzungen bis 30.Juni
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart Poettering ConstraintCASL -> Bremer Solver
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart Poettering Bremer Solver -> ConstraintCASL
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart Poettering Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers
9980033377c105d2cd6539c9d73ee61d4c2263b0Lennart Poettering parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt
f8964235e69f58225dec378437b1789744cd22a9Lennart Poettering Das kann das als Option in Hets eingebunden werden (Christian Maeder)
f8964235e69f58225dec378437b1789744cd22a9Lennart PoetteringFreiburger Constraint-Solver angucken im Juli
f8964235e69f58225dec378437b1789744cd22a9Lennart Poettering�bersetzungen bis 31. Juli
fb69ed55e5f8e82145440ba15075e8db807bf7faMichael Biebl ConstraintCASL -> Freibuger Solver/XML-Format
f8964235e69f58225dec378437b1789744cd22a9Lennart Poettering Freibuger Solver/XML-Format -> ConstraintCASL
f8964235e69f58225dec378437b1789744cd22a9Lennart Poettering************************************************
77b6e19458f37cfde127ec6aa9494c0ac45ad890Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringOmDoc-Ausgabe konform mit RelaxNG?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringOmDoc-Ausgabe Immanual zeigen
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-SzmekTypen von gebundenen Variablen weglassen
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-SzmekOMDoc-Datentyp einf�hren
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek Hets <-> Datenstruktur <-> OMDoc
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek Namensgenerierung/rekonstruktion auf der Seite Hets <-> Datenstruktur
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-SzmekUrsprung von Symbolen bei Hets -> OMDoc: irgendeins nehmen
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringAusgabe als DAG, mittels OMR oder ref
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Sharing-Algorithmus verwenden
a7f5bb1eafadbb08c8528baae588bbe773a37e79William GiokasConstraints mit Indizes: ggf. higher-order-Axiom erzeugen (Till fragen)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringAnzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringOMDoc-Bug melden f�r
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering free type Vehicle ::= sort Boat | sort Car
acbeb42770e1e99955ebc4464a0439cf741b3aebZbigniew Jędrzejewski-Szmek wobei Boat und Car aus anderen Files kommen
acbeb42770e1e99955ebc4464a0439cf741b3aebZbigniew Jędrzejewski-Szmek S. 156: Satz einfach streichen
acbeb42770e1e99955ebc4464a0439cf741b3aebZbigniew Jędrzejewski-Szmeksortdef legt bereits ein Symbol an
acbeb42770e1e99955ebc4464a0439cf741b3aebZbigniew Jędrzejewski-Szmekwerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering sie als erstes eingef�hrt wurden?
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering checken f�r Library-Importe
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringOMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart PoetteringHiding: unterschiedlich in OMDoc und Hets
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Signaturmorphismus
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering wird �bersetzt in einen OMDoc-Theoriemorphismus
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering mit leerer/identischer Abbildung, bei dem die Symbole aus
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Sigma_2 \ Sigma_1 versteckt werden
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Wenn der Signaturmorphismus keine Inklusion ist, ist keine
ab1f063390f55e14a8de87f21c4fad199eb908a6Lennart Poettering �bersetzung m�glich -> Fehler
a7f5bb1eafadbb08c8528baae588bbe773a37e79William Giokasein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering (also leere bzw. identische Abbildung) wird �bersetzt
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss
79640424059328268b9fb6c5fa8eb777b27a177eJan Engelhardt ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering der dann die Umbenennung macht, erzeugt werden
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringLogiken: �ber verschiedene OMDoc-Theorien mit URI
a7f5bb1eafadbb08c8528baae588bbe773a37e79William Giokas************************************************
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering************************************************
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering- CASL-Logik: "Relating CASL with other specification languages", S.401-408
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering siehe CASL reference manual (suche nach conservative)
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering- warum sind konservative Erweiterungen wichtig?
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering - um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert
870c4365cf3d407270788abe14d216a636ecf6c3Zbigniew Jędrzejewski-Szmek - f�r Refinement-Beweise
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,
0f0dbc46ccf5aaaf3131446d0a4d78bc97a37295Lennart Poettering definitional oder monomorph sind
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil - Beschreibung des Algorithmus in Pseudocode
4f755fc6ab8b75f89ed84c93cd5c3fac2a448b16Lennart Poettering - Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus
a7f5bb1eafadbb08c8528baae588bbe773a37e79William Giokas als konservativ erkennt, muss f�r jedes Modell der kleineren
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil Spezifikation eine Modellerweiterung zur gr��eren Spezifikation
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil gefunden werden. Z.B. im Falle von free types kann dies eine
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil Termalgebra-Konstruktion sein.
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil SP1 -- \sigma --> SP2
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocil SP2-Modell M2 mit M2|_\sigma=M1.
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal Vyskocilport CCC to Haskell
687d0825a4636b1841dc0c01fbcbf3160dddab74Michal VyskocilFunktionen imageOfMorphism und inhabited
7027ff61a34a12487712b382a061c654acc3a679Lennart Poettering von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
7027ff61a34a12487712b382a061c654acc3a679Lennart Poettering mit "cvs add SigFuns.hs" einchecken
7027ff61a34a12487712b382a061c654acc3a679Lennart Poettering"free datatypes and recursive equations are consistent"
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringcheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringJust True => Yes, is consistent
7027ff61a34a12487712b382a061c654acc3a679Lennart PoetteringJust False => No, is inconsistent
79640424059328268b9fb6c5fa8eb777b27a177eJan EngelhardtNothing => don't know
7027ff61a34a12487712b382a061c654acc3a679Lennart Poetteringcall the symbols in the image of the signature morphism "new"
7027ff61a34a12487712b382a061c654acc3a679Lennart Poettering- each new sort must be a free type,
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering i.e. it must occur in a sort generation constraint that is marked as free
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering (Sort_gen_ax constrs True)
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
e9dd9f9547350c7dc0473583b5c2228dc8f0ab76Jason St. John if not, output "don't know"
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering and there must be one term of that sort (inhabited)
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering if not, output "no"
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering- group the axioms according to their leading operation/predicate symbol,
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering i.e. the f resp. the p in
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
144f0fc0c8a5e2f6b72179e2b5fb992474da24adLennart Poettering Implication Application Strong_equation
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Implication Predication Equivalence
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering if there are axioms not being of this form, output "don't know"
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringcheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringcheck' [] = ([([],[])],emptyUniqSet)
ff01d048b4c1455241c894cf7982662c9d28fd34Lennart Poettering-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poetteringcheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringcheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering | all_vars ps = (pats, addOneToUniqSet indexs n)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering (pats,indexs) = check' rs
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering-- falls ein Konstruktor dabei ist: split_by_constructor
73e231abde39f22097df50542c745e01de879836Jan Engelhardt-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poetteringcheck' qs@((EqnInfo n ctx ps result):_)
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poettering | all_vars ps = ([], unitUniqSet n)
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poettering | constructors = split_by_constructor qs
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poettering | only_vars = first_column_only_vars qs
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poettering | otherwise = panic "Check.check': Not implemented :-("
a41fe3a29372f8e6c4e7733bf85940a023811301Lennart Poettering -- Note: RecPats will have been simplified to ConPats
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering -- at this stage.
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering constructors = or (map is_con qs)
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering only_vars = and (map is_var qs)
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poetteringsubsort definitions: are conservative if formula is satisfiable
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering (generate proof obligation)
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering************************************************
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poettering************************************************
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart PoetteringOWL-DL (<)-> CASL-DL
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poettering highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering some operation symbols
aa28aefe61c5406c5cb631f3e82457b6d1bcc967Lennart Poettering show hets output immediately
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poettering C-c C-g for hets -g
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering when hets terminates abnormally (e.g. with a fail), emacs loops
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering C-n jumps to the next error, but the message windows is not always scrolled
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering in such a way that the error is at the top (for long error lists)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering should work with parser error messages as well (adapt these?)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering easier setup of emacs mode
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering by just loading one file
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering integration into installer
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering checking for emacs and offer adaption of ~/.emacs
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering Version for XEamcs?
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering************************************************
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering************************************************
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersenlook at command line interface (just call hets)
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersenimplement simplified rule Theorem-Hide-Shift
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom GundersenIf there is an open global theorem link sigma:N1->N2 and
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersena hiding definition link theta:N3->N2 (i.e. the signature
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersenmorphism theta is from Sig(N2) to Sig(N3)), then prove
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersenthis theorem link by inserting a new global theorem link
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersentheta o sigma : N1->N3.
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersenuse functions from Proofs.TheoremHideShift
ab046dde6f355f4a8b07ff6120a7ef51f5d49fc9Tom Gundersen test file: see CASL-lib/test_TheoremHideShift.casl
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering (when doing Automatic, HideTheoremShift, Automatic, and then
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering local proof in Target')
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringissue warning whne displaing theories (or performing proofs) of
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringnodes with ingoing hiding links.
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringimprove dependency tracking for development graph proofs
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering display proved theorem links that depend on pending other proofs in yellow
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering (other proofs = proofs of other links or %implied theorems -
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering track which of the latter are actually used)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringdisplay normal form of nodes with ingoing hiding links
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringtry out examples
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringconservativity calculus
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringpushouts http://en.wikipedia.org/wiki/Pushout_%28category_theory%29
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringweakly amalgamable cocones
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poetteringdevelopment graph calculus
bc2f673ec24b59948fcfc35b3077fda0314e69d8Lennart Poettering(see Sect. IV:4.4 of the CASL Reference Manual)
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringlook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringtest command line interface (just call hets)
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringtest development graph GUI:
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering global decomposition
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering menu edit - unnamed nodes - hide/show nodes,
88d04e31ce0837ebf937ab46c3c39a0d93ab4c7cLennart Poettering node menu: show just subtree / undo
88d04e31ce0837ebf937ab46c3c39a0d93ab4c7cLennart Poettering interaction with edit - proofs - automatic?
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering use update of uDrawGraph-nodes,edges instead of erasing and adding nodes
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering for attribute changes like color
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringprofiling for "automatic" (look at www.haskell.org/ghc)
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poetteringrestrict proofs: only one prove window per node at a given time
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering************************************************
88d04e31ce0837ebf937ab46c3c39a0d93ab4c7cLennart Poettering************************************************
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poetteringgenerate (x)html code from Doc
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poetteringgenerate more readable LaTeX-code
a42c8b54b1619078c02f5e439bd2564c6d0f901fLennart Poetteringsee listings.sty for LaTeX generation (cf. CoSiT paper)
39ed67d14694983dabd6641c02216aa440eed767Lennart Poettering************************************************
5076f0ccfd36b67512d44fe355b80305ced7dcbaLennart Poettering************************************************
420c7379fb96a188459690a634d0fede55721183Lennart PoetteringUni-Refactoring,
420c7379fb96a188459690a634d0fede55721183Lennart Poetteringmake modules hierarchical, replace deprecated code (i.e. FiniteMap, hslibs),
420c7379fb96a188459690a634d0fede55721183Lennart Poetteringuse HaXml as a cabalized library, provide uni as (one?) cabal
420c7379fb96a188459690a634d0fede55721183Lennart Poetteringpackage(s), uni used to work under windows as well, watch the
420c7379fb96a188459690a634d0fede55721183Lennart Poetteringi.e. FilePath, Process discussions (libraries@haskell.org)
420c7379fb96a188459690a634d0fede55721183Lennart Poetteringpossibly switch to a subversion repository, talk to Achim
420c7379fb96a188459690a634d0fede55721183Lennart Poettering(amahnke@tzi.de)
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering************************************************
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering************************************************
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringchange management
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering reload macht folgendes:
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering lade CASL-Datei neu ==> neuer Entwicklungsgraph
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering vergleiche alten+neuen Entwicklungsgraph, konstruiere eine
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering Abbildung (Common/Lib/Map.hs) von alt nach neu
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering (jeweils eine Abblidung f�r Knoten und eine f�r Kanten)
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek Kriterien f�r Finden der Knotenabbildung:
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmekeinfaches Merge von lokalen Beweisen eines abgespeichteren DG
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering in aktuellen DG
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering************************************************
e670b166a08b7c1031a9e7d7675fa9a29c3e19c9Zbigniew Jędrzejewski-Szmek************************************************
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringrefined graph of Haskell module dependencies
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek using .import files
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering************************************************
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmek************************************************
27407a01c6c115ed09ad938ab95dcb56ab963ba9Zbigniew Jędrzejewski-Szmekport hets to windows. -- costs too much energy at this stage! Till
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart PoetteringIf hets should become successful then requests for support under
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringwindows will surely follow.
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart PoetteringGhc, uni and uDrawGraph should work under windows. Only Isabelle does
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringnot exist for windows, but SPASS does. Probably only a few path
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringcomputations need to be adapted (made modular) within hets. Also
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringposition computations (of Parsec) should be checked under windows.
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering************************************************
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringremaining stuff
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poettering************************************************
57fb9fb56db0584581ce33ee842dcbf5f1136856Lennart Poetteringset up a ticket and tracking systems (for bugs and features) instead
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poetteringof this messy todo list
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering--> sourceforge???
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringrefactoring of dgraphs: add unique tags + hashes (but no table)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering how to compare complex datastructures:
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poettering tag x1==tag x2 || (hash x1==hash x2 && x1==x2)
69c79d3c32ff4d6a572ee1cdec248b27df1fb6caLennart Poetteringdisplay library graph
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poetteringunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poetteringand uni/appl/ontologytool/AbstractGraphView.hs
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poettering(make it really abstract), possibly contact amahnke@tzi.de regarding
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart PoetteringTaxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poetteringset up default simplifier
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poetteringset up default tactics using axioms
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poettering (see DOLCE sample files)
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poetteringimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poettering************************************************
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poettering************************************************
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart Poetteringgenerate infrastructure for circular coinduction
17fe052346f1d905b5ce0f12123b5ce24e992c6bLennart PoetteringCCS example: commutativity of || by coinduction
f4889f656b477887b02caa5e9d27387309c75a87Lennart Poettering************************************************
f4889f656b477887b02caa5e9d27387309c75a87Lennart Poettering************************************************
f4889f656b477887b02caa5e9d27387309c75a87Lennart PoetteringIsabelle coding (let, case, etc.)
f4889f656b477887b02caa5e9d27387309c75a87Lennart PoetteringCoding out sub-types in HasCASL
f4889f656b477887b02caa5e9d27387309c75a87Lennart Poetteringcollect the patches for programatica (or create a package)
f4889f656b477887b02caa5e9d27387309c75a87Lennart Poettering- conv (SN i p) = PN i (S p)
f4889f656b477887b02caa5e9d27387309c75a87Lennart Poettering+ conv (SN i p) = PN i (Sn (show i) p)
f4889f656b477887b02caa5e9d27387309c75a87Lennart Poetteringin programatica/tools/base/parse2/NumberNames.hs
f4889f656b477887b02caa5e9d27387309c75a87Lennart Poetteringfixes translation error of Pair
f4889f656b477887b02caa5e9d27387309c75a87Lennart Poetteringsimplification of HasCASL sentences (omit types)
8a96d94e4c33173d1426b7e0a6325405804ba224Lennart PoetteringLogic COL is a ruin
8a96d94e4c33173d1426b7e0a6325405804ba224Lennart PoetteringHaskell modules: hiding, renaming
8a96d94e4c33173d1426b7e0a6325405804ba224Lennart Poettering- group the axioms according to their leading operation/predicate symbol,
8a96d94e4c33173d1426b7e0a6325405804ba224Lennart Poettering i.e. the f resp. the p in
8a96d94e4c33173d1426b7e0a6325405804ba224Lennart Poettering forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
8a96d94e4c33173d1426b7e0a6325405804ba224Lennart Poettering forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
8a96d94e4c33173d1426b7e0a6325405804ba224Lennart Poettering if there are axioms not being of this form, output error
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart PoetteringStatic analysis for HasCASL
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering pattern analysis for program equations
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering implemented only atomic subtyping
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart PoetteringWeak amalgamation analysis?
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart PoetteringInstantiate Transformation Application system for HasCASL?
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart PoetteringAutomatic generation of Haskell (for a HasCASL subset)
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart PoetteringProofs in HasCASL
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart PoetteringCoding HasCASL -> Isabelle with definedness axioms
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering only strict functions are defined
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart PoetteringIsabelle interface
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering One emacs with spec and proof buffer
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering Reload button should rebuild buffers while keeping as much as possible
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering keep structuring of Hets theories
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering************************************************
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering************************************************
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poetteringimplement a catch for calling MathServ based on the catch in runSpass
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering - a "connection refused" error should be handled differently:
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering "MathServ not running! Please contact
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering <hets-devel@informatik.uni-bremen.de>"
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poetteringfor the transition to ghc-6.6 spassProve must be corrected
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering - the regexp library changed in functionality
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering maybe the parse of the proof tree should be done without regular
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering performance improvements
eb91eb187b7491e05fb95215b77cb62061f41d08Lennart Poettering - use seq to force the evaluation of the proof trees while in
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering GenericATP window otherwise "Exit prover" takes a long time
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering Example: seq (length $ show $ prooftree proofStatus) proofStatus
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poetteringusability improvements
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering - forceFocus to read-only textedit widgets in textSaveDisplay windows
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering upon left mouse click
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering also add for Details window
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering - update of goal list-boxes should not longer move visible
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering area of the list
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering involves getting and setting of visible area
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poetteringcode cleanup and documentation where necessary and possilbe
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering in SPASS/* and GUI/GenericATP*, GUI/Proofmanagement.hs
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poetteringfor ProofManagement-GUI
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering mark imported theorems for selection
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering extend Logic.Prover SenStatus with wasTheorem
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering somewhere in computeTheory implement setting of wasTheorem
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering if wasTheorem not appears with right status in ProofManagementGUI
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering add wasTheorem to Common.Result.Named, as well
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering and adapt conversion functions of SenStatus to Named and vice
89f7c8465cd1ab37347dd0c15920bce31e8225dfLennart Poettering Mark old theorems in "Axioms to include" Listbox with prefixed
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering add button "Deselect former Theorems"
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering test all this with CASL-lib/Calculi/Space/RCCVerification.het
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering all nodes without incoming heterogeneous edges are provable with
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
2b3987a863975f5a1fa1754725e3d07a5d4f6478Lennart Poettering************************************************
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart PoetteringMaude as logic in Hets
845c53246f73a505f12bb7f685a530045fa60a40Zbigniew Jędrzejewski-SzmekUse Maude for CASL rewriting
2b3987a863975f5a1fa1754725e3d07a5d4f6478Lennart PoetteringUse Maude as a model description language for modal logic,
2b3987a863975f5a1fa1754725e3d07a5d4f6478Lennart Poettering integrate Maude model cheker (connection with ModalCASL)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Also integrate other model checkers (SMV, SPIN)?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Translations between model description languages?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering Run model checkers in parallel?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering************************************************
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poetteringfor ProofManagement-GUI
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering provide structured (based on spec-names) selection/deselection facility
25f5971b5e0b3ab5b91a7d0359cd7f5a5094c1d0Lennart Poettering of axioms and theorems
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringtrace if liniarity of sentences along development is given
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam Giokasfor consistency checking with Isabelle, look at the following SAT-Solvers:
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam GiokasMChaff, ZChaff, Berkmin
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam GiokasConsistency checker interface
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam Giokas via global interface, accessible from global and node menus
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam Giokas use falseSentence from Logic.Logic (property: holds in no model)
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam Giokas proved -> inconsistent
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam Giokas disproved -> consistent (assuming completeness)
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam Giokas batch mode for automatic provers such as SPASS
68562936c243a2e2190a7232c4805ffd094e9b3bWilliam Giokas (use automatic flag for provers)
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-Szmekbatch interface for Isabelle
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-Szmek each goal is proved separatedly, with a time limit enforced
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-Szmek by killing the process
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-Szmek "using Ax1 ... Axn by auto"
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-Szmek where Ax1 ... Axn is the list of all axioms.
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-Szmek "auto" could be replaced with "best", "blast" etc. (user selection)
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-SzmekIgnore axiom selection for interactive provers
9cb74bcb23dde8488459ca233bf9caee642b8402Zbigniew Jędrzejewski-SzmekTranslation between Achim's ontology data structure and CASL (in Hets)
f9f4dd51bdb016bab84f7fb3cf47a2ad102b4c76Zbigniew Jędrzejewski-Szmekvisualization of "taxonomy" of CASL signatures
f9f4dd51bdb016bab84f7fb3cf47a2ad102b4c76Zbigniew Jędrzejewski-Szmek (subsorts = inheritance, unary preds = concepts, binary preds = relations)
f9f4dd51bdb016bab84f7fb3cf47a2ad102b4c76Zbigniew Jędrzejewski-Szmek last two ... partially done
f9f4dd51bdb016bab84f7fb3cf47a2ad102b4c76Zbigniew Jędrzejewski-SzmekRecognize guarded fragment of CASL:
f9f4dd51bdb016bab84f7fb3cf47a2ad102b4c76Zbigniew Jędrzejewski-Szmek G ::= forall x . At(x) => G where At is a conjunction of atoms
f9f4dd51bdb016bab84f7fb3cf47a2ad102b4c76Zbigniew Jędrzejewski-Szmek | exists x . At(x) /\ G
f9f4dd51bdb016bab84f7fb3cf47a2ad102b4c76Zbigniew Jędrzejewski-SzmekJoost Visser wg. ATerms in Haskell => neues Repository
a8828ed93878b4b4866d40ebfb660e54995ff72eDaniel J Walsh************************************************
a8828ed93878b4b4866d40ebfb660e54995ff72eDaniel J Walsh************************************************
a8828ed93878b4b4866d40ebfb660e54995ff72eDaniel J WalshBeweise in Isabelle
82adf6af7c72b852449346835f33184a841b4796Lennart PoetteringCASL consistency checker
a8828ed93878b4b4866d40ebfb660e54995ff72eDaniel J WalshWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
f9f4dd51bdb016bab84f7fb3cf47a2ad102b4c76Zbigniew Jędrzejewski-Szmek (Vorbild: Larch-Handbuch)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringParser and static analysis for CSP-CASL
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringCASL consistency checker
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart PoetteringIntegration with generic prover interface?
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering************************************************
4d62fb4298a5904a53f484636c91540d08f68765Lennart Poettering************************************************
04d39279245834494baccfdb9349db8bf80abd13Lennart Poetteringduplicate referenced node in SimpleDatatypes.casl
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringenhance Web interface with SPASS (%implied, consistency)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poetteringtranslation of proofs along comorphisms (it this necessary at all???)
8f7a3c1402a8de36b2c63935358a53510d2fe7c1Lennart Poettering use inverse morphism?
BinInt.casl: revealing in Int1 does not work correctly
(i.e. x R1 y \/ x R2 y)
ontology mediation via pushouts/pullbacks/pulations
globally display nodes containing symbols mapped "twice" (i.e. via
uses of the symbols/concepts
UserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
Buffer.het, sublogic of node Buffer:
ensure that axiom/thm names are unique
+ translations (e.g. modal to FOL)
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)