Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II

Add to your list(s) Download to your calendar using vCal

• Christoph Benzmueller ()
• Tuesday 04 March 2008, 13:00-14:00
• Computer Laboratory, William Gates Building, Room SS03.

If you have a question about this talk, please contact Thomas Tuerk.

Speaker: Christoph Benzmueller

We sketch the results of the LEO -II project and show how the higher-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 logics in simple type theory as suggested by Brown. The starting point is a characterization of multimodal logic formulas as particular lambda-terms in simple type theory. A distinctive 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 multimodal logics such as the correspondence between 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 LEO -II via cooperation with the first-order automated theorem prover E.

This talk is part of the Computer Laboratory Automated Reasoning Group Lunches series.

This talk is included in these lists:

• All Talks (aka the CURE list)
• Cambridge talks
• Computer Laboratory Automated Reasoning Group Lunches
• Computer Laboratory, William Gates Building, Room SS03
• Department of Computer Science and Technology talks and seminars
• Interested Talks
• School of Technology
• Trust & Technology Initiative - interesting events
• bld31
• yk373's list

Note that ex-directory lists are not shown.