In this paper, we establish the Craig interpolation theorems of awareness logics by introducing semi-analytic sequent calculi for them. For a semantic clause for an awareness operator, we choose an idea of propositional awareness, which is introduced by Fagin and Halpern and means that an agent is aware of a formula if and only if he is aware of all the atomic propositions contained in it. Although our sequent calculi are not cut-free (due to the fact that our epistemic logic is based on \(\textbf{S5}\) ), we are able to restrict all applications of the rule of cut to semi-analytic ones. This enables us to employ the Maehara method in order to compute Craig interpolants.

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

Craig Interpolation for Awareness Logics

  • Kosuke Udatsu,
  • Katsuhiko Sano

摘要

In this paper, we establish the Craig interpolation theorems of awareness logics by introducing semi-analytic sequent calculi for them. For a semantic clause for an awareness operator, we choose an idea of propositional awareness, which is introduced by Fagin and Halpern and means that an agent is aware of a formula if and only if he is aware of all the atomic propositions contained in it. Although our sequent calculi are not cut-free (due to the fact that our epistemic logic is based on \(\textbf{S5}\) ), we are able to restrict all applications of the rule of cut to semi-analytic ones. This enables us to employ the Maehara method in order to compute Craig interpolants.