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. | 
