BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Exploring Properties of Normal Multimodal Logics in Simple Type Th
 eory with LEO-II - Christoph Benzmueller ()
DTSTART:20080304T130000Z
DTEND:20080304T140000Z
UID:TALK9887@talks.cam.ac.uk
CONTACT:Thomas Tuerk
DESCRIPTION:Speaker: Christoph Benzmueller\n\nWe sketch the results of the
  LEO-II project and show how\nthe higher-order theorem prover LEO-II can b
 e employed to reason about (normal) multimodal logics. For this we pick up
  and extend an embedding of multimodal logics in simple type theory as sug
 gested by Brown. The starting point is a characterization of multimodal lo
 gic formulas as particular lambda-terms in simple type theory. A\ndistinct
 ive characteristic of the encoding is that the definiens of the [ R ] oper
 ator lambda-abstracts over the accessibility relation R. We illustrate tha
 t this supports the formulation of meta properties of encoded multimodal l
 ogics such as the correspondence\nbetween certain axioms and properties of
  the accessibility relation R. We show that some of these meta properties 
 can even be efficiently automated within our higher-order theorem prover L
 EO-II via cooperation with the first-order automated theorem prover E.
LOCATION:Computer Laboratory\, William Gates Building\, Room SS03
END:VEVENT
END:VCALENDAR