Integration von Entscheidungsprozeduren in einen interaktiven Beweisassistenten

The goal of this thesis represents the integration of an automatic decision procedure into an interactive proof system. The given automatic decision procedure called CVC 3 works with first order logic but the RISC Proof Navigator needs high order logic as input language. Therefore a model had to be implemented for the translation and verification of first order to high order logic. As a preliminary work for the translation function, first order logic, typed first order logic, high order logic and typed high order logic had to be defined. Finally, the translation function was integrated as an interface between the decision procedure and the interactive proof system.