modal logic; justification logic; structural proof theory; non-monotonic reasoning; Epistemic Logic; Sequent Calculus; Circularity; Logic of Proofs; Justification Extraction
Fitting Melvin, Kuznets Roman (2015), Modal interpolation via nested sequents, in Annals of Pure and Applied Logic
, 166(3), 274-305.
Artemov Sergei, Kuznets Roman (2014), Logical Omniscience As Infeasibility, in Annals of Pure and Applied Logic
, 165(1), 6-25.
Bucheli Samuel, Kuznets Roman, Studer Thomas (2014), Realizing Public Announcements by Justifications, in Journal of Computer and System Sciences
, 80(6), 1046-1066.
Bucheli Samuel, Kuznets Roman, Studer Thomas (2013), Decidability for Justification Logics Revisited, in Richter Frank, Bezhanishvili Guram , Marra Vincenzo , Löbner Sebastian (ed.), Springer, Berlin Heidelberg, 166-181.
Kuznets Roman, Studer Thomas (2013), Update as Evidence: Belief Expansion, in Nerode Anil, Artemov Sergei (ed.), Springer, Berlin Heidelberg, 266-279.
Kuznets Roman, Studer Thomas (2012), Justifications, Ontology, and Conservativity, in Braüner Torben , Bolander Thomas , Moss Lawrence , Ghilardi Silvio (ed.), College Publications, London, 437-458.
Goetschi Remo, Kuznets Roman (2012), Realization for Justification Logics via Nested Sequents: Modularity through Embedding, in Annals of Pure and Applied Logic
, 163(9), 1271-1298.
Bucheli Samuel, Kuznets Roman, Studer Thomas (2011), Justifications for Common Knowledge, in Journal of Applied Non-Classical Logics
, 21(1), 35-60.
Bucheli Samuel, Kuznets Roman, Studer Thomas (2011), Partial Realization in Dynamic Justification Logic, in de Queiroz Ruy, Beklemishev Lev (ed.), Springer, Berlin Heidelberg, 35-51.
Giese Martin , Kuznets Roman (ed.) (2011), TABLEAUX 2011: Workshops, Tutorials, and Short Papers
Modal logic is a convenient way of formalizing a wide range of notions: permission/ obligation (deontic logic), time relations (temporal logic), knowledge (epistemic logic), belief (doxastic logic), etc. Although epistemic and doxastic modal logics are successfully used in artificial intelligence to model various modes of reasoning, agent interaction, and belief revision, there are also clear indications that in some instances of these applications modal language is not optimal. In such cases, justification logic has often proved useful in supplying the missing formal machinery. One of the weaknesses of epistemic modal logics, for instance, is the phenomenon of Logical Omniscience: agents whose reasoning abilities are described by modal principles unrealistically possess knowledge of all logical truths and of all logical consequences of the facts they know. Justification logic provides a more nuanced way of representing knowledge by introducing syntactic methods for handling justifications, which has proved fruitful in tackling the Logical Omniscience Problem. Modal language is also not expressive enough to faithfully capture the philosophical discussions about the nature of knowledge in mainstream epistemology, e.g., the discussions prompted by the famous Gettier examples that question the notion of knowledge as justified true belief, which can be traced back to Plato. In these examples, a belief is true and justified but the facts that make it true contradict the internal reasoning used by the agent to justify the belief; as a result, treating such a belief as knowledge seems counterintuitive. Where logical methods developed in formal epistemology remain powerless, justification language has succeeded in formalizing and analyzing these and similar epistemic paradoxes.While successes of justification logic in epistemic studies are encouraging, there is a serious obstacle that impedes further applications: the lack of a universal algorithm for justification extraction, i.e., for translating modal descriptions and arguments into a more precise language of explicit justifications. The existing justification extraction methods are highly sensitive to the formalism used to describe the laws of modal reasoning. Not only is a suitable formalism required, but it must also possess a valuable but rare property called cut-elimination (in the proofs-as-programs paradigm, the process of cut-elimination corresponds to program execution via an elimination of implicit descriptions; a mathematical analog is a removal of intermediate lemmas in a proof). While translating a modal argument into a suitable type of formalism rarely presents serious challenges, no general methods exist for designing formalisms that are cut-free.As a result, modeling with justifications currently relies on luck (the existence of a suitable cut-free formalism) or ad hoc tricks. Since a design of cut-free systems has remained elusive for more than half a century, the idea of this project is to develop new cut-tolerant techniques of justification extraction. A natural way of achieving this goal is to use the instrumentarium of structural proof theory: manipulating symbolic representations of proofs and devising algorithms for obtaining representations with required structural properties. In particular, studying modal proofs that are structurally suitable for justification extraction should pave way to concise and expressive sets of operations on justifications sufficient for representing various modes of reasoning, including non-monotonic reasoning.Equipped with general techniques of justification extraction, justification logic will become a reliable and handy tool in the arsenal of formal epistemology and will serve to strengthen the ties with its philosophical counterpart, mainstream epistemology. Further, the developed techniques will extend the reach of justification logic to temporal reasoning used in program verification, a development currently blocked by a lack of basic cut-free formulations for major temporal modal logics. The invigorated justification logic should prove an effective tool for studies in belief revision, knowledge representation, game theory, multi-agent systems, and automated proof search.