Bridging holes on Dedukti proofs, an overview

Guillaume Burel

There are many contexts in which one may be interested in proofs containing holes: In interactive theorem proving, metavariables can be used to refine goals into subgoals. Proof traces produced by automated theorem provers can also be seen as proofs in which some steps are missing. Finally, in the context of proof interoperability and of cooperation between provers, a hole in a proof can be used as a point where the subgoal has been delegated to another prover or another procedure. We will survey how this issue has been tackled in the domain of Dedukti. This involves restarting the proof from scratch, using the proof trace merely as a guide; reconstructing the missing steps using proof-generating automated theorem provers; and developing tactics that deals with proof holes.

Back to the main page