Die berühmte Double Negation Translation stellt eine Einbettung von klassischer in intuitionistische Logik dar. Interessanterweise ist die umgekehrte Richtung in der Literatur noch nicht behandelt worden. Wir präsentieren eine effektive Einbettung von intuitionistischer in klassische Logik, sowohl im Fall der Aussagenlogik als auch im Fall der Prädikatenlogik, sowie eine effektive Einbettung von intuitionistischer Aussagenlogik in quantifizierte boolesche Formeln. Darüber hinaus implementieren wir ein System, das intuitionistische Probleme der Prädikatenlogik im tptp-Dateiformat als Input nimmt und die Transformation durchführt. Dies ermöglicht die Verwendung von klassischen Beweissystemen zur Überprüfung intuitionistischer Gültigkeit. Wir testen unsere Implementierung mithilfe des Vampire-Beweissystems an der ILTP-Datenbank. Schließlich diskutieren wir, wie die generierten klassischen Beweise des transformierten Problems in intuitionistische Beweise des ursprünglichen Problems zurückübersetzt werden können. Insgesamt wird damit ein neuartiger Ansatz zum automatisiertem Theorembeweis für intuitionistische Logik etabliert und ein erster Proof of Concept erbracht.

The famous double negation translation establishes an embedding from classical into intuitionistic logic. Curiously, the reverse direction has not been covered in literature. We present an effective embedding from intuitionistic into classical logic, both in the propositional and first-order case, as well as an effective embedding of intuitionistic propositional logic into quantified boolean formulas. Furthermore, we implement a system that takes intuitionistic first-order problems in the tptp file format as an input and performs our transformation. This allows the use of classical theorem provers for checking intuitionistic validity. We benchmark our implementation using the Vampire theorem prover on the ILTP problem set. Finally, we discuss how the generated classical proofs of the transformed problem can be translated back into intuitionistic proofs of the original problem. All in all, this establishes a novel approach to theorem proving for intuitionistic logic and provides a first proof of concept.