144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiPlan and priority list for CoFI tool activities

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiImmanuel

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiSuchfunktion f�r einen Knoten im DG:

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski erstmal auf eine Logik (z.B. CASL) beschr�nken

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - Funktion f�r Morphismus-Suche zwischen Theorien

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski RawSymbolMap als "Suche-Guide" wird erestzt durch Axiome/Theoreme

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski - Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKonfidenzgrade von Beweisen?

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskivon Till/HiWi zu erledigen:

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiRepr�sentation �ndern:

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Beweisobjekte an DGs, nicht an Regeln -- done

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski F�r Theoreme in Theorien an Beweisobjekte -- done

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski BasicProof mit Liste von Beweisobjekten -- �berfl�ssig

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Definitionen auszeichnen -- done

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski F�r alles siehe G_theory, ThSens und SenStatus.

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Isabelles Beweisobjekte einbinden

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

38f30f746aa42d4fc659a15e183801f2f74596d0Till MossakowskiRazvan (Till)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

ed892c579cca270fff0aa9cc2a34351c420e3182Till MossakowskiIntegration with PGIP

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski Hets needs to be equipped with a command-line interface that reads in

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski specification libraries and proof commands

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski Proof commands are special annotations in the libraries

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski All menu commands of the development graph interface (GUI/...) should become (proof) commands

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski when stepping through the specs, dg calculus generates proof obligations

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski (for the current dg node only),

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski which then can be discharged by Isabelle, SPASS etc.

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski That is, the proof commands always occur at the position in the text

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski that generates the dg node?!? or should they occur after each specification?

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski needs incremental parsing and static analysis for Hets libraries

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski easy: parse and analyse one specification at a time, and then process it with proof commands

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski more challenging: incrementally parse and analyse also individual specifications

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski************************************************

ed892c579cca270fff0aa9cc2a34351c420e3182Till MossakowskiAnton (Till)

ed892c579cca270fff0aa9cc2a34351c420e3182Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiModal-CASL <-> CASL-DL

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski see Chapter 4 of "The Description Logic Handbook"

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski and ask Klaus for a print out of it

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiimprove Modal-CASL

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski possibly also modal logic in CoCASL

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski**************** task A ************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiProofs with Isabelle and SPASS

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiCASL basic datatypes

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHasCASL examples

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- improve simplifier for partiality in Isabelle coding

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski program interaction between solver, subgoaler and simplifier in such a way

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski that proofs of definedness conditions are postponed

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFlorian (Till)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiBremer Constraint-Solver angucken

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiShi Hui wegen Anwendungen kontaktieren 1. Juni

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLiteratur �ber DCC und RCC8 lesen bis Mitte Juni

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMitte/Ende Juni: Outline der Diplomarbeit

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski�bersetzungen bis 30.Juni

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski ConstraintCASL -> Bremer Solver

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski CASL/ComputeTable

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Bremer Solver -> ConstraintCASL

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Parser (mit Parsec), der Kompositionstabelle des Bremer Solvers

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski parsiert und ConstraintCASL-Spec (abstrakte Syntax) zur�ckgibt

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Das kann das als Option in Hets eingebunden werden (Christian Maeder)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFreiburger Constraint-Solver angucken im Juli

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski�bersetzungen bis 31. Juli

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski ConstraintCASL -> Freibuger Solver/XML-Format

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski CASL/ComputeTable

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Option: comptable.xml

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Freibuger Solver/XML-Format -> ConstraintCASL

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHendrik (Till)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiwerden Signatur-Symbole in OMDoc mit der Theorie versehen, in der

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski sie als erstes eingef�hrt wurden?

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski checken f�r Library-Importe

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiOMDoc/OpenMath-Formeln als Haskell-Datentyp formulieren; diesen als Zwischendatentyp verwenden

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHiding: unterschiedlich in OMDoc und Hets

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiein Hets-Hiding-Link mit einer Inklusion Sigma_1->Sigma_2 als

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Signaturmorphismus

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski wird �bersetzt in einen OMDoc-Theoriemorphismus

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski mit leerer/identischer Abbildung, bei dem die Symbole aus

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Sigma_2 \ Sigma_1 versteckt werden

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Wenn der Signaturmorphismus keine Inklusion ist, ist keine

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski �bersetzung m�glich -> Fehler

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiein OMDoc-Theoriemorphismus mit Hiding, der eine Inklusion ist

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (also leere bzw. identische Abbildung) wird �bersetzt

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski in einen Hets-Hiding-Link, mit Inklusion als Signaturmorphismus

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski falls der OMDoc-Theoriemorphismus keine Inklusion ist, muss

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski ein Hets-Hiding-Link, gefolgt von einem normalen (globalen) Link,

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski der dann die Umbenennung macht, erzeugt werden

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiLogiken: �ber verschiedene OMDoc-Theorien mit URI

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiMingyi (Till)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiport CCC to Haskell

e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiFunktionen imageOfMorphism und inhabited

e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski mit "cvs add SigFuns.hs" einchecken

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiNew module FreeTypes.hs:

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski"free datatypes and recursive equations are consistent"

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskicheckFreeType :: Morphism f e m -> [FORMULA f] -> Maybe Bool

e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskiJust True => Yes, is consistent

e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskiJust False => No, is inconsistent

e539b8cb4a47f987bc57c90ee964219ac53841ffTill MossakowskiNothing => don't know

e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski

e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowskicall the symbols in the image of the signature morphism "new"

e539b8cb4a47f987bc57c90ee964219ac53841ffTill Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- each new sort must be a free type,

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski i.e. it must occur in a sort generation constraint that is marked as free

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (Sort_gen_ax constrs True)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski such that the sort is in srts, where (srts,ops,_)=recover_Sort_gen_ax constrs

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski if not, output "don't know"

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski and there must be one term of that sort (inhabited)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski if not, output "no"

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski- group the axioms according to their leading operation/predicate symbol,

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski i.e. the f resp. the p in

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t

f69658e57cba7ecb37c0d84181f4c563215c2534Till Mossakowski forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Implication Application Strong_equation

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski forall x_1:s_n .... x_n:s_n . p(t_1,...,t_m)<=>phi

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Implication Predication Equivalence

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski if there are axioms not being of this form, output "don't know"

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck' [] = ([([],[])],emptyUniqSet)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-- nur ein Pattern, bestehend aus nur Variablen? fertig, True

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck' [EqnInfo n ctx ps (MatchResult CanFail _)]

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-- besteht das erste Pattern nur aus Variablen? dann darf es kein zweites geben!

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | all_vars ps = (pats, addOneToUniqSet indexs n)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski where

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (pats,indexs) = check' rs

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-- falls ein Konstruktor dabei ist: split_by_constructor

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski-- wenn die ersten Argument nur Variablen sind: first_column_only_vars

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskicheck' qs@((EqnInfo n ctx ps result):_)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | all_vars ps = ([], unitUniqSet n)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | constructors = split_by_constructor qs

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | only_vars = first_column_only_vars qs

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski | otherwise = panic "Check.check': Not implemented :-("

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski where

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski -- Note: RecPats will have been simplified to ConPats

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski -- at this stage.

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski constructors = or (map is_con qs)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski only_vars = and (map is_var qs)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskisubsort definitions: are conservative if formula is satisfiable

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski (generate proof obligation)

38f30f746aa42d4fc659a15e183801f2f74596d0Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiHeng (Klaus)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiOWL-DL logic

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiOWL-DL (<)-> CASL-DL

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiemacs mode:

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski highlight does not work properly for HasCASL/Set.het or UserManual/Sbcs.casl

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski some operation symbols

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski show hets output immediately

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski C-c C-g for hets -g

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski when hets terminates abnormally (e.g. with a fail), emacs loops

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski C-n jumps to the next error, but the message windows is not always scrolled

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski in such a way that the error is at the top (for long error lists)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Version for XEamcs?

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski should work with parser error messages as well (adapt these?)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiKen (Till)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskidevelopment graph calculus

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(see Sect. IV:4.4 of the CASL Reference Manual)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilook at Static/DevGraph.hs

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilook at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifix bug: when lodaing Basic/RelationsAndOrders.casl and

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski doing 4x edit - proofs - Global Decomposition, we get

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski hets: applyChangesAux2: deleted edge from 3 to 15 of type GlobalThm

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski and origin DGProof of development graph does not exist in abstraction graph

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski look at Proofs/Global.hs, GUI/ConvertAbstractToDevgraph,

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski function applyChanges

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski Hint: first try to cut down the example (find out the minimal

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski subpart that still leads to the error)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitest development grapg GUI:

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski menu edit - unnamed nodes - hide/show nodes,

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski node menu: show just subtree / undo

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski interaction with edit - proofs - automatic?

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiimplement simplified rule Theorem-Hide-Shift

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskitry out examples

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiconservativity calculus

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiweakly amalgamable cocones

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifurther task 1

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifurther task 2

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till MossakowskiUni-Refactoring,

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskimake modules hierarchical, change scoped type variables for ghc-6.5

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(and older ghcs), replace deprecated code (i.e. FiniteMap, hslibs),

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskiuse HaXml as a cabalized library, provide uni as (one?) cabal

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipackage(s), uni used to work under windows as well, watch the

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskii.e. FilePath, Process discussions (libraries@haskell.org)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskipossibly switch to a subversion repository, talk to Achim

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski(amahnke@tzi.de)

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskifurther task 3

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowski************************************************

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilook fgl/Data/Graph/Inductive/Graph.hs

144d4893ba5a3815bd1639d498ee4a20ed13a211Till Mossakowskilook at Static/DevGraph.hs

change management

reload button im Edit-Men� hinzuf�gen (GUI/ConvertAbstractToDevgraph.hs)

reload macht folgendes:

lade CASL-Datei neu ==> neuer Entwicklungsgraph

vergleiche alten+neuen Entwicklungsgraph, konstruiere eine

Abbildung (Common/Lib/Map.hs) von alt nach neu

(jeweils eine Abblidung f�r Knoten und eine f�r Kanten)

Kriterien f�r Finden der Knotenabbildung:

- Namen

- DGOrigin

- Signatur

einfaches Merge von lokalen Beweisen eines abgespeichteren DG

in aktuellen DG

************************************************

further task 4

************************************************

graph of Haskell module dependencies

using .import files

************************************************

further task 5

************************************************

port hets to windows. -- costs too much energy at this stage! Till

If hets should become successful then requests for support under

windows will surely follow.

Ghc, uni and uDrawGraph should work under windows. Only Isabelle does

not exist for windows, but SPASS does. Probably only a few path

computations need to be adapted (made modular) within hets. Also

position computations (of Parsec) should be checked under windows.

************************************************

further task 6

************************************************

refactor pretty printing

eine HetCASL spezifische PP Lib (mit neuem Doc Typ), um Text, Latex

und andere Formate besser zu unterst�tzen und einheitlichen PP code

(independent from GlobalAnnos) f�r die (Het-)CASL (and HasCASL!)

Datentypen (particularly for HasCASL data types) zu bekommen.

LaTeX: see listings.sty for LaTeX generation (cf. CoSiT paper)

************************************************

remaining stuff

************************************************

set up a ticket and tracking systems (for bugs and features) instead

of this messy todo list

--> sourceforge???

refactoring of dgraphs: add unique tags + hashes (but no table)

how to compare complex datastructures:

tag x1==tag x2 || (hash x1==hash x2 && x1==x2)

display library graph

unify GUI/AbstractGraphView.hs and Taxonomy/AbstractGraphView.hs

and uni/appl/ontologytool/AbstractGraphView.hs

(make it really abstract), possibly contact amahnke@tzi.de regarding

Taxonomy, possibly use uni/appl/ontologytool instead of Taxonomy!

set up default simplifier

set up default tactics using axioms

(see DOLCE sample files)

improve efficiency (e.g. of UserManual/Sbcs.casl), using profiling

************************************************

Daniel

************************************************

generate infrastructure for circular coinduction

CCS example: commutativity of || by coinduction

************************************************

Christian

************************************************

Isabelle coding

- improve display syntax in HasCASL-Isabelle coding

- correct CASL2Isabelle

(inconsistency due to coding of free datatypes)

more abstract datatypes?

collect the patches for programatica (or create a package)

- conv (SN i p) = PN i (S p)

+ conv (SN i p) = PN i (Sn (show i) p)

in programatica/tools/base/parse2/NumberNames.hs

fixes translation error of Pair

simplification of HasCASL sentences (omit types)

Logic COL is a ruin (with wrongly qualified module names)

logic coding from the comand line with printing of results

Haskell modules: hiding, renaming

- group the axioms according to their leading operation/predicate symbol,

i.e. the f resp. the p in

forall x_1:s_n .... x_n:s_n . phi => f(t_1,...,t_m)=t

forall x_1:s_n .... x_n:s_n . phi1 => p(t_1,...,t_m)<=>phi

if there are axioms not being of this form, output error

Static analysis for HasCASL

pattern analysis for program equations

implemented only atomic subtyping

Weak amalgamation analysis?

Instantiate Transformation Application system for HasCASL?

Automatic generation of Haskell (for a HasCASL subset)

Proofs in HasCASL

Case study

Coding HasCASL -> Isabelle with definedness axioms

only strict functions are defined

Isabelle interface

One emacs with spec and proof buffer

Reload button should rebuild buffers while keeping as much as possible

keep structuring of Hets theories

************************************************

Rainer (Klaus)

************************************************

Connecting Hets with MathServ

Either use

- haifa (http://www.dcs.shef.ac.uk/~simonf/HAIFA.html)

pros: * relies not on external tool

* light weight call

cons: * code is not well maintained

* a lot of the deserialization of the answer must be done

in Haskell

- call a java program included in MathServ distrib

pros: * works imediately

* deserilisation is mostly done in java

cons: * use of external tool

Use modified dfg2tptp to translate SPASS theories into TPTP problems

(ask Klaus for sources)

Add possibility to choose a prover out of a list of available provers

(similar to "More fine grained..." and behind more fine grained)

Adapt Comorphisms.KnownProvers to select a certain prover at the end of a

comorphism automatically

Adapt existing SPASS GUI to cover call of the MathServ broker

by - transforming the grid layout packer into the packer

used in GUI.ProofManagement (easier to maintain and to extend)

- abstraction of certain parts of the GUI into helper functions

forms a new generic Prover-GUI toolkit

- on top of this GUI toolkit

Write a GUI based on the generic Prover-GUI

to call MathServ's Vampire service directly

with additional parameters

************************************************

Klaus

************************************************

for consistency checking with Isabelle, look at the following SAT-Solvers:

MChaff, ZChaff, Berkmin

Consistency checker interface

via global interface, accessible from global and node menus

use falseSentence from Logic.Logic (property: holds in no model)

proved -> inconsistent

disproved -> consistent (assuming completeness)

batch mode for automatic provers such as SPASS

(use automatic flag for provers)

batch interface for Isabelle

each goal is proved separatedly, with a time limit enforced

by killing the process

the tactic is

"using Ax1 ... Axn by auto"

where Ax1 ... Axn is the list of all axioms.

"auto" could be replaced with "best", "blast" etc. (user selection)

Ignore axiom selection for interactive provers

Translation between Achim's ontology data structure and CASL (in Hets)

visualization of "taxonomy" of CASL signatures

(subsorts = inheritance, unary preds = concepts, binary preds = relations)

last two ... partially done

allgemeine Hets-GUI

f�r Anzeige von (un)bewiesenen Goals, ... done

bewiesene Goals als Axioms mit ausgeben ... was ist das ???

das ist schon implementiert ("Theorems to include if proven")

Recognize guarded fragment of CASL:

G ::= forall x . At(x) => G where At is a conjunction of atoms

| exists x . At(x) /\ G

Joost Visser wg. ATerms in Haskell => neues Repository

************************************************

Markus, Lutz

************************************************

Beweise in Isabelle

CASL consistency checker

Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen

(Vorbild: Larch-Handbuch)

Simpsets/Taktiken fuer Minimierung der ueberladenen Typen entwickeln

Parser and static analysis for CSP-CASL

************************************************

Christoph

************************************************

CASL consistency checker

Integration with generic prover interface?

************************************************

Till

************************************************

Fragen an Michael:

werden Links in der richtigen Reihenfolge geschrieben (S. 183 OMDoc)?

was ist dort eigentlich das Problem?

Codierung von Subsorten?

paper with Paolo

semantic adequecy of HOL translation

Regulate concurrent proving

.dg files: store only current library; import .dg files for other libraries

Markus' Bsp:

Isabelle: use meta-quantifiers

local subsumption ?

better syntax (Tina)

check for proved theorems

AbstractGraphView: switch to Result monad

unite or rename consCheck and cons_checkers

BinInt.casl: revealing in Int1 does not work correctly

from Stefan W�lfl:

computeTheory does not work across library imports

local theorems

all nodes named

hierarchical Isabelle theories

daVinci printing is not adequate

hiding of internal nodes does not work

CSPs

----

FOL without quantifiers and with uniform disjunctions

(i.e. x R1 y \/ x R2 y)

(with and without =)

algorithmic path consistency over a relation algebra

plug in reasoner for this

develop correctness results (algorithmic path consistency=path consistency)

within CASL

CASL sublogics:

---------------

FOL without quantifiers (with and without =)

guarded fragment

Prop

[from DOLCE cooperation:

quit wish!

ontology mediation via pushouts/pullbacks/pulations

Robinson consistency with shared theory constructed via pre-image?

show theorem links between same instances of different parameterized

specs (where one is an extension of the other one)

link menu for %implies, $def, %cons, even without open proof obligation

for a proved theorem, show minimal part of DG needed for proof

cons, def, mono for nodes

Isabelle interface: each qed should write proof info into file

globally display nodes containing symbols mapped "twice" (i.e. via

different signature morphisms)

and add a menu for each node allowing for tracking the different

uses of the symbols/concepts

topsort coding: partial functions as relations?

]

theorem link menu for proof obligations

UserManual/Chapter7.casl: local thm link starting from Monoid leads to type error

in Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms

correctly.

Buffer.het, sublogic of node Buffer:

Fail: illegal node type in sublogic computation

J�rgen Zimmer, Saarbr�cken+Edinburgh, Beweiserkennung f�r versch. Logiken im MathWeb

for CSP-CASL example: with logic

heterogeneous static ana

theorem links between nodes in different libraries

basicProofs: use info about used axioms

ensure that axiom/thm names are unique

Overload / inlineAxioms: injections

remove "prove" menu in abstracted dg

better sublogic analysis in codings

thy files in subdir

adjust path for thy files, such that hets can also be started from subdirs

Restrict Sonjas simplifications to HasCASL

add suitable axioms to simplifier and CR

computeTheory: remove double axioms

add suitable axioms to simplifier and classical reasoner

better display of internal nodes (use tooltip?)

update Hets, CASL, daVinci on web page

CASL2PCFOL: x_i -> t_i, t=[inj(x_i)] (and what not!)

packing of binaries: add hets-update, refer to TclTk

CCC interface

test for sublogic before applying comorphism

Missing points for heterogeneous WADT 04 example:

- coding to Isabelle: translate sort gen constraints

- Improve adapation to Isabelle's lexis

Isabelle: (ask Christoph)

remove datatypes from sort list

prove local thm link (=> green)

"prove" menu with choice windows

incorporate sublogics

sublogic translation table

better interaction between Isabelle instance (for one node)

+ selection of single goals that are proved

=> use PGIP interface (Christoph, David)

correct show theory

Keep proofs and lemmas in .thy files (kind of merge)

CASL-like syntax

CASL annotation for lemmas that should be used in proof

inherit CASL's mixfix syntax

Signatures versus theories: where to store additional infos?

comp(id,x)=x for comorphism names

Generalise CASL2Modal

Mixfix analysis + typecheck for modality axiomatizations

Modal logics: modal logic, temporal logic, mu calculus

+ translations (e.g. modal to FOL)

CASL->Haskell with free DTs (mark sortgens) + recursion

- List[Dec] wird List[Pos]

- node numbers do not match

- thm links with external target should be provable as well

Remove warnings

Different types of logic translations

Improve Static analysis of structured specs

Development graph calculus, Strategies for DG rules

use graph grammars to model rules? transformation units?

Management of change

Integrate provers

Otter model checker

FOL-prover by Uli Furhbach

modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig

Isabelle codings: www.inf.ethz.ch/~vigano

Renate Schmidt, Manchester: uses FOL prover for description logic

(as efficient as DL-specific tools!)

Look at PROSPER toolkit

consistency: see IJCAR-workshop on non-provability in Cork

IJCAR workshop about logical frameworks and meta-languages

Integrate CCC

Encodings

Errors:

Klaus' wayfinding example

ask Detlef: critical pairs, Fossacs paper by Francesco

UniForM workbench:

first steps towards CASL instance, using ATerms and re-using MMISS instance

variants for specs (needed for DOLCE: CASL variant, DL variant, ...)

Integration of MAYA and Isabelle/HOL (global HOL-Coding of

Grothendieck logic)

+ for TAS: reflection of HOL in HOL, to be composed with encodings

(i.e. signatures, axioms, signature morphisms in HOL,

re-use ML signatures) (Einar)

Display Specs as daVinci subgraphs

User interface

--------------

Logic graph window

Input text window

Development graph window

Prover windows

************************************************

FOR STUDENTS

************************************************

Hets interactive (provide cmd line interface, but hold loaded libraries in memory, provide switch to context of spec, and type checking of expressions, interaction with emacs mode)

Packaging of installation

GUI (vgl. VSE)

with Eclipse, WXHaskell or GTk?

how to integrate with event system of UniForM workbench?

integrate graphviz (or use Java interface for racer? or Isabelle browser? or...?)

this interacts with GUI!

Data.Serizable (only when ghc supports it) better: rely on pointer equality

XML interface

increase performance

integrate QuickCheck: come to lecture!

++++++++++++++++++++++++++++++++++++++++++++++++

Remaining things

++++++++++++++++++++++++++++++++++++++++++++++++

Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude

Coq, PTT in Maude

Proofs with basic datatypes

Verbesserung der Fehlermeldungen

Improve encoding: CATS/basic_encode.sml (3 days)

More HOL-theories: CATS/HOL-CASL/struct_encode.sml (2 days)

Renamings in hide-elimination: CATS/struct_encode.sml, CATS//flatten.sml (1 week)

Example of Agnes und Frank: proofs in HOL-CASL (2 days)

Term input+errors in cmd line interface: CATS/casl/casl.sml (1 day)

Examples for cond rewriting -> Christophe

Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?

Adapt more stuff from isabelle/src/HOL/Tools/datatype_package.ML (2 weeks)

Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS

HOL-CASL Simplifier: CATS/HOL-CASL/simplifier.sml (1 week)

HOL-CASL tactics: CATS/HOL-CALS/tactic.sml (2 days)

HOL-CASL encoding: CATS/HOL-CASL/basic_encode.sml (1 day)

Encoding of structured free (3 days)

Encoding of structured cofree (2 weeks)

Eingabesyntax als Mix zwischen CASL und HOL (3 days)

Adapt Isabelle unions to CASL unions (1 week)

IsaWin git/src/isa_ext/casl_thy.sml (1 week)

Generate Proof obligations (1 week)

Add renaming to Isabelle kernel (2 months)

Basic datatypes CASL-lib/Basic/basic.casl

Repository mit korrekten und fehlerhaften Specs

HetCATS User manual, Doku fuer Environments (2 weeks)

Conversion ASF/SDF-Parser -> abstract syntax (in Haskell)

Comparsion of parsers (ML-yacc parser, SDF-Parser)

Conversion-Tool CASL 1.0 => CASL 1.0.1 komplettieren

PVS anbinden (Kooperation mit Cachan?)

Portations: Intel-Solaris, Mac OS-10 (2 weeks)

(X)Emacs mode for CASL, hide Display Annotations (2 weeks) -> Raffael Sturm

Views on CASL specs: CATS/viewer.sml (2 weeks)

Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII

Module graph CATS/module_graph.sml (1 week) -> Maya?

ATerms via XML: CATS/aterms.sml (2 weeks)

Neues Tool-Schaubild auf Web-Seiten ver�ffentlichen

Library management: CATS/lib_ana.sml (2 weeks)

Version management/Uniform Workbench: CATS/lib_ana.sml (2 months)

{- This does not work due to needed ordering:

instance Functor Set where

fmap = mapSet

instance Monad Set where

return = unitSet

m >>= k = unionManySets (setToList (fmap k m))

-}

Aufbau von comptable

--------------------

[("normal","normal","normal"),

("normal","inclusion","normal"),

("inclusion","normal","normal"),

("inclusion","inclusion","inclusion")]

Aufbau von ginfo

--------------------

Mit initgraphs erzeugen

Aufbau des Graphen selbst

------------------------

addnode

addlink