Converse \(\textsf{PDL}\) is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse \(\textsf{PDL}\) enjoys the (local) Craig Interpolation Property, with respect to both atomic programs and propositional variables. As a corollary we establish the Beth Definability Property for the logic. Our interpolation proof is based on an adaptation of Maehara’s proof-theoretic method. For this purpose we introduce a sound and complete cyclic sequent system for this logic. This calculus features an analytic cut rule and uses a focus mechanism for recognising successful cycles.

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

Interpolation for Converse PDL

  • Johannes Kloibhofer,
  • Valentina Trucco Dalmas,
  • Yde Venema

摘要

Converse \(\textsf{PDL}\) is the extension of propositional dynamic logic with a converse operation on programs. Our main result states that Converse \(\textsf{PDL}\) enjoys the (local) Craig Interpolation Property, with respect to both atomic programs and propositional variables. As a corollary we establish the Beth Definability Property for the logic. Our interpolation proof is based on an adaptation of Maehara’s proof-theoretic method. For this purpose we introduce a sound and complete cyclic sequent system for this logic. This calculus features an analytic cut rule and uses a focus mechanism for recognising successful cycles.