University of Cambridge > > 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-II

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

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.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.


© 2006-2024, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity