JavaSplitter. A Java Implementation of Variable Splitting Proof Search

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.