[Club2] 23.04; 10.30 (Turing)

[Norbert Schirmer]

Am Montag, 23.04, ab 10:30 im Turing (00.09.055):

SEP "Google meets Isabelle: Advanced Search für Isabelles Theorem- 
Bibliothek"

Isabelle ist ein generischer Theorembeweiser. Mathematische Formeln  
können in
einer formalen Sprache notiert und in einem logischen Kalkül bewiesen  
werden.
Inzwischen ist eine große Bibliothek bereits bewiesener Theoreme aus
zahlreichen Gebieten der Mathematik, darunter Zahlentheorie, Analysis,
Algebra und Mengenlehre, Bestandteil von Isabelle. Insgesamt enthält  
diese
Bibliothek zur Zeit weit über 5000 Theoreme.

Diese große Anzahl von Theoremen macht eine Suchfunktion unentbehrlich.
Eine solche Suchfunktion ist bereits in Isabelle implementiert. Der  
User kann
diese Suche im ProofGeneral über "Find Theorems" aufrufen.

Doch gerade der unerfahrene User wird beim Aufruf von "Find Theorems"  
vor
einigen Problemen stehen. Er wird sich erst einmal die Frage stellen,  
wie die
Suchfunktion überhaupt funktioniert. Er wird sich unweigerlich  
fragen, nach
was er suchen kann, welche Suchkriterien es gibt, und welche Syntax  
die Suche
erfordert. Ohne weiteres Recherchieren wird dieser User die  
Suchfunktion nicht
nutzen können.

Um dieses Problem zu lösen, wurde im Rahmen eines SEPs eine Suchmaske
entwickelt. Zudem sollte auch ein Konfigurationsdialog entwickelt  
werden, der
es auf komfortable Weise ermöglicht, im ProofGeneral die  
isabellespezifischen
Parameter einzustellen.

Die Suchmaske und der Dialog zum Einstellen der Parameter werden am  
Montag,
den 23.04.07 um 10.30 Uhr vorgestellt.

    Norbert