Sequent Calculus with Zippers
Xiaoshuang Yang

Abstract:
Sequent calculus, a method of formal logical argumentation developed by Gerhard Gentzen, is often used for backward-searching proofs. The success of sequent calculus is significantly influenced by the specific order and choice of inference rules and principal formulas used. The selection of appropriate rules and principal formulas in conventional sequent calculus provers often requires repeated trial and error, which is, however, a time-consuming and memory-intensive process.
To address this issue, in this thesis we develop a sequent calculus prover that employs zippers, a data structure introduced by Gérard Huet in 1997. Zippers can facilitate efficient navigation and modification of hierarchical data structures, such as trees and lists, enabling rapid, targeted updates without the necessity for complete reconstruction. The use of zippers enables the dynamic management of the proof tree, thereby facilitating the application of different rules to specific sequents while maintaining the integrity of the remainder of the proof tree.
We investigate whether the use of zippers can enhance the efficiency of the proof search process and reduce the requisite computational resources. We developed two generic modular provers. One uses the conventional tree representation, and another uses a zipper. For both provers, we then implement the three systems G3C, G3I, and G3K. Subsequently, we make a comparison of their efficiency in terms of run time and memory usage.
Our findings indicate that in some cases where the formula is unprovable, the zipper- based prover consumes a markedly reduced amount of time and memory compared to the tree-based prover. This improvement can be attributed to the fact that the zipper-based prover does not (or almost does not) have to perform garbage collection, which optimises the proof search process by efficiently handling the unfocused components of the proof tree.