Bridging the gap between automated and interactive theorem provers remains one of the major challenges in formal reasoning. Automated theorem provers can generate proofs very efficiently, but their internal proof representations are usually not readily translatable into proofs checkable by interactive theorem provers. Techniques such as the analytic tableau method are, in principle, well suited to produce proofs that can be certified, but things get more complicated when we use more advanced proof-search strategies — e.g., Skolemization — that transform the structure of the proof.

In this talk, we will discuss how this problem can be addressed through deskolemization, the process of reconstructing the logical structure of tableau proofs that rely on different Skolemization strategies. We will present a generic deskolemization framework, implemented in the Goéland prover, and show how the resulting proofs can be exported and verified in systems such as Rocq, Lambdapi, SC-TPTP and Lisa.