We've implemented tree history functions to store past states of the proof. In existential graphs this is essential because the proof is the series of steps and not contained in any particular state. We've also implemented the first few rules of inference but we haven't connected all of them to the interface yet.
We still need to come up with a method for selecting objects before we can tie some of the rules of inference we've implemented into the interface. We also need to come up with a method for handing insertion of complex structures. I'd prefer to be able to do that without having to use a dialog box or similar.
Currently our proof history system saves the entire tree but we are considering making the history store just the changes instead.