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 talksSurrogate models in Bayesian Inverse Problems Poland, Europe, Freedom: A Personal Reflection on the Last 40 Years Louisiana Creole - a creole at the periphery Understanding model diversity in CMIP5 projections of westerly winds over the Southern Ocean Protein Folding, Evolution and Interactions Symposium Validation & testing of novel therapeutic targets to treat osteosarcoma Stromal microenvironments and the control T-cell development and selection Cyclic Peptides: Building Blocks for Supramolecular Designs Amino acid sensing: the elF2a signalling in the control of biological functions Satellite Applications Catapult Quickfire Talks |