<p>The notion of reduced sequents plays an important role in proving the decidability of some sequent calculi. A reduced sequent is a sequent without repetitive substructures. While it is straightforward to obtain reduced sequents in Gentzen-style calculi, it is unclear how to obtain them algorithmically in modal display calculi, because modal display calculi contain more complex structures in sequents so that repetitive substructures cannot be recognized at first sight. This paper provides an algorithm to count minimal repetitive substructures in a sequent and to obtain reduced sequents and shows that reduced sequents obtained from a sequent are ‘equivalent’ in a certain sense. Moreover, the paper discusses a proposal for proving the decidability of a modal display calculus and analyzes the reasons why it does not work. The algorithm and proposal may serve as a stepping stone for analyzing calculi with complex structures in sequents and proving their decidability.</p>

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Reduced Sequents in Modal Display Calculi

  • Jinsheng Chen

摘要

The notion of reduced sequents plays an important role in proving the decidability of some sequent calculi. A reduced sequent is a sequent without repetitive substructures. While it is straightforward to obtain reduced sequents in Gentzen-style calculi, it is unclear how to obtain them algorithmically in modal display calculi, because modal display calculi contain more complex structures in sequents so that repetitive substructures cannot be recognized at first sight. This paper provides an algorithm to count minimal repetitive substructures in a sequent and to obtain reduced sequents and shows that reduced sequents obtained from a sequent are ‘equivalent’ in a certain sense. Moreover, the paper discusses a proposal for proving the decidability of a modal display calculus and analyzes the reasons why it does not work. The algorithm and proposal may serve as a stepping stone for analyzing calculi with complex structures in sequents and proving their decidability.