Plan and priority list for CoFI tool activities

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

Immanuel

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

Suchfunktion f�r einen Knoten im DG:

welche anderen Knoten sind hier mit Theoriemorphismus abbildbar?

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

- Funktion f�r Morphismus-Suche zwischen Theorien

- evtl. angucken: CASL.SymbolMapAnalysis, inducedFromToMorphism Map.empty

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

- Einbindung ins GUI (GUI.ConvertAbstractToDevGraph)

BasicProof in Proofs.Proofs: sind Datenstrukturen f�r informelle Beweise OK?

Konfidenzgrade von Beweisen?

von Till/HiWi zu erledigen:

Repr�sentation �ndern:

Beweisobjekte an DGs, nicht an Regeln -- done

F�r Theoreme in Theorien an Beweisobjekte -- done

BasicProof mit Liste von Beweisobjekten -- �berfl�ssig

Definitionen auszeichnen -- done

F�r alles siehe G_theory, ThSens und SenStatus.

Isabelles Beweisobjekte einbinden

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

Florian (Till)

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

abstrakte Syntax f�r ConstraintCASL (s. CASL-lib/ConstraintCASL/)

nach HetCATS/ConstraintCASL/AS_ConstraintCASL.der.hs

Range hinzuf�gen (vgl. HetCATS/CASL/AS_Basic.der.hs)

Parser f�r ConstraintCASL

nach HetCATS/ConstraintCASL/Parse_AS_Basic.hs

tokens aus Common/Lexer.hs wiederverwenden

neuer Parser f�r Terme

Testen mit

hets -o ast.het CASL-lib/ConstraintCASL/RCC8.het

trace verwenden

einfachen Test einchecken

Freiburger Constraint-Solver angucken

Bremer Constraint-Solver angucken

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

Mingyi (Till)

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

port CCC to Haskell

Funktionen imageOfMorphism und inhabited

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

mit "cvs add SigFuns.hs" einchecken

New module FreeTypes.hs:

"free datatypes and recursive equations are consistent"

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

Just True => Yes, is consistent

Just False => No, is inconsistent

Nothing => don't know

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

- each new sort must be a free type,

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

(Sort_gen_ax constrs True)

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

if not, output "don't know"

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

if not, output "no"

- 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 . f(t_1,...,t_m)=t

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

Implication Application Strong_equation

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

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

Implication Predication Equivalence

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

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

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

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

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

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

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

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

| all_vars ps = (pats, addOneToUniqSet indexs n)

where

(pats,indexs) = check' rs

-- falls ein Konstruktor dabei ist: split_by_constructor

-- wenn die ersten Argument nur Variablen sind: first_column_only_vars

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

| all_vars ps = ([], unitUniqSet n)

| constructors = split_by_constructor qs

| only_vars = first_column_only_vars qs

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

where

-- Note: RecPats will have been simplified to ConPats

-- at this stage.

constructors = or (map is_con qs)

only_vars = and (map is_var qs)

subsort definitions: are conservative if formula is satisfiable

(generate proof obligation)

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

Heng (Klaus)

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

OWL-DL logic

OWL-DL (<)-> CASL-DL

emacs mode:

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

some operation symbols

show hets output immediately

C-c C-g for hets -g

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

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

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

Version for XEamcs?

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

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

Hilfskraft 1

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

Modal-CASL <-> CASL-DL

see Chapter 4 of "The Description Logic Handbook"

and ask Klaus for a print out of it

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

Hilfskraft 2

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

Uni-Refactoring,

make modules hierarchical, change scoped type variables for ghc-6.5

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

use HaXml as a cabalized library, provide uni as (one?) cabal

package(s), uni used to work under windows as well, watch the

i.e. FilePath, Process discussions (libraries@haskell.org)

possibly switch to a subversion repository, talk to Achim

(amahnke@tzi.de)

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

Ken (Till)

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

development graph calculus

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

look at Static/DevGraph.hs

look at Proofs/EdgeUtils.hs Proofs/StatusUtils.hs Proofs/Global.hs

implement simplified rule Theorem-Hide-Shift

try out examples

conservativity calculus

weakly amalgamable cocones

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

Zheng (Till)

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

look at Static/DevGraph.hs

look at translation to OMDoc

change management via translation to OMDoc

einfaches Merge von lokalen Beweisen eines abgespeichteren DG

in aktuellen DG

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

Hilfskraft 4

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

port hets to windows.

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.

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

Hilfskraft 5

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

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 (but no table)

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

development graph calculus

- Stack overflow for "show just subtree"

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

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

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

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

for local subsume in RelationsAndOrders

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

Daniel

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

generate infrastructure for circular coinduction

CCS example: commutativity of || by coinduction

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

Christian

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

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

Missing points for heterogeneous WADT 04 example:

- improve display of HasCASL sigs + mors

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

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

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

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

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

IsaWin: support CASL-libraries

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

Till

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

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

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