todo revision 7805ba9a692e55ad925baf0fca762a7ee39ea006
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaPlan and priority list for CoFI tool activities
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaSuchfunktion f�r einen Knoten im DG:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana erstmal auf eine Logik (z.B. CASL) beschr�nken
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - Funktion f�r Morphismus-Suche zwischen Theorien
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaKonfidenzgrade von Beweisen?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanavon Till/HiWi zu erledigen:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRepr�sentation �ndern:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Beweisobjekte an DGs, nicht an Regeln -- done
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana F�r Theoreme in Theorien an Beweisobjekte -- done
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana BasicProof mit Liste von Beweisobjekten -- �berfl�ssig
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Definitionen auszeichnen -- done
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana F�r alles siehe G_theory, ThSens und SenStatus.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Isabelles Beweisobjekte einbinden
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIntegration with PGIP
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Hets needs to be equipped with a command-line interface that reads in
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana specification libraries and proof commands
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Proof commands are special annotations in the libraries
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana All menu commands of the development graph interface (GUI/...) should become (proof) commands
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana when stepping through the specs, dg calculus generates proof obligations
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (for the current dg node only),
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana which then can be discharged by Isabelle, SPASS etc.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana That is, the proof commands always occur at the position in the text
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana that generates the dg node?!? or should they occur after each specification?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana needs incremental parsing and static analysis for Hets libraries
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana easy: parse and analyse one specification at a time, and then process it with proof commands
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana more challenging: incrementally parse and analyse also individual specifications
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaModal-CASL <-> CASL-DL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana see Chapter 4 of "The Description Logic Handbook"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana and ask Klaus for a print out of it
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaimprove Modal-CASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana possibly also modal logic in CoCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana**************** task A ************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaProofs with Isabelle and SPASS
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCASL basic datatypes
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHasCASL examples
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- improve simplifier for partiality in Isabelle coding
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana program interaction between solver, subgoaler and simplifier in such a way
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana that proofs of definedness conditions are postponed
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaModelchecker f�r algebraische Eigenschaften
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana neue Hets-Option in Driver/WriteFn.hs implementieren
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana hets -n NonAssocRelationAlgebra
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana --modelSparQ=datei.lisp Calculi/Algebra/RelationAlgebra.casl
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana siehe auch CASL.CompositionTable.ComputeTable
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana modelCheck :: SIMPLE_ID -> (Sign f e, [Named (FORMULA f)])
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana -> Result Bool
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Warnung mit Gegenbspen ausgeben, wenn eine Eigenschaft nicht gilt
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (abbrechen nach 10 Gegenbspen)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Warnungen erzeugen mit Funktion warning aus Common.Result
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Range aus den CASL-FORMULAs extrahieren
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Result ist eine Monade, ggf. mit do-Notation arbeiten
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Pr�fung der G�ltigkeit von CASL-Formel in einer Table, rekursiv:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Allquantoren --> all, Existenzquantor --> any
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana CASL-Junktoren --> Haskell-Junktoren
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Terme rekursiv auswerten, Operationen aus der Table nehmen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAufgabe von Shi Hui: XML-Anfragen mit DCC-Ausdr�cken an Bremer Solver schicken
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - ggf. Server nutzen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - Vorverarbeitung f�r Solver (z.B. Duplikate raus)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - Shi soll auf Freiburger XML-Format umsteigen (ggf. mit XSLT)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaApplikation1 ---
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | | -- Freibuger Solver
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana XML --- |---- Franz�sischer Solver
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | |-- Hets -- Bremer Solver
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaApplikation2 ----- |
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ConstraintCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Semantische Modelle/Korrektheit (CASL, HAsCASL)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaXML-Einlesen in Haskell:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHXT (siehe OMDoc.XmlHandling): kann Namespaces
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana(HaXML: kann Haskell-Datenypen in DTDs umwandeln)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaOutline der Diplomarbeit
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Qualitative Constraint-Kalk�le (siehe Thomas)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana CASL (siehe Paper T. Mossakowski: Relating CASL with Other Specification Languages:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana the Institution Level Theoretical Computer Science 286, p. 367-475, 2002.)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana CASL-Formeln nur ganz kurz
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ConstraintCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Signaturen, Signaturmorphismen (aus CASL)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Modelle (aus CASL)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Erf�lltheit von Formeln
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana optional: Erf�lltheitsbedingung
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana M |= sigma(phi) <=> M|_sigma |= phi
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana f�r Signaturmorphismus sigma:Sigma_1->Sigma_2
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana M \in Mod(Sigma_2), phi\in Sen(Sigma_1)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Formalisierung von Kalk�len in ConstraintCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Constraint-Solver (auch in ihren Eigenheiten)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana �bersetzungen zwischen den verschieden Formaten
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana praktischer Vergleich
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana�bersetzungen bis 30.Juni
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ConstraintCASL -> Bremer Solver
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Bremer Solver -> ConstraintCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Das kann das als Option in Hets eingebunden werden (Christian Maeder)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaFreiburger Constraint-Solver angucken im Juli
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana�bersetzungen bis 31. Juli
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ConstraintCASL -> Freibuger Solver/XML-Format
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Freibuger Solver/XML-Format -> ConstraintCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaOmDoc-Ausgabe konform mit RelaxNG?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaOmDoc-Ausgabe Immanual zeigen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaTypen von gebundenen Variablen weglassen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaOMDoc-Datentyp einf�hren
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Hets <-> Datenstruktur <-> OMDoc
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Namensgenerierung/rekonstruktion auf der Seite Hets <-> Datenstruktur
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaUrsprung von Symbolen bei Hets -> OMDoc: irgendeins nehmen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAusgabe als DAG, mittels OMR oder ref
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Sharing-Algorithmus verwenden
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaConstraints mit Indizes: ggf. higher-order-Axiom erzeugen (Till fragen)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAnzeigen von lokalen Beweiszielen bei nicht-gesetztem Cons: Till fragen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaOMDoc-Bug melden f�r
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana free type Vehicle ::= sort Boat | sort Car
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana wobei Boat und Car aus anderen Files kommen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana S. 156: Satz einfach streichen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanasortdef legt bereits ein Symbol an
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanawerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana sie als erstes eingef�hrt wurden?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana checken f�r Library-Importe
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaOMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHiding: unterschiedlich in OMDoc und Hets
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Signaturmorphismus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana wird �bersetzt in einen OMDoc-Theoriemorphismus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana mit leerer/identischer Abbildung, bei dem die Symbole aus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Sigma_2 \ Sigma_1 versteckt werden
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Wenn der Signaturmorphismus keine Inklusion ist, ist keine
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana �bersetzung m�glich -> Fehler
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (also leere bzw. identische Abbildung) wird �bersetzt
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana der dann die Umbenennung macht, erzeugt werden
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaLogiken: �ber verschiedene OMDoc-Theorien mit URI
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- CASL-Logik: "Relating CASL with other specification languages", S.401-408
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- Konservative, definitionale und monomorphe Erweiterungen, Konsistenz
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana siehe CASL reference manual (suche nach conservative)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- warum sind konservative Erweiterungen wichtig?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - um zu pr�fen, ob Spezifikationen konsistent sind, also implementiert
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - f�r Refinement-Beweise
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- Algorithmen zur Pr�fung von Erweiterungen, ob diese konservativ,
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana definitional oder monomorph sind
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - Beschreibung des Algorithmus in Pseudocode
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - Korrektheitsbeweis, d.h. f�r die Erweiterungen, die der Algorithmus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana als konservativ erkennt, muss f�r jedes Modell der kleineren
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Spezifikation eine Modellerweiterung zur gr��eren Spezifikation
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana gefunden werden. Z.B. im Falle von free types kann dies eine
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Termalgebra-Konstruktion sein.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana SP1 -- \sigma --> SP2
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana konservativ: jedes SP_1-Modell M1 hat eine Erweiterung zu einem
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana SP2-Modell M2 mit M2|_\sigma=M1.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaport CCC to Haskell
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaFunktionen imageOfMorphism und inhabited
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana mit "cvs add SigFuns.hs" einchecken
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana"free datatypes and recursive equations are consistent"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanacheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaJust True => Yes, is consistent
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaJust False => No, is inconsistent
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaNothing => don't know
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacall the symbols in the image of the signature morphism "new"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- each new sort must be a free type,
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana i.e. it must occur in a sort generation constraint that is marked as free
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (Sort_gen_ax constrs True)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana if not, output "don't know"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana and there must be one term of that sort (inhabited)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana if not, output "no"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- group the axioms according to their leading operation/predicate symbol,
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana i.e. the f resp. the p in
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Implication Application Strong_equation
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Implication Predication Equivalence
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana if there are axioms not being of this form, output "don't know"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacheck' [] = ([([],[])],emptyUniqSet)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana-- nur ein Pattern, bestehend aus nur Variablen? fertig, True
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacheck' [EqnInfo n ctx ps (MatchResult CanFail _)]
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | all_vars ps = (pats, addOneToUniqSet indexs n)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (pats,indexs) = check' rs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana-- falls ein Konstruktor dabei ist: split_by_constructor
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana-- wenn die ersten Argument nur Variablen sind: first_column_only_vars
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacheck' qs@((EqnInfo n ctx ps result):_)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | all_vars ps = ([], unitUniqSet n)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | constructors = split_by_constructor qs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | only_vars = first_column_only_vars qs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | otherwise = panic "Check.check': Not implemented :-("
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana -- Note: RecPats will have been simplified to ConPats
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana -- at this stage.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana constructors = or (map is_con qs)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana only_vars = and (map is_var qs)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanasubsort definitions: are conservative if formula is satisfiable
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (generate proof obligation)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaOWL-DL (<)-> CASL-DL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana some operation symbols
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana show hets output immediately
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana C-c C-g for hets -g
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana when hets terminates abnormally (e.g. with a fail), emacs loops
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana C-n jumps to the next error, but the message windows is not always scrolled
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana in such a way that the error is at the top (for long error lists)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Version for XEamcs?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana should work with parser error messages as well (adapt these?)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanalook at command line interface (just call hets)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaimplement simplified rule Theorem-Hide-Shift
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIf there is an open global theorem link sigma:N1->N2 and
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaa hiding definition link theta:N3->N2 (i.e. the signature
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanamorphism theta is from Sig(N2) to Sig(N3)), then prove
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanathis theorem link by inserting a new global theorem link
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatheta o sigma : N1->N3.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanause functions from Proofs.TheoremHideShift
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana test file: see CASL-lib/test_TheoremHideShift.casl
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (when doing Automatic, HideTheoremShift, Automatic, and then
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana local proof in Target')
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaissue warning whne displaing theories (or performing proofs) of
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushananodes with ingoing hiding links.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaimprove dependency tracking for development graph proofs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana display proved theorem links that depend on pending other proofs in yellow
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanadisplay normal form of nodes with ingoing hiding links
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatry out examples
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaconservativity calculus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanapushouts http://en.wikipedia.org/wiki/Pushout_%28category_theory%29
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaweakly amalgamable cocones
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanadevelopment graph calculus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana(see Sect. IV:4.4 of the CASL Reference Manual)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanalook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatest command line interface (just call hets)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatest development graph GUI:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana global decomposition
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana menu edit - unnamed nodes - hide/show nodes,
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana node menu: show just subtree / undo
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana interaction with edit - proofs - automatic?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana use update of uDrawGraph-nodes,edges instead of erasing and adding nodes
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana for attribute changes like color
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaprofiling for "automatic" (look at www.haskell.org/ghc)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanarestrict proofs: only one prove window per node at a given time
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanagenerate (x)html code from Doc
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanagenerate more readable LaTeX-code
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanasee listings.sty for LaTeX generation (cf. CoSiT paper)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaUni-Refactoring,
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanamake modules hierarchical, replace deprecated code (i.e. FiniteMap, hslibs),
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanause HaXml as a cabalized library, provide uni as (one?) cabal
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanapackage(s), uni used to work under windows as well, watch the
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanai.e. FilePath, Process discussions (libraries@haskell.org)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanapossibly switch to a subversion repository, talk to Achim
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana(amahnke@tzi.de)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanachange management
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana reload macht folgendes:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana lade CASL-Datei neu ==> neuer Entwicklungsgraph
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana vergleiche alten+neuen Entwicklungsgraph, konstruiere eine
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Abbildung (Common/Lib/Map.hs) von alt nach neu
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (jeweils eine Abblidung f�r Knoten und eine f�r Kanten)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Kriterien f�r Finden der Knotenabbildung:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaeinfaches Merge von lokalen Beweisen eines abgespeichteren DG
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana in aktuellen DG
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanarefined graph of Haskell module dependencies
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana using .import files
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaport hets to windows. -- costs too much energy at this stage! Till
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIf hets should become successful then requests for support under
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanawindows will surely follow.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaGhc, uni and uDrawGraph should work under windows. Only Isabelle does
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushananot exist for windows, but SPASS does. Probably only a few path
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacomputations need to be adapted (made modular) within hets. Also
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaposition computations (of Parsec) should be checked under windows.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaremaining stuff
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaset up a ticket and tracking systems (for bugs and features) instead
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaof this messy todo list
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana--> sourceforge???
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanarefactoring of dgraphs: add unique tags + hashes (but no table)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana how to compare complex datastructures:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana tag x1==tag x2 || (hash x1==hash x2 && x1==x2)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanadisplay library graph
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaunify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaand uni/appl/ontologytool/AbstractGraphView.hs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana(make it really abstract), possibly contact amahnke@tzi.de regarding
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaTaxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaset up default simplifier
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaset up default tactics using axioms
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (see DOLCE sample files)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaimprove efficiency (e.g. of UserManual/Sbcs.casl), using profiling
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanagenerate infrastructure for circular coinduction
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCCS example: commutativity of || by coinduction
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIsabelle coding (let, case, etc.)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCoding out sub-types in HasCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacollect the patches for programatica (or create a package)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- conv (SN i p) = PN i (S p)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana+ conv (SN i p) = PN i (Sn (show i) p)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanain programatica/tools/base/parse2/NumberNames.hs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafixes translation error of Pair
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanasimplification of HasCASL sentences (omit types)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaLogic COL is a ruin
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHaskell modules: hiding, renaming
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- group the axioms according to their leading operation/predicate symbol,
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana i.e. the f resp. the p in
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana if there are axioms not being of this form, output error
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaStatic analysis for HasCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana pattern analysis for program equations
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana implemented only atomic subtyping
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaWeak amalgamation analysis?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaInstantiate Transformation Application system for HasCASL?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAutomatic generation of Haskell (for a HasCASL subset)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaProofs in HasCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCoding HasCASL -> Isabelle with definedness axioms
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana only strict functions are defined
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIsabelle interface
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana One emacs with spec and proof buffer
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Reload button should rebuild buffers while keeping as much as possible
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana keep structuring of Hets theories
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaimplement a catch for calling MathServ based on the catch in runSpass
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - a "connection refused" error should be handled differently:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana "MathServ not running! Please contact
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana <hets-devel@informatik.uni-bremen.de>"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafor the transition to ghc-6.6 spassProve must be corrected
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - the regexp library changed in functionality
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana maybe the parse of the proof tree should be done without regular
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana performance improvements
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - use seq to force the evaluation of the proof trees while in
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana GenericATP window otherwise "Exit prover" takes a long time
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Example: seq (length $ show $ prooftree proofStatus) proofStatus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanausability improvements
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - forceFocus to read-only textedit widgets in textSaveDisplay windows
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana upon left mouse click
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana also add for Details window
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana - update of goal list-boxes should not longer move visible
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana area of the list
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana involves getting and setting of visible area
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacode cleanup and documentation where necessary and possilbe
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana in SPASS/* and GUI/GenericATP*, GUI/Proofmanagement.hs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafor ProofManagement-GUI
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana mark imported theorems for selection
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana extend Logic.Prover SenStatus with wasTheorem
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana somewhere in computeTheory implement setting of wasTheorem
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana if wasTheorem not appears with right status in ProofManagementGUI
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana add wasTheorem to Common.Result.Named, as well
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana and adapt conversion functions of SenStatus to Named and vice
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Mark old theorems in "Axioms to include" Listbox with prefixed
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana add button "Deselect former Theorems"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana test all this with CASL-lib/Calculi/Space/RCCVerification.het
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana all nodes without incoming heterogeneous edges are provable with
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafor ProofManagement-GUI
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana provide structured (based on spec-names) selection/deselection facility
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana of axioms and theorems
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatrace if liniarity of sentences along development is given
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafor consistency checking with Isabelle, look at the following SAT-Solvers:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaMChaff, ZChaff, Berkmin
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaConsistency checker interface
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana via global interface, accessible from global and node menus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana use falseSentence from Logic.Logic (property: holds in no model)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana proved -> inconsistent
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana disproved -> consistent (assuming completeness)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana batch mode for automatic provers such as SPASS
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (use automatic flag for provers)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanabatch interface for Isabelle
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana each goal is proved separatedly, with a time limit enforced
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana by killing the process
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana "using Ax1 ... Axn by auto"
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana where Ax1 ... Axn is the list of all axioms.
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana "auto" could be replaced with "best", "blast" etc. (user selection)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIgnore axiom selection for interactive provers
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaTranslation between Achim's ontology data structure and CASL (in Hets)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanavisualization of "taxonomy" of CASL signatures
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (subsorts = inheritance, unary preds = concepts, binary preds = relations)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana last two ... partially done
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRecognize guarded fragment of CASL:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana G ::= forall x . At(x) => G where At is a conjunction of atoms
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana | exists x . At(x) /\ G
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaJoost Visser wg. ATerms in Haskell => neues Repository
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaBeweise in Isabelle
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCASL consistency checker
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaWeitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (Vorbild: Larch-Handbuch)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaSimpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaParser and static analysis for CSP-CASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCASL consistency checker
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIntegration with generic prover interface?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaduplicate referenced node in SimpleDatatypes.casl
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaenhance Web interface with SPASS (%implied, consistency)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatranslation of proofs along comorphisms (it this necessary at all???)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana use inverse morphism?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana leads to translation of G_theory along comorphism that also
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana keeps proof status info
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana this may be used in GUI prover interfaces for recovering old proof attempts
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana and offering them as default
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaproveCMDLinteractive (PGIP)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaModel expansion flag for comorphisms
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaUmlaute in daVinci anzeigen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaFragen an Michael:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanawerden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana was ist dort eigentlich das Problem?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCodierung von Subsorten?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanapaper with Paolo
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana semantic adequecy of HOL translation
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRegulate concurrent proving
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana.dg files: store only current library; import .dg files for other libraries
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIsabelle: use meta-quantifiers
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanalocal subsumption ?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanabetter syntax (Tina)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacheck for proved theorems
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAbstractGraphView: switch to Result monad
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaunite or rename consCheck and cons_checkers
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaBinInt.casl: revealing in Int1 does not work correctly
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafrom Stefan W�lfl:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanacomputeTheory does not work across library imports
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaall nodes named
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanahierarchical Isabelle theories
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanadaVinci printing is not adequate
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanahiding of internal nodes does not work
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaFOL without quantifiers and with uniform disjunctions
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (i.e. x R1 y \/ x R2 y)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (with and without =)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaalgorithmic path consistency over a relation algebra
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana plug in reasoner for this
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana develop correctness results (algorithmic path consistency=path consistency)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCASL sublogics:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana---------------
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaFOL without quantifiers (with and without =)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaguarded fragment
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana[from DOLCE cooperation:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaontology mediation via pushouts/pullbacks/pulations
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRobinson consistency with shared theory constructed via pre-image?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanashow theorem links between same instances of different parameterized
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana specs (where one is an extension of the other one)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanalink menu for %implies, $def, %cons, even without open proof obligation
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafor a proved theorem, show minimal part of DG needed for proof
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacons, def, mono for nodes
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIsabelle interface: each qed should write proof info into file
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaglobally display nodes containing symbols mapped "twice" (i.e. via
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana different signature morphisms)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana and add a menu for each node allowing for tracking the different
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatopsort coding: partial functions as relations?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatheorem link menu for proof obligations
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaUserManual/Chapter7.casl: local thm link starting from Monoid leads to type error
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanain Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaBuffer.het, sublogic of node Buffer:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaFail: illegal node type in sublogic computation
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaJ�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafor CSP-CASL example: with logic
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaheterogeneous static ana
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatheorem links between nodes in different libraries
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanabasicProofs: use info about used axioms
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ensure that axiom/thm names are unique
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaOverload / inlineAxioms: injections
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaremove "prove" menu in abstracted dg
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanabetter sublogic analysis in codings
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanathy files in subdir
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaadjust path for thy files, such that hets can also be started from subdirs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRestrict Sonjas simplifications to HasCASL
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaadd suitable axioms to simplifier and CR
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanacomputeTheory: remove double axioms
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaadd suitable axioms to simplifier and classical reasoner
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanabetter display of internal nodes (use tooltip?)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaupdate Hets, CASL, daVinci on web page
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanapacking of binaries: add hets-update, refer to TclTk
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanatest for sublogic before applying comorphism
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaMissing points for heterogeneous WADT 04 example:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- coding to Isabelle: translate sort gen constraints
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- Improve adapation to Isabelle's lexis
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIsabelle: (ask Christoph)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana remove datatypes from sort list
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana prove local thm link (=> green)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana "prove" menu with choice windows
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana incorporate sublogics
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana sublogic translation table
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana better interaction between Isabelle instance (for one node)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana + selection of single goals that are proved
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana => use PGIP interface (Christoph, David)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana correct show theory
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Keep proofs and lemmas in .thy files (kind of merge)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana CASL-like syntax
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana CASL annotation for lemmas that should be used in proof
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana inherit CASL's mixfix syntax
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaSignatures versus theories: where to store additional infos?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanacomp(id,x)=x for comorphism names
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaGeneralise CASL2Modal
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaMixfix analysis + typecheck for modality axiomatizations
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaModal logics: modal logic, temporal logic, mu calculus
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana+ translations (e.g. modal to FOL)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaCASL->Haskell with free DTs (mark sortgens) + recursion
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- List[Dec] wird List[Pos]
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- node numbers do not match
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana- thm links with external target should be provable as well
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRemove warnings
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaDifferent types of logic translations
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaImprove Static analysis of structured specs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaDevelopment graph calculus, Strategies for DG rules
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana use graph grammars to model rules? transformation units?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaManagement of change
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIntegrate provers
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Otter model checker
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana FOL-prover by Uli Furhbach
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Isabelle codings: www.inf.ethz.ch/~vigano
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Renate Schmidt, Manchester: uses FOL prover for description logic
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (as efficient as DL-specific tools!)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Look at PROSPER toolkit
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana consistency: see IJCAR-workshop on non-provability in Cork
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana IJCAR workshop about logical frameworks and meta-languages
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaKlaus' wayfinding example
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaask Detlef: critical pairs, Fossacs paper by Francesco
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaUniForM workbench:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanafirst steps towards CASL instance, using ATerms and re-using MMISS instance
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanavariants for specs (needed for DOLCE: CASL variant, DL variant, ...)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIntegration of MAYA and Isabelle/HOL (global HOL-Coding of
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Grothendieck logic)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana + for TAS: reflection of HOL in HOL, to be composed with encodings
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana (i.e. signatures, axioms, signature morphisms in HOL,
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana re-use ML signatures) (Einar)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaDisplay Specs as daVinci subgraphs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaLogic graph window
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaInput text window
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaDevelopment graph window
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana************************************************
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHets 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)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaPackaging of installation
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana with Eclipse, WXHaskell or GTk?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana how to integrate with event system of UniForM workbench?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaintegrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana this interacts with GUI!
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaData.Serizable (only when ghc supports it) better: rely on pointer equality
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaincrease performance
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanaintegrate QuickCheck: come to lecture!
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana++++++++++++++++++++++++++++++++++++++++++++++++
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRemaining things
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana++++++++++++++++++++++++++++++++++++++++++++++++
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaMark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana Coq, PTT in Maude
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaProofs with basic datatypes
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaVerbesserung der Fehlermeldungen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaImprove encoding: CATS/basic_encode.sml (3 days)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaMore HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRenamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaExample of Agnes und Frank: proofs in HOL-CASL (2 days)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaTerm input+errors in cmd line interface: CATS/casl/casl.sml (1 day)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaExamples for cond rewriting -> Christophe
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaDoku: VSE-Prover, VSE-Method VSE-demo in Bremen?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAdapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaEigene IsaWin-Instanz mit CASL-RS statt HOL-RS
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaEncoding of structured free (3 days)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaEncoding of structured cofree (2 weeks)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaEingabesyntax als Mix zwischen CASL und HOL (3 days)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAdapt Isabelle unions to CASL unions (1 week)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaIsaWin git/src/isa_ext/casl_thy.sml (1 week)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaGenerate Proof obligations (1 week)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAdd renaming to Isabelle kernel (2 months)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaBasic datatypes CASL-lib/Basic/basic.casl
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaRepository mit korrekten und fehlerhaften Specs
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaHetCATS User manual, Doku fuer Environments (2 weeks)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaConversion ASF/SDF-Parser -> abstract syntax (in Haskell)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaComparsion of parsers (ML-yacc parser, SDF-Parser)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaConversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaPVS anbinden (Kooperation mit Cachan?)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaPortations: Intel-Solaris, Mac OS-10 (2 weeks)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaViews on CASL specs: CATS/viewer.sml (2 weeks)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaUebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaModule graph CATS/module_graph.sml (1 week) -> Maya?
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaATerms via XML: CATS/aterms.sml (2 weeks)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaNeues Tool-Schaubild auf Web-Seiten ver�ffentlichen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaLibrary management: CATS/lib_ana.sml (2 weeks)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaVersion management/Uniform Workbench: CATS/lib_ana.sml (2 months)
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana{- This does not work due to needed ordering:
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanainstance Functor Set where
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushanainstance Monad Set where
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana return = unitSet
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana m >>= k = unionManySets (setToList (fmap k m))
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAufbau von comptable
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana--------------------
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana[("normal","normal","normal"),
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ("normal","inclusion","normal"),
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ("inclusion","normal","normal"),
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana ("inclusion","inclusion","inclusion")]
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAufbau von ginfo
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana--------------------
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaMit initgraphs erzeugen
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh NagabhushanaAufbau des Graphen selbst
56b2bdd1f04d465cfe4a95b88ae5cba5884154e4Gireesh Nagabhushana------------------------