FLOC 2018: FEDERATED LOGIC CONFERENCE 2018
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: