Bi-intuitionistic logic is the extension of intuitionistic logic with exclusion, a connective dual to implication. Cut-elimination in bi-intuitionistic logic is complicated due to the interaction between these two connectives, and various extended sequent calculi, including a display calculus, have been proposed to address this problem.rnIn this paper, we present a new extended sequent calculus DBilnt for bi-intuitionistic logic which uses nested sequents and "deep inference", i.e., inference rules can be applied at any level in the nested sequent. We show that DBilnt can simulate our previous "shallow" sequent calculus LBilnt. In particular, we show that deep inference can simulate the resid-uation rules in the display-like shallow calculus LBilnt. We also consider proof search and give a simple restriction of DBilnt which allows terminating proof search. Thus our work is another step towards addressing the broader problem of proof search in display logic.
展开▼
