The semester is nearing an end but the project will be continuing over the summer and also next semester.
We hope to have the basics of the proof system ready this semester. We've gotten most of the back-end and a large part of the front end working. We still have to get the hardest rule iteration and de-iteration working and also smooth out some of the other rules. After those are set along with a way to switch proof modes and save and load proofs we should be set with the fundamental software. A couple of added touches to the GUI are needed too.
After that there will be a split in the branches of development. Professor Bram van Heuveln is guiding us through the way of adding features to the project for a classroom environment. Some features to be added is multi-user environments, multi-touch environments, logic short-circuiting, and dual-direction proof modes. Since we are doing everything in java-script the multi user feature can easily be integrated from converting this into a full web app. We also hope to eventually port it into a tablet for the multi-touch use. The logic short-circuiting and dual direction proofs are back-end features that will probably be worked on next semester. An automated proof checker will also be added in over the summer or next summer to allow the user to make sure they're on the right track.
One interesting problem that has come up recently in this project is to create an algorithm that can efficiently tell if two existential graphs are identical. At first, this sounds like simple tree isomorphism, for which linear time algorithms exist, but its actually more complex then that, since tree isomorphism only compares the structure of the graph, and doesn't check if the variables match up properly. If the graph is highly symmetric, there could be a large number(exponential) of ways that the structure of the graph can be matched, which all have to be checked to make sure the variables match up. This would lead to a very expensive algorithm. Fortunately, we have come up with a efficient (n^2 time) algorithm, which is as follows:
Go through a tree and make a list of all unique variables used in that tree
Make sure that the list is identical to the one for the other tree, otherwise they can't match
Assign each variable in the list a number starting from 2
Go through each tree again, and for every node:
If variable n is a child of that node, create a new child node that has n children
If the node was empty (no variables or children) create a child node that has one child
Run a tree isomorphism algorithm on the new trees, if they match, then the original graphs were identical