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.
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.
- 18:00 Transfer and arrival at Schloss Etelsen
18:00 - 19:00 Diner
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
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
Breakfast and departure
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.
