Computational Linguistics Colloquium

Thursday, November 15, 16:15, Building 17, Seminar Room

Implicational Goal Directed Proof Methods

The idea of implicational goal directed proof methods attempts to present a large variety of non-classical, intermediate, substructural and non-monotonic logics in a uniform way, using an object level Prolog like goal directed proof theory.

This approach not only gives efficient uniform proof methods for many logics (since a strong Cut is built in) but also allows for metalevel mechanisms (such as interpolation, abduction, resource cost, etc.) to be inductively calculated following the proof procedures.

Surprising examples and applications will be given.

References:
Gabbay - Olivetti - Goal directed proof, Kluwer 2000.
Gabbay - Elementary Logics a procedural perspective, Prentice Hall 1998.

If you would like to meet with the speaker, please contact Jörg Siekmann.