Inferring the Proof Process
Andrius Velykis · 2012
Abstract. This PhD project aims to investigate how enough informa-tion can be collected from an interactive formal proof to capture an expert’s ideas as a high-level proof process. It would then serve for ex-tracting proof strategies to facilitate proof automation. Ways of inferring this proof process automatically are explored; and a family of tools is de-veloped to capture the different proof processes and their features. 1