:: My Divided Soul ::

On Friday, I will be presenting my A-Exam for admission to candidacy in the PhD program. The work is based on the paper I presented at MKM in Germany. Below is the announcement for my exam and any of you in Ithaca are more than welcome to attend!

Title: A Proof-Theoretic Approach to Hierarchical Math Library Organization
Speaker: Kamal Aboul-Hosn
When: Friday, 19 August 2005 at 11:00am
Location: Rhodes 484

The relationship between theorems and lemmas in mathematical reasoning is often vague. Nevertheless, the decisions we make in creating lemmas provide an inherent hierarchical structure to the statements we prove. Theorem provers generally have flat library structures with no formal distinction between lemmas and theorems. The reasons to distinguish lemmas from theorems in these systems is the same as the reasons in papers: to ascribe various levels of importance and to introduce dependency or scoping relationships. We seek to formalize these notions and provide a proof-theoretic means by which to organize a set of proofs in a hierarchical fashion that reflects this natural structure.

In this talk, we propose a system that represents and manipulates scope formally through the structure of the library of proofs. We provide a representation of proofs, a set of rules to manipulate proofs, and several motivating examples. We believe that the ability to create and manage complex scoping and dependency relationships among proofs will allow systems for formalized mathematics to more accurately reflect the natural structure of mathematical knowledge.