Abstract
This thesis describes the design and implementation of JavaSplitter, a
prototype 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 variable
sharing derivations, and to keep track of how variables are split into
different branches of a derivation. A graph representation of the
indices occurring in a skeleton and operations on this graph are used
to determine when splitting of such variables is sound.
The design and implementation of the data structures and operations
necessary for the proof search procedures are described. Further, the
three modes of proof search are compared with regard to number of
steps used to reach a proof for a set of valid input sequents.