BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//talks.cam.ac.uk//v3//EN
BEGIN:VTIMEZONE
TZID:Europe/London
BEGIN:DAYLIGHT
TZOFFSETFROM:+0000
TZOFFSETTO:+0100
TZNAME:BST
DTSTART:19700329T010000
RRULE:FREQ=YEARLY;BYMONTH=3;BYDAY=-1SU
END:DAYLIGHT
BEGIN:STANDARD
TZOFFSETFROM:+0100
TZOFFSETTO:+0000
TZNAME:GMT
DTSTART:19701025T020000
RRULE:FREQ=YEARLY;BYMONTH=10;BYDAY=-1SU
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
CATEGORIES:Computer Laboratory Automated Reasoning Group Lunc
hes
SUMMARY:Exploring Properties of Normal Multimodal Logics i
n Simple Type Theory with LEO-II - Christoph Benzm
ueller ()
DTSTART;TZID=Europe/London:20080304T130000
DTEND;TZID=Europe/London:20080304T140000
UID:TALK9887AThttp://talks.cam.ac.uk
URL:http://talks.cam.ac.uk/talk/index/9887
DESCRIPTION:Speaker: Christoph Benzmueller\n\nWe sketch the re
sults of the LEO-II project and show how\nthe high
er-order theorem prover LEO-II can be employed to
reason about (normal) multimodal logics. For this
we pick up and extend an embedding of multimodal l
ogics in simple type theory as suggested by Brown.
The starting point is a characterization of multi
modal logic formulas as particular lambda-terms in
simple type theory. A\ndistinctive characteristic
of the encoding is that the definiens of the [ R
] operator lambda-abstracts over the accessibility
relation R. We illustrate that this supports the
formulation of meta properties of encoded multimod
al logics such as the correspondence\nbetween cert
ain axioms and properties of the accessibility rel
ation R. We show that some of these meta propertie
s can even be efficiently automated within our hig
her-order theorem prover LEO-II via cooperation wi
th the first-order automated theorem prover E.
LOCATION:Computer Laboratory\, William Gates Building\, Roo
m SS03
CONTACT:Thomas Tuerk
END:VEVENT
END:VCALENDAR