CIAO-02 Workshop

Edinburgh, 11-12 April 2002

DReaM group
Division of Informatics
University of Edinburgh
Scotland

Organiser:
Ewen Denney

Foreword


The 11th CLAM-INKA-OMRS workshop (CIAO-2002) was held in Edinburgh on the 11th and 12th of April 2002. Previous CIAO's have been held in Genova (2001), Dagstuhl (2000), and Edinburgh (1999). It is intended to provide a snapshot of research into automating mathematical reasoning, especially in the areas of proof planning, rippling, combination and integration of specialised reasoners (as, e.g. decision procedures) as well as their application to program development and related areas.

The CIAO series of workshops began in 1992 and was originally limited to the Clam and INKA systems, later joined by the OMRS system. Given the widening of interest in these areas, the CIAO-2002 workshop is inviting participation from groups involved in closely related research.

Group photo

Last minute problems

If you have any last minute questions or problems concerning the CIAO-02 Workshop, if I am not accessible, please contact either myself or Alan Smaill, smaill@dai.ed.ac.uk who has kindly agreed to look after problems in my absence.

Ewen

Accommodation

I've compiled a list of suggestions for you to contact directly.

Miscellaneous Info

Edinburgh Tour
A good overview of the city and its surroundings from the Department of Geography.
Edinburgh and Lothians Tourist Board
The official Edinburgh tourist site.

Programme

Wednesday 10th of April 19:00 - 21:00

Informal get together at The Elephant House
21 George IVth Bridge (location map -- look for the red circle).
We'll have a couple of tables in here from 7 till 9pm. Come along any time if you want to get something to eat and meet up with other participants.
Thursday 11th of April

All talks take place in room F13, 80 South Bridge.

9:00 - 9:20 Coffee Available
9:20 - 9:30
Welcome to CIAO-02
9:30 - 10:45 Methods
9:30 - 9:55 Alan Bundy:
Limitations of Rippling
9:55 - 10:20 James Brotherston:
Hierarchy Vs. Meritocracy: A Best-First Methodical in Lambda-Clam
10:20 - 10:45 Seungyeob Choi:
Semantic Restriction of Methods in Proof Planning
10:45 - 11:15 Coffee Break
11:15 - 12:30 Representation Issues
11:15 - 11:40 Mateja Jamnik:
Automatic Learning of Proof Methods in Proof Planning
11:40 - 12:05 Manfred Kerber:
Extendible Reasoning
12:05 - 12:30 Martin Pollet:
Frame Representation of Mathematical Concepts for Proof Planning
12:30 - 14:00 Lunch
14:00 - 15:15 Foundations
14:00 - 14:25 Julian Richardson:
Continuing Continuations of Proof Strategies
14:25 - 14:50 Ewen Denney:
Towards a Framework for Tactic Languages
14:50 - 15:15 Axel Schairer:
Supporting Evolutionary Formal Development using Proof Transformations
15:15 - 15:45 Coffee Break
15:45 - 17:00 Logical Issues
15:45 - 16:10 Paolo Torrini:
Embedding intuitionistic second-order propositional logic in Isabelle HOL
16:10 - 16:35 Alan Smaill:
Recursive plan formation via linear logic
16:35 - 17:00 Serge Autexier:
Intuitive & Contextual Reasoning
19:30 - ad lib. Official CIAO-02 Dinner
Hadrian's, Balmoral Hotel, 1 Princes Street

Friday 12th of April

All talks take place in room F13, 80 South Bridge.

9:30 - 10:00 Coffee Available
10:00 - 10.50 Verification
10:00 - 10:25 Stephan Schweitzer:
Equality Reasoning in the VeriFun System
10:25 - 10:50 Andrew Ireland:
An Investigation into Proof Automation for the SPARK Approach to High Integrity Ada
10:50 - 11:15 Coffee Break
11:15 - 12:30 System Integration
11:15 - 11:40 Paul Jackson:
Translating the Mizar Mathematical Library into HOL
11:40 - 12:05 Lucas Dixon:
A Framework for Proof Planning in Isabelle
12:05 - 12:30 Graham Steel:
Using Implicit Induction To Guide A Parallel Search For Inconsistency
12:30 - 14:00 Lunch
14:00 - 15:15 Mathematical Applications
14:00 - 14:25 Toby Walsh:
A Proof Planner to Generate Implied Constraints
14:25 - 14:50 Volker Sorge:
Comparing Approaches to the Exploration of the Domain of Residue Classes
14:50 - 15:15 Ewen Maclean:
Proof Planning Nonstandard Analysis
15:15 - 15:45 Coffee Break
15:45 - 17:00 Other Applications
15:45 - 16:10 Dieter Hutter:
Security of Mobile Agents
16:10 - 16:35 Louise Dennis:
Planning the Whisky Problem: A Comparison of Two Proof Critics
16:35 - 17:00 Alexei Lisitsa:
Towards proof planning for first-order temporal reasoning

Created by ewd@dai.ed.ac.uk and A.Smaill@ed.ac.uk
Last modified: Tue Apr 9 10:31:57 BST 2002