Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task?

## Authors: Hanna Lachnitt, Christoph Benzmüller and Maximilian Claus

## Paper Information

Title: | Embedding Intuitionistic Modal Logics in Higher-Order Logic. An Easy Task? |

Authors: | Hanna Lachnitt, Christoph Benzmüller and Maximilian Claus |

Proceedings: | WiL Short Papers and Abstracts |

Editors: | Valeria de Paiva, Amy Felty and Ursula Martin |

Keywords: | Intuitionistic Modal Logic, Higher-Order Logic, Automatic Verification |

Abstract: | ABSTRACT. Intuitionistic logics are very useful in practise, they are for example valuable for proof assistants. Nevertheless, they have been regarded controversial. David Hilbert wrote that: "Taking the principle of excluded middle from the mathematician would be the same, say, as proscribing the telescope to the astronomer or to the boxer the use of his fists."[5] Indeed, this property of intuitionistic logic may cause problems when trying to embed them in higher-order logic. The talk will give a short overview about this challenge and discuss possible solutions. |

Pages: | 1 |

Talk: | Jul 08 16:15 (Session 42R) |

Paper: |