Melanie Taprogge

• Automated Theorem Proving is a core area of artificial intelligence research, focusing on the development of software that autonomously proves complex statements from given premises across various application fields. However, the diversity of output encodings of specialized systems hinders the verification of derived proofs and cooperation between provers. The Dedukti framework addresses this issue by implementing the λΠ-calculus modulo, enabling proofs originating from different frameworks to be expressed, combined, and checked automatically. Formal verification of fully automated higher-order logic provers remains an unmet challenge. This thesis establishes a theoretical foundation for such verification by identifying common challenges and developing general encoding strategies. Based on these strategies, a modular encoding of selected inference rules of the versatile prover Leo-III is presented. The effectiveness of this approach is empirically evaluated through the partial automation of generating proof certificates verifiable within the Dedukti framework.