This thesis describes the design and implementation of JavaSplitter, aprototype incremental proof search engine based on a variable splitting sequent calculus. The prover also includes modes for variable pure derivations, and for variable sharing derivations without splitting.
The splitting calculus uses an index system to achieve variablesharing derivations, and to keep track of how variables are split intodifferent branches of a derivation. A graph representation of theindices occurring in a skeleton and operations on this graph are usedto determine when splitting of such variables is sound.
The design and implementation of the data structures and operationsnecessary for the proof search procedures are described. Further, thethree modes of proof search are compared with regard to number ofsteps used to reach a proof for a set of valid input sequents.