LTG Logic and Theory Group

This project aims to extend the scope of Justification Logic to areas where traditionally Modal Logic has been applied---such as artificial intelligence, multi-agent systems, belief revision, dynamic epistemic logic, knowledge representation, program specification and verification, etc. Despite the popularity of themodal language, it has well-known drawbacks such as the Logical Omniscience Problem and lacks expressivity to deal with the "Justified" part of the famous "Knowledge as Justified True Belief" paradigm. Justification Logic provides a solution by refining the language with syntactic objects that are interpreted as justifications (or proofs, or witnesses) and by introducing a formal machinery for handling them.

The success of Modal Logic is due in part to its versatility: the modal language can be used to describe different phenomena by varying the axioms within the same language. Thus, it is necessary to provide a translation not only for the modal language in general, but also for individual theories in the modal language that are used in various applications. This process of translating modal reasoning into reasoning with justifications is called realization. Unfortunately, the applicability scope of the currently known realization algorithms is greatly narrowed by the fact that they require that the modal logic being translated have a purely syntactic and cut-free proof system.In particular, the most commonly used axiomatic, Hilbert-style representation of modal reasoning is not suitable for these realization algorithms.

Since developing cut-free proof systems has proven to be difficult, this project proposes to develop new cut-tolerant realization techniques. A natural way of achieving this goal is by using the tools of structural proof theory: manipulating symbolic representations of proofs and devising algorithms for obtaining representations with required structural properties. The success of this project will allow automating justification extraction for a wide range of modal logics, especially those that resist cut elimination, including temporal modal logics and public announcement logics.