Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Uniform Agent-interpolation of Distributed Knowledge

Youan Su

TL;DR

This paper develops the sequent calculi provided in Murai and Sano (2020), combining with the methods studied by B{\'\i}lkov{\'a} (2007) to show the uniform interpolation for epistemic logic $\mathbf{K}$, $\mathbf{KD}$ and $\mathbf{KT}$ with distributed knowledge.

Abstract

Uniform interpolation property (UIP) is a strengthening of Craig interpolation property. It can be understood as the definability of propositional quantifiers. This paper develops the sequent calculi provided in Murai and Sano (2020), combining with the methods studied by B{\'ı}lkov{á} (2007) to show the uniform interpolation for epistemic logic $\mathbf{K}$, $\mathbf{KD}$ and $\mathbf{KT}$ with distributed knowledge. A purely syntactic algorithm is presented to determine a uniform interpolant formula. In the definition of an interpolant formula, not only propositional variables but also agent symbols are taken into consideration.

Uniform Agent-interpolation of Distributed Knowledge

TL;DR

This paper develops the sequent calculi provided in Murai and Sano (2020), combining with the methods studied by B{\'\i}lkov{\'a} (2007) to show the uniform interpolation for epistemic logic , and with distributed knowledge.

Abstract

Uniform interpolation property (UIP) is a strengthening of Craig interpolation property. It can be understood as the definability of propositional quantifiers. This paper develops the sequent calculi provided in Murai and Sano (2020), combining with the methods studied by B{\'ı}lkov{á} (2007) to show the uniform interpolation for epistemic logic , and with distributed knowledge. A purely syntactic algorithm is presented to determine a uniform interpolant formula. In the definition of an interpolant formula, not only propositional variables but also agent symbols are taken into consideration.
Paper Structure (9 sections, 26 theorems, 17 equations, 3 tables)

This paper contains 9 sections, 26 theorems, 17 equations, 3 tables.

Table of Contents

  1. introduction
  2. Syntax
  3. Sequent Calculi and Structural Properties
  4. Finite model property
  5. Main theorem of $\mathsf{G}\mathbf{(K}_D)$ and $\mathsf{G}\mathbf{(KD}_D)$
  6. UIP in Logic $\mathbf{KT}_D$
  7. Proof-theoretic properties of sequent calculus
  8. Main theorem of $\mathsf{G}\mathbf{(KT}_D)$
  9. Conclusion and Future Direction

Key Result

Proposition 3.5

An arbitrary backward proof-search in $\mathsf{G}\mathbf{(K}_D)$ and $\mathsf{G}\mathbf{(KD}_D)$ always terminates.

Theorems & Definitions (61)

  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 3.1
  • Definition 3.2
  • Definition 3.3
  • Definition 3.4
  • Proposition 3.5
  • Definition 3.6
  • ...and 51 more