CADE-15 Workshop on

Many practical applications of deduction systems in mathematics, computer science, and artificial intelligence rely on the correct and efficient treatment of partial functions. For this purpose different approaches -- from workarounds for concrete situations to proper general treatments -- have been developed.

There are essentially three approaches to treating partiality, which further subdivide into a multitude of specialized logical systems. In the first category, undefined expressions are syntactically excluded. In the second, they are disregarded or bypassed. In the third, partiality is taken seriously and this is reflected in the semantics and the calculus.

All approaches have their own advantages and disadvantages and are adequate for certain applications. The workshop is devoted to discussing these advantages and disadvantages and relating the different approaches. Applications of the different approaches are of particular interest.

Interested persons can directly register for the workshop with CADE.

The following programme is planned (papers available in gzipped PostScript form,
Copyright with the authors):

Session I (Chair: M. Kerber) | |

9:00-10:00 | Invited Talk: William M. Farmer |

STMM and partial functions | |

10:00-10:30 | Jan Kuper and Jan Feenstra |

Some experiments with undefinedness | |

10:30-11:00 | Coffe Break |

Session II (Chair: J. Giesl) | |

11:00-11:30 | Manfred Kerber |

A three-valued approach to overcome paradoxes in syntactic theory | |

11:30-12:00 | Lilian Burdy |

A treatment of partiality: its application to the B method | |

12:00-12:30 | Catherine Dubois and Véronique Viguié Donzeau-Gouge |

A step towards the mechanization of partial functions: domains as inductive predicates | |

12:30-14:00 | Lunch |

Session III (Chair: M. Kohlhase) | |

14:00-15:00 | Invited Talk: Deepak Kapur |

Regular Data Structures and Partiality--Interaction between Specification and Reasoning | |

15:00-15:30 | Jürgen Giesl |

Partial functions in induction theorem proving | |

15:30-16:00 | Coffee Break |

Session IV (Chair: R. Arthan) | |

16:00-16:30 | Jürgen Brauburger |

How to compute the domains of partial functions | |

16:30-17:00 | David A. Duffy |

Partial functions in the Z specification language | |

17:00-18:00 | Panel Session |

The complete workshop proceedings can be found here, PostScript, compressed, 304k.

**Organizers:**

- Rob Arthan,
Lemma 1 Ltd., Reading, UK

e-mail:`rda@lemma-one.com`. -
Jürgen Giesl, TU Darmstadt, Darmstadt, Germany

e-mail:`giesl@informatik.tu-darmstadt.de` - Ray Gumb,
University of Massachusetts, Lowell, MA, USA

e-mail:`gumb@cs.uml.edu` - Manfred Kerber,
The University of Birmingham, School of Computer Science, UK

e-mail:`M.Kerber@cs.bham.ac.uk`. - Michael Kohlhase,
Universität des Saarlandes, Saarbrücken, Germany

e-mail:`kohlhase@ags.uni-sb.de`.

The original Call for Participation can be found here.

Further information on partiality and its mechanization can be found here.

Last update: 24 June 1998