ECAI 2004 Conference Paper

[full paper]

Contextualized Abstraction for Assertion-Level Theorem Proving

Quoc Bao VO

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.

Keywords: Proof Planning, Knowledge Representation, Theorem Proving, Meta-Heuristics for AI

Citation: Quoc Bao VO: Contextualized Abstraction for Assertion-Level Theorem Proving. In R.López de Mántaras and L.Saitta (eds.): ECAI2004, Proceedings of the 16th European Conference on Artificial Intelligence, IOS Press, Amsterdam, 2004, pp.1107-1108.