18th CIAO Workshop, CIAO-2009

31.3 - 3.4.2009, Schloß Etelsen, Langwedel (close to Bremen)


The CIAO workshop 2009 will be held at Schloß Etelsen, Langwedel, Germany (located close to Bremen) from the evening of March 31st until Friday 3rd 2009 in the morning.

It is intended to provide a snapshot of research into automating mathematical reasoning, especially in the areas of proof planning, rippling, verification and related areas. Given the widening interested in these areas, the CIAO-2009 workshop is inviting participation from groups involved in closely related research.

Participation and Talks

If you plan to attend the CLAM-INKA-OMRS Workshop, please send an email to Dieter (hutter@dfki.de) as soon as possible but not later than February 13th 2009. Please specify if your arrival/departure dates differ from the planned 31.3/3.4 and if you want a double room and with whom you would like to share it. If nothing is specified we assume that you are heading for a single room. If you also plan to give a talk, please specify the title and abstract and any constraints you may have (eg. you still want to use a blackboard or an overhead projector). The deadline is the same.


The CIAO workshop 2009 will be held at Schloß Etelsen, Langwedel, Germany (located close to Bremen). We will organize a mini-bus shuttle from the railway station and airport of Bremen to this location.


Some pictures of the event are available here. Thanks to Alan and Serge.


Tuesday, March 31


          - 18:00      Transfer and arrival at Schloss Etelsen

18:00 - 19:00      Diner


Wednesday, April 1


8:45  - 9:00         Welcome

9:00  - 10:30       Composition of theories

Till Mossakowski:     The heterogeneous tool set

Florian Rabe:           A Module System for a Logical Framework

Alan Smaill:              A variant of signature morphisms.

10:30 - 11:00      Coffee break

11:00 - 12:30      Logic and Deduction

Lucas Dixon:            From logic to DAGs with a eye to changing notation

Dominik Dietrich:     Specification and Compilation of Deep Inference Rules

Manfred Kerber:      Normalizations for Testing Heuristics in Propositional Logic

12:30 - 14:00      Lunch

14:00 - 16:00      Galileo and Ontologies

Alan Bundy:              The Architecture of the GALILEO Project

Jos Lehmann:          A Case Study of Ontology Evolution in Atomic Physics as the  Basis of the Open Structure Ontology Repair Plan

Michael Chan:          Towards an ontology repair plan for unifying theories

Lutz Schröder:         TBox Reasoning in Coalgebraic Hybrid Logic

16:00 - 16:30      Coffee break

16:30 - 17:30      Security

Anne Kayem:           Data Outsourcing in Service Oriented Architectures:   Mitigating Security Challenges.

Lassaad Cheikhrouhou and Werner Stephan: 
                                 Inductive Verification of Password Protocols

18:00                  Diner


Thursday, April 2


9:00  - 11:00       Formal System Managenent

Serge Autexier:        DocTip - System Architecture

Dieter Hutter:            DocTip - Management of Change

David Aspinall, Christoph Lüth:  

                                 Towards a generic hierarchical proof theory.

Christoph Lange      Integrating Web Services into Active

11:00 - 11:30      Coffee break

11:30 - 12:30      Heuristics (1)

Markus Aderhold:     Synthesis of Induction Axioms for Procedures with
Second-Order Recursion

Alison Pease:           Metaphor and Analogy in Mathematics

12:30 - 13:30      Lunch

13:30 - 15:00      Heuristics (2)

Mark Guhe:               Local contexts in human and machine intelligence

Marvin Schiller:        Putting Adaptive Modelling of Proof Step Size for Mathematics Tutoring to the Empirical Test

Frank Theiss:           Higher-Order and First-Order TPTP in Practice

15:00 - 15:30      Coffee break

15:30 - 17:30      Theorem  generation and verification

Christopher Krauss: Property preserving refinement in hybrid automata

Roy McCasland:      Theorem-Producing Rules -- One Year On

Omar Montano Rivas:  Scheme-based theorem discovery and concept invention

Lilia Georgieva:        First-order logic for program validation

18:00                  Diner


Friday, April 3


Breakfast and departure


Further Information

German train schedule is available here

There are direct flights with Ryan Air from Edinburgh to Bremen. From Linz flights are via Munich or Frankfurt with Lufthansa and Austrian Airlines.

Previous CIAO Workshops


Dieter Hutter, DFKI GmbH, Bremen, Germany, hutter@dfki.de Tel. ++49 421 218 64277, Fax. ++49 421 218 98 64277