Sciweavers

Share
MKM
2005
Springer

A Proof-Theoretic Approach to Hierarchical Math Library Organization

9 years 8 months ago
A Proof-Theoretic Approach to Hierarchical Math Library Organization
Abstract. The relationship between theorems and lemmas in mathematical reasoning is often vague. No system exists that formalizes the structure of theorems in a mathematical library. Nevertheless, the decisions we make in creating lemmas provide an inherent hierarchical structure to the statements we prove. In this paper, we develop a formal system that organizes theorems based on scope. Lemmas are simply theorems with a local scope. We develop a representation of proofs that captures scope and present a set of proof rules to create and reorganize the scopes of theorems and lemmas. The representation and rules allow systems for formalized mathematics to more accurately reflect the natural structure of mathematical knowledge.
Kamal Aboul-Hosn, Terese Andersen
Added 28 Jun 2010
Updated 28 Jun 2010
Type Conference
Year 2005
Where MKM
Authors Kamal Aboul-Hosn, Terese Andersen
Comments (0)
books