Contextualized abstraction for assertion-level theorem proving

In this paper we propose a context-based approach to abstract theorem proving. The challenges stem from the need to identify an abstract level for theorem proving where (less important) information can be temporarily ignored so that a (plan for a) proof of the abstracted problem can be devised to guide the (re)construction of the object-level proof. Contextualization is realized by preserving the logical structures of the formulas of the original representation while pushing the less important subformulas, according to a relevance relation, into the hierarchical subcontexts. This representation allows the problem to be gradually unfolded during the proof search process by hierarchically exploring the subcontexts required to provide support for the hypotheses used in the proof plan. The underlying inference machinery is also equipped with an assertion application module which allows mathematical assertions such as axioms, definitions, theorems, and even global and local assumptions to be applied directly to a proof situation to obtain their logical consequences (from the applied proof situation) and fill in the gaps opened up by an abstract-level proof step. This guarantees that our achievement is two-fold: on the one hand, we are able to carry out effective techniques to search for and construct proofs for a problem; on the other hand, the constructed proof is readily at a sufficiently high level of abstraction so that it can be communicated directly to human mathematicians without undergoing a proof transformation process as required by most machine-generated proofs.