Montag, 4. Oktober 2004

14:00 - 14:15

J. Siekmann: Eröffnung & Logik und Deduktion in Saarbrücken

14:15 - 14:45

D. Hutter: Management of Change

14:45 - 15:15

A. Schairer: Transformations for Evolutionary Formal Developments

15:15 – 16:00

Kaffeepause

16:00 – 16:30

T. Kraußer: Reasoning within Pointer Structures: A VSE Case Study

16:30 – 17:00

R. Küster: Automatic Analysis of Cryptographic Protocols with Exclusive Or and Diffie-Hellman Exponentiation

17:00 – 17:30

R. Piskac: A formally verified algorithm for checking priority queues

17:30 – 18:30

FG 1.2.1 Business Meeting

Dienstag, 5. Oktober 2004

9:00 – 9:30

S. Autexier, M. Pollet: The Mathematics Assistance System OMEGA

9:30 – 10:00

A. Meier: Beweisplanen mit mehreren Strategien

10:00 – 10:30

A. Fiedler: User-oriented interactive authoring of checkable mathematical documents

10:30 – 11:15

Kaffeepause

11:15 – 11:45

C. Benzmüller: Natural Language-based Interaction with a Mathematics Assistance System

11:45 – 12:15

B. Q. Vo: A Proof-Manager for the DIALOG Project

12:15 – 14:00

Mittagessen

14:00 – 15:00

(Invited Talk) D. Kuske: MSO-definierbare lokale temporale Logiken fuer Mazurkiewicz-Spuren

15:00 – 15:30

J. Johannsen: Bounded model checking for all regular properties

15:30 – 16:00

Kaffeepause

16:00 – 16:30

V. Sofronie-Stokkermans: On shallow and local extensions of a base theory

16:30 – 17:00

B. Löchner: A Redundancy Criterion Based on Ground Reducibility by Ordered Rewriting

17:00 – 17:30

T. Schmidt-Samoa: Introduction to the New Proof Control of the Inductive Theorem Prover QuodLibet

17:30 – 18:30

FG 0.1.6 Business Meeting

From 19:30

Workshop Dinner

Mittwoch, 6. Oktober 2004

9:00 – 9:30

F. Baader: Syntactic sugar can speed up reasoning in Description Logics

9:30 – 10:00

P. Baumgartner: The Bernays-Schönfinkel Fragment of First-Order Autoepistemic Logic

10:00 – 10:45

Kaffeepause

10:45 – 11:15

H. de Nivelle: Deciding Modal Logics through Translations into GF2

11:15 – 11:45

C. Brown: Automated Theorem Proving in Extensional Type Theory

11:45 – 12:00

Abschluß