Freie Logik erweitert Logik um den Aspekt der Nichtexistenz von Objekten und schafft Raum für Undefiniertheit. Logische Schlussfolgerungen über solche nicht-klassischen Logiken können über unkonventionelle Einbettungen in die klassische Logik höherer Stufe gezogen werden. Automatische Beweiser für höherstufige Logik sezen auf die TPTP-Sprache THF, eine standardisierte Kodierung für Formeln der Logik höherer Stufe. In dieser Arbeit wurde eine TPTP-konforme Kodierung für die nicht-klassische freie Logik entworfen sowie die Einbettung von freier Logik in Logik höherer Stufe implementiert. Ziel der Arbeit war es, die native Formulierung von Formeln der freien Logik zu ermöglichen, für deren Auswertung aber trotzdem auf die Fertigkeiten von namhaften höherstufigen Theorembeweisern wie Leo-II(I) ausgewichen wird.

Die Effektivität der Übersetzung wurde anhand beispielhafter Formalisierungen untersucht. Ansatzpunkt dafür bildete das kategorientheoretische Buch Categories, Allegories von Freyd und Scedrov (1990).