@article {Kuznets01062016,
title = {Weak arithmetical interpretations for the Logic of Proofs},
journal = {Logic Journal of IGPL},
volume = {24},
number = {3},
year = {2016},
pages = {424-440},
abstract = {Artemov established an arithmetical interpretation for the Logics of Proofs LPCS, which yields a classical provability semantics for the modal logic S4. The Logics of Proofs are parameterized by so-called constant specifications CS, stating which axioms can be used in the reasoning process, and the arithmetical interpretation relies on constant specifications being finite. In this article, we remove this restriction by introducing weak arithmetical interpretations that are sound and complete for a wide class of constant specifications, including infinite ones. In particular, they interpret the full Logic of Proofs LP.},
url = {http://www.iam.unibe.ch/ltgpub/2016/kust16.pdf},
author = {Roman Kuznets and Thomas Studer}
}
@article {fkm15,
title = {Modal interpolation via nested sequents},
journal = {Annals of pure and applied logic},
volume = {166},
number = {3},
year = {2015},
month = {March},
pages = {274-305},
publisher = {Elsevier},
abstract = {The main method of proving the Craig Interpolation Property (CIP) constructively uses cut-free sequent proof systems. Until now, however, no such method has been known for proving the CIP using more general sequent-like proof formalisms, such as hypersequents, nested sequents, and labelled sequents. In this paper, we start closing this gap by presenting an algorithm for proving the CIP for modal logics by induction on a nested-sequent derivation. This algorithm is applied to all the logics of the so-called modal cube.},
url = {http://www.iam.unibe.ch/ltgpub/2015/fkm15.pdf},
author = {Melvin Fitting and Roman Kuznets}
}
@article {ak13,
title = {Logical Omniscience As Infeasibility},
journal = {Annals of Pure and Applied Logic},
volume = {165},
number = {1},
year = {2014},
pages = {6-25},
abstract = {Abstract Logical theories for representing knowledge are often plagued by the so-called Logical Omniscience Problem. The problem stems from the clash between the desire to model rational agents, which should be capable of simple logical inferences, and the fact that any logical inference, however complex, almost inevitably consists of inference steps that are simple enough. This contradiction points to the fruitlessness of trying to solve the Logical Omniscience Problem qualitatively if the rationality of agents is to be maintained. We provide a quantitative solution to the problem compatible with the two important facets of the reasoning agent: rationality and resource boundedness. More precisely, we provide a test for the logical omniscience problem in a given formal theory of knowledge. The quantitative measures we use are inspired by the complexity theory. We illustrate our framework with a number of examples ranging from the traditional implicit representation of knowledge in modal logic to the language of justification logic, which is capable of spelling out the internal inference process. We use these examples to divide representations of knowledge into logically omniscient and not logically omniscient, thus trying to determine how much information about the reasoning process needs to be present in a theory to avoid logical omniscience.},
issn = {0168-0072},
doi = {http://dx.doi.org/10.1016/j.apal.2013.07.003},
url = {http://www.iam.unibe.ch/ltgpub/2013/ak13.pdf},
author = {Sergei Artemov and Roman Kuznets}
}
@article {bks12a,
title = {Realizing Public Announcements by Justifications},
journal = {Journal of Computer and System Sciences},
volume = {80},
number = {6},
year = {2014},
pages = {1046-1066},
abstract = {Modal public announcement logics study how beliefs change after public announcements. However, these logics cannot express the reason for a new belief. Justification logics fill this gap since they can formally represent evidence and justifications for an agent{\textquoteright}s belief. We present ${\sf OPAL(K)}$ and ${\sf JPAL(K)}$, two alternative justification counterparts of Gerbrandy{\textendash}Groeneveld{\textquoteright}s public announcement logic ${\sf PAL(K)}$. We show that ${\sf PAL(K)}$ is the forgetful projection of both ${\sf OPAL(K)}$ and ${\sf JPAL(K)}$. We also establish that ${\sf JPAL(K)}$ partially realizes ${\sf PAL(K)}$. The question whether a similar result holds for ${\sf OPAL(K)}$ is still open.},
keywords = {Belief revision, Dynamic epistemic logic, justification logic, Public announcements},
doi = {10.1016/j.jcss.2014.04.001},
url = {http://www.iam.unibe.ch/ltgpub/2012/bks12a.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer}
}
@inbook {bks13,
title = {Decidability for Justification Logics Revisited},
booktitle = {Logic, Language, and Computation, 9th~International Tbilisi Symposium on Logic, Language, and Computation, TbiLLC~2011, Kutaisi, Georgia, September 26-30, 2011, Revised Selected Papers},
volume = {7758},
year = {2013},
pages = {166-181},
publisher = {Springer},
organization = {Springer},
abstract = {Justification logics are propositional modal-like logics that instead of statements \emph{$A$~is known} include statements of the form \emph{$A$~is known for reason~$t$} where the term~$t$ can represent an informal justification for~$A$ or a formal proof of~$A$. In our present work, we introduce model-theoretic tools, namely: filtrations and a certain form of generated submodels, in the context of justification logic in order to obtain decidability results. Apart from reproving already known results in a uniform way, we also prove new results. In particular, we use our submodel construction to establish decidability for a justification logic with common knowledge for which so far no decidability proof was available.},
keywords = {decidability, filtration, justification logic},
doi = {10.1007/978-3-642-36976-6_12},
url = {http://www.iam.unibe.ch/ltgpub/2013/bks13.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Guram Bezhanishvili and Sebastian L{\"o}bner and Vincenzo Marra and Frank Richter}
}
@inbook {ks13,
title = {Update as Evidence: Belief Expansion},
booktitle = {Logical Foundations of Computer Science, International Symposium, LFCS~2013, San Diego, CA, USA, January 6{\textendash}8, 2013, Proceedings},
series = {Lecture Notes in Computer Science},
volume = {7734},
year = {2013},
pages = {266-279},
publisher = {Springer},
organization = {Springer},
abstract = {We introduce a justification logic with a novel constructor for evidence terms, according to which the new information itself serves as evidence for believing it. We provide a sound and complete axiomatization for belief expansion and minimal change and explain how the minimality can be graded according to the strength of reasoning. We also provide an evidential analog of the Ramsey axiom.},
doi = {10.1007/978-3-642-35722-0_19},
url = {http://www.iam.unibe.ch/ltgpub/2013/ks13.pdf},
author = {Roman Kuznets and Thomas Studer},
editor = {Sergei Artemov and Nerode, Anil}
}
@conference {1311,
title = {Justifications, Ontology, and Conservativity},
booktitle = {Advances in Modal Logic, volume 9},
year = {2012},
pages = {437-458},
publisher = {College Publications},
organization = {College Publications},
url = {http://www.iam.unibe.ch/ltgpub/2012/ks12.pdf},
author = {Roman Kuznets and Thomas Studer},
editor = {Thomas Bolander and Torben Bra{\"u}ner and Silvio Ghilardi and Lawrence Moss}
}
@article {1313,
title = {Lower complexity bounds in justification logic},
journal = {Annals of Pure and Applied Logic},
volume = {163},
year = {2012},
note = {Published online November~2011},
pages = {888-905},
abstract = {Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in~NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound. The proof method is then extended to provide a uniform proof that the corresponding full pure justification logics are $\Pi^p_2$-hard, reproving and generalizing an earlier result by Milnikel.},
keywords = {Logic of Proofs},
doi = {10.1016/j.apal.2011.09.010},
url = {http://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/APAL09_final.pdf},
author = {Buss, Samuel R. and Roman Kuznets}
}
@article {1306,
title = {Realization for Justification Logics via Nested Sequents: Modularity through Embedding},
journal = {Annals of Pure and Applied Logic},
volume = {163},
year = {2012},
month = {September},
pages = {1271-1298},
doi = {10.1016/j.apal.2012.02.002},
url = {http://www.iam.unibe.ch/ltgpub/2012/gk12.pdf},
author = {Remo Goetschi and Roman Kuznets}
}
@article {1321,
title = {Justifications for Common Knowledge},
journal = {Journal of Applied Non-classical Logics},
volume = {21},
year = {2011},
note = {To appear, 2011},
pages = {35-60},
doi = {10.3166/JANCL.21.35-60},
url = {http://www.iam.unibe.ch/ltgpub/2011/bks11a.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Valentin Goranko and Wojtek Jamroga}
}
@conference {1322,
title = {Partial Realization in Dynamic Justification Logic},
booktitle = {Logic, Language, Information and Computation, 18th International Workshop, WoLLIC 2011, Philadelphia, PA, USA, May 18-20, 2011, Proceedings},
series = {Lecture Notes in Artificial Intelligence},
volume = {6642},
year = {2011},
pages = {35-51},
doi = {10.1007/978-3-642-20920-8_9},
url = {http://www.iam.unibe.ch/ltgpub/2011/bks11b.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Lev Beklemishev and de Queiroz, Ruy}
}
@conference {1342,
title = {A Syntactic Realization Theorem for Justification Logics},
booktitle = {Advances in Modal Logic, Volume 8},
year = {2010},
pages = {39-58},
publisher = {College Publications},
organization = {College Publications},
abstract = {Justification logics are refinements of modal logics where modalities are replaced by justification terms. They are connected to modal logics via so-called realization theorems. We present a syntactic proof of a single realization theorem that uniformly connects all the normal modal logics formed from the axioms~$\mathsf{d}$, $\mathsf{t}$, $\mathsf{b}$, $\mathsf{4}$, and~$\mathsf{5}$ with their justification counterparts. The proof employs cut-free nested sequent systems together with Fitting{\textquoteright}s realization merging technique. We further strengthen the realization theorem for $\mathsf{KB5}$~and~$\mathsf{S5}$ by showing that the positive introspection operator is superfluous.},
keywords = {realization theorem},
url = {http://www.iam.unibe.ch/ltgpub/2010/bgk10.pdf},
author = {Kai Br{\"u}nnler and Remo Goetschi and Roman Kuznets},
editor = {Lev Beklemishev and Valentin Goranko and Valentin Shehtman}
}
@article {1327,
title = {Explicit Evidence Systems with Common Knowledge},
year = {2010},
month = {may},
publisher = {arXiv.org},
type = {E-print},
abstract = {Justification logics are epistemic logics that explicitly include justifications for the agents{\textquoteright} knowledge. We develop a multi-agent justification logic with evidence terms for individual agents as well as for common knowledge. We define a Kripke-style semantics that is similar to Fitting{\textquoteright}s semantics for the Logic of Proofs~$\mathsf{LP}$. We show the soundness, completeness, and finite model property of our multi-agent justification logic with respect to this Kripke-style semantics. We demonstrate that our logic is a conservative extension of Yavorskaya{\textquoteright}s minimal bimodal explicit evidence logic, which is a two-agent version of~$\mathsf{LP}$. We discuss the relationship of our logic to the multi-agent modal logic~$\mathsf{S4}$ with common knowledge. Finally, we give a brief analysis of the coordinated attack problem in the newly developed language of our logic.},
url = {http://arxiv.org/abs/1005.0484},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer}
}
@conference {1340,
title = {Justified Belief Change},
booktitle = {Proceedings of the Second ILCLI International Workshop on Logic and Philosphy of Knowledge, Communication and Action (LogKCA-10)},
year = {2010},
pages = {135-155},
publisher = {University of the Basque Country Press},
organization = {University of the Basque Country Press},
abstract = {Justification Logic is a framework for reasoning about evidence and justification. Public Announcement Logic is a framework for reasoning about belief changes caused by public announcements. This paper develops JPAL, a dynamic justification logic of public announcements that corresponds to the modal theory of public announcements due to Gerbrandy and Groeneveld. JPAL allows us to reason about evidence brought about by and changed by Gerbrandy{\textendash}Groeneveld-style public announcements.},
url = {http://www.iam.unibe.ch/ltgpub/2010/bkrss10.pdf},
author = {Samuel Bucheli and Roman Kuznets and Renne, Bryan and Sack, Joshua and Thomas Studer},
editor = {Arrazola, Xabier and Ponte, Mar\'{\i}a}
}
@article {1328,
title = {Self-Referential Justifications in Epistemic Logic},
journal = {Theory of Computing Systems},
volume = {46},
year = {2010},
month = {may},
pages = {636-661},
abstract = {This paper is devoted to the study of self-referential proofs and/or justifications, i.e., valid proofs that prove statements about these same proofs. The goal is to investigate whether such self-referential justifications are present in the reasoning described by standard modal epistemic logics such as~$\mathsf{S4}$. We argue that the modal language by itself is too coarse to capture this concept of self-referentiality and that the language of justification logic can serve as an adequate refinement. We consider well-known modal logics of knowledge/belief and show, using explicit justifications, that~$\mathsf{S4}$, $\mathsf{D4}$, $\mathsf{K4}$, and~$\mathsf{T}$ with their respective justification counterparts~$\mathsf{LP}$, $\mathsf{JD4}$, $\mathsf{J4}$, and~$\mathsf{JT}$ describe knowledge that is self-referential in some strong sense. We also demonstrate that self-referentiality can be avoided for~$\mathsf{K}$ and~$\mathsf{D}$. In order to prove the former result, we develop a machinery of minimal evidence functions used to effectively build models for justification logics. We observe that the calculus used to construct the minimal functions axiomatizes the reflected fragments of justification logics. We also discuss difficulties that result from an introduction of negative introspection.},
keywords = {self-referentiality},
doi = {10.1007/s00224-009-9209-3},
url = {http://www.iam.unibe.ch/ltgpub/2010/kuz10.pdf},
author = {Roman Kuznets}
}
@conference {1337,
title = {Two Ways to Common Knowledge},
booktitle = {Proceedings of the 6th~Workshop on Methods for Modalities (M4M{\textendash}6~2009), Copenhagen, Denmark, 12{\textendash}14 November 2009},
series = {Electronic Notes in Theoretical Computer Science},
year = {2010},
pages = {83-98},
publisher = {Elsevier},
organization = {Elsevier},
abstract = {It is not clear what a system for evidence-based common knowledge should look like if common knowledge is treated as a greatest fixed point. This paper is a preliminary step towards such a system. We argue that the standard induction rule is not well suited to axiomatize evidence-based common knowledge. As an alternative, we study two different deductive systems for the logic of common knowledge. The first system makes use of an induction axiom whereas the second one is based on co-inductive proof theory. We show the soundness and completeness for both systems.},
keywords = {proof theory},
doi = {10.1016/j.entcs.2010.04.007},
url = {http://www.iam.unibe.ch/ltgpub/2010/bks10a.pdf},
author = {Samuel Bucheli and Roman Kuznets and Thomas Studer},
editor = {Thomas Bolander and Torben Bra{\"u}ner}
}
@conference {1364,
title = {A Note on the Use of Sum in the Logic of Proofs},
booktitle = {Proceedings of the 7th~Panhellenic Logic Symposium},
year = {2009},
pages = {99-103},
publisher = {Patras University Press},
organization = {Patras University Press},
address = {Patras University, Greece},
url = {http://www.iam.unibe.ch/ltgpub/2009/kuz09b.pdf},
author = {Roman Kuznets},
editor = {Costas Drossos and Pavlos Peppas and Constantine Tsinakis}
}
@conference {1349,
title = {Logical Omniscience as a Computational Complexity Problem},
booktitle = {Theoretical Aspects of Rationality and Knowledge, Proceedings of the Twelfth Conference (TARK~2009)},
year = {2009},
pages = {14-23},
publisher = {ACM},
organization = {ACM},
address = {Stanford University, California},
abstract = {The logical omniscience feature assumes that an epistemic agent knows all logical consequences of her assumptions. This paper offers a general theoretical framework that views logical omniscience as a computational complexity problem. We suggest the following approach: we assume that the knowledge of an agent is represented by an epistemic logical system~$E$; we call such an agent \emph{not logically omniscient} if for any valid knowledge assertion~$\mathcal{A}$ of type \emph{$F$~is known}, a proof of~$F$ in~$E$ can be found in polynomial time in the size of~$\mathcal{A}$. We show that agents represented by major modal logics of knowledge and belief are logically omniscient, whereas agents represented by justification logic systems are not logically omniscient with respect to \emph{$t$~is a justification for~$F$}.},
doi = {10.1145/1562814.1562821},
url = {http://www.iam.unibe.ch/ltgpub/2009/ak09.pdf},
author = {Sergei Artemov and Roman Kuznets},
editor = {Aviad Heifetz}
}
@conference {1359,
title = {The NP-completeness of reflected fragments of justification logics},
booktitle = {Proceedings of Symposium on Logical Foundations of Computer Science (LFCS{\textquoteright}09)},
series = {Lecture Notes in Computer Science},
volume = {5407},
year = {2009},
pages = {122-136},
abstract = {Justification Logic studies epistemic and provability phenomena by introducing justifications/proofs into the language in the form of justification terms. Pure justification logics serve as counterparts of traditional modal epistemic logics, and hybrid logics combine epistemic modalities with justification terms. The computational complexity of pure justification logics is typically lower than that of the corresponding modal logics. Moreover, the so-called reflected fragments, which still contain complete information about the respective justification logics, are known to be in~NP for a wide range of justification logics, pure and hybrid alike. This paper shows that, under reasonable additional restrictions, these reflected fragments are NP-complete, thereby proving a matching lower bound.},
doi = {10.1007/978-3-540-92687-0_9},
url = {http://www.iam.unibe.ch/ltgpub/2009/bk09.pdf},
author = {Buss, Samuel R. and Roman Kuznets},
editor = {Sergei Artemov and Nerode, Anil}
}