Beweisobjekte an DGs, nicht an Regeln
F�r Theoreme in Theorien an Beweisobjekte
BasicProof mit Liste von Beweisobjekten
Isabelles Beweisobjekte einbinden
************************************************
************************************************
set up default simplifier
set up default tactics using axioms
************************************************
************************************************
rename variables that conflict with operation syntax
(or restrict mixfix decls for consts)
die Mixfix-Deklarationen f�hren noch zu Problemen.
f�hrt dazu, dass c nicht mehr als Variable verwendet werden kann.
K�nntest du diese Mixfix-Deklarationen auf die notwendigen F�lle
beschr�nken, und ggf. die Variablen umbenennen?
Zudem m�ssen Underscores escaped werden:
Interface Hets <-> ISabelle
Hets muss eine Pipe als Inode erzeugen
und dann auf Beweisterme warten
und dann Proof_status sen proof_tree entsprechend ausf�llen
Isabelle (im .thy file, dass von
IsaProve.hs erzeugt wird)
Beweisterme (siehe Kapitel im RefMan)
ML "proofs := 1" (am Anfang des .thy file)
am Ende jedes Theorems: Beweisterm in die Pipe schreiben
(Pipenamen direkt angeben, vom thy-file-Namen abgeleitet)
am Schluss "Ende" ausgeben
Theorem link nur dann gr�n, wenn alle Goals bewiesen wurden
************************************************
************************************************
use save button for saving proof info
development graph calculus
- Stack overflow for "show just subtree"
- fail when doing first globDecomp, then local decomp in RelationsAndOrders
- correct MAYA: glob decomp: some links are not found (Jorina)
for local subsume in RelationsAndOrders
************************************************
************************************************
Funktionen imageOfMorphism und inhabited
"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
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)
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)
(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 :-("
-- Note: RecPats will have been simplified to ConPats
constructors = or (map is_con qs)
only_vars = and (map is_var qs)
subsort definitions: are conservative if formula is satisfiable
(generate proof obligation)
************************************************
************************************************
LaTeX: see
listings.sty for LaTeX generation (cf. CoSiT paper)
show hets output immediately
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)
-------------------------------------------------------------------
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.
************************************************
************************************************
generate infrastructure for circular coinduction
CCS example: commutativity of || by coinduction
************************************************
************************************************
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)
fixes translation error of Pair
simplification of HasCASL sentences (omit types)
Logic COL is a ruin (with wrongly qualified module names)
pretty printing mangles trailing and preceding annotations
logic coding from the comand line with printing of results
Haskell modules: hiding, renaming
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)
************************************************
************************************************
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
Joost Visser wg. ATerms in Haskell => neues Repository
************************************************
************************************************
Weitere %implies-Annotationen zu den Basic Datatypes hinzufuegen
(Vorbild: Larch-Handbuch)
Parser and static analysis for CSP-CASL
************************************************
************************************************
IsaWin: support CASL-libraries
************************************************
************************************************
computeTheory does not work across library imports
hierarchical Isabelle theories
daVinci printing is not adequate
hiding of internal nodes does not work
FOL without quantifiers and with uniform disjunctions
algorithmic path consistency over a relation algebra
plug in reasoner for this
develop correctness results (algorithmic path consistency=path consistency)
FOL without quantifiers (with and without =)
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
topsort coding: partial functions as relations?
theorem link menu for proof obligations
in Isabelle. Reason: Inlineaxioms does not translate ga_totality axioms
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
theorem links between nodes in different libraries
basicProofs: use info about used axioms
Overload / inlineAxioms: injections
remove "prove" menu in abstracted dg
better sublogic analysis in codings
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
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
sublogic translation table
better interaction between Isabelle instance (for one node)
+ selection of single goals that are proved
=> use PGIP interface (Christoph, David)
Keep proofs and lemmas in .thy files (kind of merge)
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
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
Different types of logic translations
Improve Static analysis of structured specs
Development graph calculus, Strategies for DG rules
FOL-prover by Uli Furhbach
modal logic: IRIT, Toulouse. Tableaux prover LOTREC, Andreas Herzig
Renate Schmidt, Manchester: uses FOL prover for description logic
(as efficient as DL-specific tools!)
consistency: see IJCAR-workshop on non-provability in Cork
IJCAR workshop about logical frameworks and meta-languages
Klaus' wayfinding example
ask Detlef: critical pairs, Fossacs paper by Francesco
first steps towards CASL instance, using ATerms and re-using MMISS instance
variants for specs (needed for DOLCE: CASL variant, DL variant, ...)
+ 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
************************************************
************************************************
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
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...?)
Data.Serizable (only when ghc supports it) better: rely on pointer equality
integrate QuickCheck: come to lecture!
++++++++++++++++++++++++++++++++++++++++++++++++
++++++++++++++++++++++++++++++++++++++++++++++++
Mark-Oliver Stehr, Hamburg cf. HOL-Nurpl-Translation in Maude
Proofs with basic datatypes
Verbesserung der Fehlermeldungen
Example of Agnes und Frank: proofs in HOL-CASL (2 days)
Examples for cond rewriting -> Christophe
Doku: VSE-Prover, VSE-Method VSE-demo in Bremen?
Eigene IsaWin-Instanz mit CASL-RS statt HOL-RS
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)
Generate Proof obligations (1 week)
Add renaming to Isabelle kernel (2 months)
Repository mit korrekten und fehlerhaften Specs
HetCATS User manual, Doku fuer Environments (2 weeks)
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
Uebersetzung von CASL-LaTeX-Spezifikationen nach ASCII
Neues Tool-Schaubild auf Web-Seiten ver�ffentlichen
{- This does not work due to needed ordering:
instance Functor Set where
m >>= k = unionManySets (setToList (fmap k m))
[("normal","normal","normal"),
("normal","inclusion","normal"),
("inclusion","normal","normal"),
("inclusion","inclusion","inclusion")]
Aufbau des Graphen selbst