Abstract

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.