COOKIES: By using this website you agree that we can place Google Analytics Cookies on your device for performance monitoring. |

University of Cambridge > Talks.cam > Computer Laboratory Automated Reasoning Group Lunches > Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-II

## Exploring Properties of Normal Multimodal Logics in Simple Type Theory with LEO-IIAdd 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 talks
- Computer Laboratory, William Gates Building, Room SS03
- Interested Talks
- School of Technology
- Trust & Technology Initiative - interesting events
- bld31
- yk373's list
Note that ex-directory lists are not shown. |
## Other listsThe Oon Lectures What IS the deal with meat? ETECH Projects## Other talksUnderstanding model diversity in CMIP5 projections of westerly winds over the Southern Ocean Louisiana Creole - a creole at the periphery Poland, Europe, Freedom: A Personal Reflection on the Last 40 Years Surrogate models in Bayesian Inverse Problems Satellite Applications Catapult Quickfire Talks |