Jim Burton and Sven Linker of the University of Brighton visited our project last week.
Jim and Sven work with set representations such as Venn, Euler and Spider diagrams. Their project last week was to use existing implementations of inference rules for Venn/Euler diagrams to create an Openbox plugin implementing these rules.
With just a couple of days work Jim and Sven were able to achieve this task. They used an graphical editor component for Venn/Euler diagrams written by Nik Swoboda which allows them to draw and edit diagrams. The graphical editor produces a model, also designed by Nik.
To implement their logic, Jim and Sven first wrote code that translates from Nik's model to the model required by their existing code. They then wrapped the code for each of their existing inference rules in a shell which takes the support diagrams (in Nik's model), translates into their model, runs the inference rule, and finally compares the result of their inference with the translation of the purported conclusion of the inference. Since this shell also implemented the Openbox's inference rule API, they were then able to plug these inference rules into the Openbox.
This work demonstrates that the Openbox can be used to mix-and-match plugins implemented by different authors. Jim and Sven plan to use the resulting proof environment as a teaching tool at their Winter School on Diagrammatic Reasoning at the end of the year (a second iteration of this event).