My PhD work will focus on Network Visualization. I will post my progress made on related projects on this page. A recent newspaper article discussing the project I'm working on can be found here.
Throughout my tenure as a Master's student I worked on implementing and deriving algorithms related to the equational theory of allegories. The first step of my research work was to implement a proof system that allows users to complete proofs as if they were doing them by hand. This began the development of a proof assistant called RelAPS ("Relation Algebraic Proof System").
The RelAPS system has several aspects that are worth mentioning. First of all, a user may define custom (nullary, unary and binary) operations. These operations may be combined with arbitrary axioms to produce new theories. The base theory of the system is the theory of allegories which consists of the following operations: the identity, converse, intersection and composition. Once the above functionality was implemented, I focused on implemeting a decision procedure for the equational theory of allegories. This algorithm was previously described in a PhD thesis by Claudio Gutierrez (PhD). It was this algorithm that provided motivation for the main focus of my MSc research. My MSc research was geared towards providing an algorithm that will allow proof systems to automatically derive provable equations in the theory of allegories. The algorithm is an extension of the decision procedure alluded to above. I will post a link to my thesis once it is approved (later this summer). Click here or click the screenshot above for a larger image. Click here for the RelAPS User Manual.
The image viewer below contains screenshots of various projects I worked on throughout my BSc. Most of the projects were major portions of classes I took. One of them was part of a major group project that took an entire semester to develop. These projects can essentially be grouped into three areas: VST Development, Graphics, and Graphing. |