"Integration von Entscheidungsprozeduren in einen interaktiven Beweisassistenten"
, Serie Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria, 6-2008
Integration von Entscheidungsprozeduren in einen interaktiven Beweisassistenten
Sprache des Titels:
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.
Sprache der Kurzfassung:
Research Institute for Symbolic Computation (RISC), Johannes Kepler University, Linz, Austria