fa9e4066f08beec538e775443c5be79dd423fcabahrensPlan and priority list for CoFI tool activities

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg************************************************

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jgSonja (Till)

fa9e4066f08beec538e775443c5be79dd423fcabahrens************************************************

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensDiplom: Encoding for HasCASL in Isabelle/HOL(CF)

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensInterface Hets <-> ISabelle

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensin IsaProve.hs

fa9e4066f08beec538e775443c5be79dd423fcabahrens Hets muss eine Pipe als Inode erzeugen

fa9e4066f08beec538e775443c5be79dd423fcabahrens und dann auf Beweisterme warten

fa9e4066f08beec538e775443c5be79dd423fcabahrens und auf "Ende" warten

fa9e4066f08beec538e775443c5be79dd423fcabahrens und dann Proof_status sen proof_tree entsprechend ausf�llen

fa9e4066f08beec538e775443c5be79dd423fcabahrens (siehe Logic/Prover.hs)

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensIsabelle (im .thy file, dass von IsaProve.hs erzeugt wird)

fa9e4066f08beec538e775443c5be79dd423fcabahrens Beweisterme (siehe Kapitel im RefMan)

97322426b5359bb3ffd4527e1ad8b2c5f7dab832Darren J Moffat ML "proofs := 1" (am Anfang des .thy file)

fa9e4066f08beec538e775443c5be79dd423fcabahrens am Ende jedes Theorems: Beweisterm in die Pipe schreiben

fa9e4066f08beec538e775443c5be79dd423fcabahrens (Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)

fa9e4066f08beec538e775443c5be79dd423fcabahrens mit pretty_proof_of und Pretty.string_of

fa9e4066f08beec538e775443c5be79dd423fcabahrens und Start- und Endmarker

45818ee124adeaaf947698996b4f4c722afc6d1fMatthew Ahrens am Schluss "Ende" ausgeben

45818ee124adeaaf947698996b4f4c722afc6d1fMatthew Ahrens

45818ee124adeaaf947698996b4f4c722afc6d1fMatthew Ahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensFunktion basicInferenceNode in Proofs/Proofs.hs:

fa9e4066f08beec538e775443c5be79dd423fcabahrens Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensEmacs: uni/emacs, George fragen (ger@)

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens************************************************

fa9e4066f08beec538e775443c5be79dd423fcabahrensJorina (Till)

fa9e4066f08beec538e775443c5be79dd423fcabahrens************************************************

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensdevelopment graph calculus

fa9e4066f08beec538e775443c5be79dd423fcabahrens- Stack overflow for "show just subtree"

fa9e4066f08beec538e775443c5be79dd423fcabahrens- view-test7.casl should be provable with globDecomp + locDecopm

fa9e4066f08beec538e775443c5be79dd423fcabahrens- fail when doing first globDecomp, then local decomp in RelationsAndOrders

fa9e4066f08beec538e775443c5be79dd423fcabahrens- correct MAYA: glob decomp: some links are not found (Jorina)

fa9e4066f08beec538e775443c5be79dd423fcabahrens- Fail: No match in record selector Static.DevGraph.dgn_sign

fa9e4066f08beec538e775443c5be79dd423fcabahrens for local subsume in RelationsAndOrders

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens************************************************

fa9e4066f08beec538e775443c5be79dd423fcabahrensMartin (Till)

fa9e4066f08beec538e775443c5be79dd423fcabahrens************************************************

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrenstype check for CASL

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensdocumentation

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens*** Error encode.casl:8.30, No correct typing for

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens************************************************

fa9e4066f08beec538e775443c5be79dd423fcabahrensMingyi (Till)

fa9e4066f08beec538e775443c5be79dd423fcabahrens************************************************

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensport CCC to Haskell

fa9e4066f08beec538e775443c5be79dd423fcabahrens

45818ee124adeaaf947698996b4f4c722afc6d1fMatthew AhrensFunktionen imageOfMorphism und inhabited

45818ee124adeaaf947698996b4f4c722afc6d1fMatthew Ahrens von OnePoint.hs in eigenes Modul verschieben: Modul SignFuns.hs

fa9e4066f08beec538e775443c5be79dd423fcabahrens mit "cvs add SigFuns.hs" einchecken

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrensNew module FreeTypes.hs:

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens"free datatypes and recursive equations are consistent"

fa9e4066f08beec538e775443c5be79dd423fcabahrens

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

fa9e4066f08beec538e775443c5be79dd423fcabahrensJust True => Yes, is consistent

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jgJust False => No, is inconsistent

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jgNothing => don't know

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jgcall the symbols in the image of the signature morphism "new"

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg- each new sort must be a free type,

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

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg (Sort_gen_ax constrs True)

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

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg if not, output "don't know"

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg and there must be one term of that sort (inhabited)

bb25c06cca41ca78e5fb87fbb8e81d55beb18c95jg if not, output "no"

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

7014882c6a3672fd0e5d60200af8643ae53c5928Richard Lowe i.e. the f resp. the p in

7014882c6a3672fd0e5d60200af8643ae53c5928Richard Lowe forall x_1:s_n .... x_n:s_n . f(t_1,...,t_m)=t

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

7014882c6a3672fd0e5d60200af8643ae53c5928Richard Lowe Implication Application Strong_equation

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

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

fa9e4066f08beec538e775443c5be79dd423fcabahrens Implication Predication Equivalence

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

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrenscheck' :: [EquationInfo] -> ([ExhaustivePat],EqnSet)

fa9e4066f08beec538e775443c5be79dd423fcabahrenscheck' [] = ([([],[])],emptyUniqSet)

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens-- nur ein Pattern, bestehend aus nur Variablen? fertig, True

fa9e4066f08beec538e775443c5be79dd423fcabahrenscheck' [EqnInfo n ctx ps (MatchResult CanFail _)]

fa9e4066f08beec538e775443c5be79dd423fcabahrens | all_vars ps = ([(takeList ps (repeat new_wild_pat),[])], unitUniqSet n)

fa9e4066f08beec538e775443c5be79dd423fcabahrens

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

fa9e4066f08beec538e775443c5be79dd423fcabahrenscheck' qs@((EqnInfo n ctx ps (MatchResult CanFail _)):rs)

fa9e4066f08beec538e775443c5be79dd423fcabahrens | all_vars ps = (pats, addOneToUniqSet indexs n)

fa9e4066f08beec538e775443c5be79dd423fcabahrens where

fa9e4066f08beec538e775443c5be79dd423fcabahrens (pats,indexs) = check' rs

fa9e4066f08beec538e775443c5be79dd423fcabahrens

fa9e4066f08beec538e775443c5be79dd423fcabahrens-- falls ein Konstruktor dabei ist: split_by_constructor

fa9e4066f08beec538e775443c5be79dd423fcabahrens-- wenn die ersten Argument nur Variablen sind: first_column_only_vars

fa9e4066f08beec538e775443c5be79dd423fcabahrenscheck' qs@((EqnInfo n ctx ps result):_)

fa9e4066f08beec538e775443c5be79dd423fcabahrens | all_vars ps = ([], unitUniqSet n)

fa9e4066f08beec538e775443c5be79dd423fcabahrens | constructors = split_by_constructor qs

fa9e4066f08beec538e775443c5be79dd423fcabahrens | only_vars = first_column_only_vars qs

fa9e4066f08beec538e775443c5be79dd423fcabahrens | otherwise = panic "Check.check': Not implemented :-("

fa9e4066f08beec538e775443c5be79dd423fcabahrens where

fa9e4066f08beec538e775443c5be79dd423fcabahrens -- Note: RecPats will have been simplified to ConPats

-- at this stage.

constructors = or (map is_con qs)

only_vars = and (map is_var qs)

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

Heng (Klaus)

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

emacs mode

OWL-DL logic

OWL-DL -> CASL

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

LaTeX pretty printer

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

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

f�r die CASL Datentypen zu bekommen.

HasCASL hat auch noch keine Mixfix- und Latex Ausgabe.

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

Christian

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

logic coding form 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

Missing points for heterogeneous WADT 04 example:

- improve display of HasCASL sigs + mors

Static analysis for HasCASL

checking class constraints of terms

pattern analysis for program equations

Sub-/Supertypes

- for simple types (currently type synonyms)

symbol representation

symbol map analysis (hiding sub/supertypes)

Weak amalgamation analysis?

Instantiate Transformation Application system for HasCASL?

Automatic generation of Haskell (for a HasCASL subset)

Proofs in HasCASL

Case study

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

Klaus

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

CASL -> SPASS

Coding of subsorts as unary predicates (for ontologies)

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)

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

IsaWin: support CASL-libraries

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

Till

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

basicProofs: use info about used axioms

ensure that axiom/thm names are unique

Overload / inlineAxioms: injections

GUI: use daVinci close button;

use Workbench tool registration for central shutdown

use save button for saving proof info

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)]

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]

- George wg. Schlie�en von Fenstern

- 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

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)

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