We propose a multi-agent epistemic logic capturing reasoning with degrees of plausibility that agents can assign to a given statement with 1 interpreted as ‘entirely plausible for the agent’ and 0 as ‘completely implausible’ (i.e., the agent knows that the statement is false). We formalise such reasoning in an expansion of Gödel fuzzy logic with an involutive negation and multiple \(\textbf{S5}\) -like modalities. As already Gödel single-modal logics are known to lack the finite model property w.r.t. their standard [0, 1]-valued Kripke semantics, we provide an alternative semantics that allows for the finite model property. For this semantics, we construct a strongly terminating tableaux calculus that allows us to produce finite counter-models of non-valid formulas. We then use the tableaux to show that the validity problem in our logic is \(\textsf{PSpace}\) -complete when there are two or more agents, and \(\textsf{coNP}\) -complete for the single-agent case.

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

Tableaux for Epistemic Gödel Logic

  • Marta Bílková,
  • Thomas Ferguson,
  • Daniil Kozhemiachenko

摘要

We propose a multi-agent epistemic logic capturing reasoning with degrees of plausibility that agents can assign to a given statement with 1 interpreted as ‘entirely plausible for the agent’ and 0 as ‘completely implausible’ (i.e., the agent knows that the statement is false). We formalise such reasoning in an expansion of Gödel fuzzy logic with an involutive negation and multiple \(\textbf{S5}\) -like modalities. As already Gödel single-modal logics are known to lack the finite model property w.r.t. their standard [0, 1]-valued Kripke semantics, we provide an alternative semantics that allows for the finite model property. For this semantics, we construct a strongly terminating tableaux calculus that allows us to produce finite counter-models of non-valid formulas. We then use the tableaux to show that the validity problem in our logic is \(\textsf{PSpace}\) -complete when there are two or more agents, and \(\textsf{coNP}\) -complete for the single-agent case.