Dynamic Epistemic Logic with justification

Justification Logic is the study of a family of logics used to reason about justified true belief. Dynamic Epistemic Logic is the study of logics used to reason about communication and true belief. This dissertation is a first step in merging these two areas, in that it defines theories for a joint language in which we may reason about communication alongside justified true belief.;After some preliminary matters, we go through a comprehensive survey of Dynamic Epistemic Logic, which primes us for the work at the end of the text. We then move into the core work of the dissertation, where we introduce a number of extensions of existing languages and theories of Justification Logic. Our extensions are all based on the work of Sergei Artemov, who extended the language of propositional logic by the addition of formula-labeling terms. This extension allows us to take a term t and a formula ϕ and form the new formula t:ϕ. The terms have a derivation-compatible structure that allows us to view terms as evidence verifying the truth of the formulas they label, which provides us with a means for reasoning about justified true belief.;We look at extensions of these theories that allow us to reason about evidence admissibility: the new formula t ≫ ϕ lets us express that t is admissible as evidence for ϕ, by which we mean that t may be taken into account when considering the truth of ϕ, though t need not conclusively validate ϕ. A further extension adds a unary modal operator □ that we use to reason about alternative evidence possibilities.;Nominated extensions of the latter languages allow us to express a notion of dynamic evidence introduction, whereby we may introduce a term t as admissible as evidence for ϕ. These extensions lead us to the final chapter of the text, where we combine our various systems of Justification Logic with the framework of Dynamic Epistemic Logic. Such joint theories contribute to the ongoing work aiming to provide a better foundational account of the reasoning of computational social agents.