01037nas a2200133 4500008004100000245006200041210006200103300001200165490000700177520063000184100001900814700001900833856005100852 2016 eng d00aWeak arithmetical interpretations for the Logic of Proofs0 aWeak arithmetical interpretations for the Logic of Proofs a424-4400 v243 aArtemov 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.1 aKuznets, Roman1 aStuder, Thomas uhttp://www.iam.unibe.ch/ltgpub/2016/kust16.pdf00932nas a2200145 4500008004100000245004400041210004400085260002000129300001200149490000800161520052800169100002000697700001900717856005000736 2015 eng d00aModal interpolation via nested sequents0 aModal interpolation via nested sequents bElseviercMarch a274-3050 v1663 aThe 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.1 aFitting, Melvin1 aKuznets, Roman uhttp://www.iam.unibe.ch/ltgpub/2015/fkm15.pdf01758nas a2200145 4500008004100000022001400041245004100055210004100096300000900137490000800146520137000154100002001524700001901544856004901563 2014 eng d a0168-007200aLogical Omniscience As Infeasibility0 aLogical Omniscience As Infeasibility a6-250 v1653 aAbstract 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.1 aArtemov, Sergei1 aKuznets, Roman uhttp://www.iam.unibe.ch/ltgpub/2013/ak13.pdf01259nas a2200193 4500008004100000245005300041210005300094300001400147490000700161520069100168653002000859653002800879653002400907653002500931100002000956700001900976700001900995856005101014 2014 eng d00aRealizing Public Announcements by Justifications0 aRealizing Public Announcements by Justifications a1046-10660 v803 aModal 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's belief. We present ${\sf OPAL(K)}$ and ${\sf JPAL(K)}$, two alternative justification counterparts of Gerbrandy–Groeneveld'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.10aBelief revision10aDynamic epistemic logic10ajustification logic10aPublic announcements1 aBucheli, Samuel1 aKuznets, Roman1 aStuder, Thomas uhttp://www.iam.unibe.ch/ltgpub/2012/bks12a.pdf01408nas a2200241 4500008004100000245005200041210005200093260001300145300001200158490000900170520073600179653001700915653001500932653002400947100002000971700001900991700001901010700002501029700002301054700002001077700001901097856005001116 2013 eng d00aDecidability for Justification Logics Revisited0 aDecidability for Justification Logics Revisited bSpringer a166-1810 v77583 aJustification 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.10adecidability10afiltration10ajustification logic1 aBucheli, Samuel1 aKuznets, Roman1 aStuder, Thomas1 aBezhanishvili, Guram1 aLöbner, Sebastian1 aMarra, Vincenzo1 aRichter, Frank uhttp://www.iam.unibe.ch/ltgpub/2013/bks13.pdf00847nas a2200169 4500008004100000245004100041210004000082260001300122300001200135490000900147520039700156100001900553700001900572700002000591700001700611856004900628 2013 eng d00aUpdate as Evidence: Belief Expansion0 aUpdate as Evidence Belief Expansion bSpringer a266-2790 v77343 aWe 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.1 aKuznets, Roman1 aStuder, Thomas1 aArtemov, Sergei1 aNerode, Anil uhttp://www.iam.unibe.ch/ltgpub/2013/ks13.pdf00513nas a2200169 4500008004100000245004900041210004700090260002500137300001200162100001900174700001900193700002100212700002100233700002100254700001900275856004900294 2012 eng d00aJustifications, Ontology, and Conservativity0 aJustifications Ontology and Conservativity bCollege Publications a437-4581 aKuznets, Roman1 aStuder, Thomas1 aBolander, Thomas1 aBraüner, Torben1 aGhilardi, Silvio1 aMoss, Lawrence uhttp://www.iam.unibe.ch/ltgpub/2012/ks12.pdf01442nas a2200145 4500008004100000245005100041210005100092300001200143490000800155520099900163653002001162100002001182700001901202856007501221 2012 eng d00aLower complexity bounds in justification logic0 aLower complexity bounds in justification logic a888-9050 v1633 aJustification 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.10aLogic of Proofs1 aBuss, Samuel, R1 aKuznets, Roman uhttp://www.math.ucsd.edu/~sbuss/ResearchWeb/rlp_lower/APAL09_final.pdf00458nas a2200133 4500008004100000245009100041210006900132260001400201300001400215490000800229100001900237700001900256856004900275 2012 eng d00aRealization for Justification Logics via Nested Sequents: Modularity through Embedding0 aRealization for Justification Logics via Nested Sequents Modular cSeptember a1271-12980 v1631 aGoetschi, Remo1 aKuznets, Roman uhttp://www.iam.unibe.ch/ltgpub/2012/gk12.pdf00447nas a2200157 4500008004100000245004000041210004000081300001000121490000700131100002000138700001900158700001900177700002200196700002000218856005100238 2011 eng d00aJustifications for Common Knowledge0 aJustifications for Common Knowledge a35-600 v211 aBucheli, Samuel1 aKuznets, Roman1 aStuder, Thomas1 aGoranko, Valentin1 aJamroga, Wojtek uhttp://www.iam.unibe.ch/ltgpub/2011/bks11a.pdf00475nas a2200157 4500008004100000245005500041210005500096300001000151490000900161100002000170700001900190700001900209700002100228700001700249856005100266 2011 eng d00aPartial Realization in Dynamic Justification Logic0 aPartial Realization in Dynamic Justification Logic a35-510 v66421 aBucheli, Samuel1 aKuznets, Roman1 aStuder, Thomas1 aBeklemishev, Lev1 aQueiroz, Ruy uhttp://www.iam.unibe.ch/ltgpub/2011/bks11b.pdf01279nas a2200193 4500008004100000245006100041210006100102260002500163300001000188520069000198653002400888100001900912700001900931700001900950700002100969700002200990700002301012856005001035 2010 eng d00aA Syntactic Realization Theorem for Justification Logics0 aA Syntactic Realization Theorem for Justification Logics bCollege Publications a39-583 aJustification 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'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.10arealization theorem1 aBrünnler, Kai1 aGoetschi, Remo1 aKuznets, Roman1 aBeklemishev, Lev1 aGoranko, Valentin1 aShehtman, Valentin uhttp://www.iam.unibe.ch/ltgpub/2010/bgk10.pdf01271nas a2200133 4500008004100000245005200041210005200093260001900145520088000164100002001044700001901064700001901083856003501102 2010 eng d00aExplicit Evidence Systems with Common Knowledge0 aExplicit Evidence Systems with Common Knowledge barXiv.orgcmay3 aJustification logics are epistemic logics that explicitly include justifications for the agents' 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'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'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.1 aBucheli, Samuel1 aKuznets, Roman1 aStuder, Thomas uhttp://arxiv.org/abs/1005.048401023nas a2200193 4500008004100000245002800041210002800069260004300097300001200140520049200152100002000644700001900664700001700683700001700700700001900717700002100736700002000757856005200777 2010 eng d00aJustified Belief Change0 aJustified Belief Change bUniversity of the Basque Country Press a135-1553 aJustification 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–Groeneveld-style public announcements.1 aBucheli, Samuel1 aKuznets, Roman1 aRenne, Bryan1 aSack, Joshua1 aStuder, Thomas1 aArrazola, Xabier1 aPonte, Mar\'ıa uhttp://www.iam.unibe.ch/ltgpub/2010/bkrss10.pdf01735nas a2200145 4500008004100000245005500041210005400096260000800150300001200158490000700170520131900177653002401496100001901520856005001539 2010 eng d00aSelf-Referential Justifications in Epistemic Logic0 aSelfReferential Justifications in Epistemic Logic cmay a636-6610 v463 aThis 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.10aself-referentiality1 aKuznets, Roman uhttp://www.iam.unibe.ch/ltgpub/2010/kuz10.pdf01052nas a2200181 4500008004100000245003300041210003300074260001300107300001000120520057200130653001700702100002000719700001900739700001900758700002100777700002100798856005100819 2010 eng d00aTwo Ways to Common Knowledge0 aTwo Ways to Common Knowledge bElsevier a83-983 aIt 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.10aproof theory1 aBucheli, Samuel1 aKuznets, Roman1 aStuder, Thomas1 aBolander, Thomas1 aBraüner, Torben uhttp://www.iam.unibe.ch/ltgpub/2010/bks10a.pdf00492nas a2200145 4500008004100000245005200041210005200093260005500145300001100200100001900211700002000230700001900250700002600269856005100295 2009 eng d00aA Note on the Use of Sum in the Logic of Proofs0 aA Note on the Use of Sum in the Logic of Proofs aPatras University, GreecebPatras University Press a99-1031 aKuznets, Roman1 aDrossos, Costas1 aPeppas, Pavlos1 aTsinakis, Constantine uhttp://www.iam.unibe.ch/ltgpub/2009/kuz09b.pdf01299nas a2200145 4500008004100000245006200041210006200103260004100165300001000206520083000216100002001046700001901066700001901085856004901104 2009 eng d00aLogical Omniscience as a Computational Complexity Problem0 aLogical Omniscience as a Computational Complexity Problem aStanford University, CaliforniabACM a14-233 aThe 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$}.1 aArtemov, Sergei1 aKuznets, Roman1 aHeifetz, Aviad uhttp://www.iam.unibe.ch/ltgpub/2009/ak09.pdf01290nas a2200157 4500008004100000245007100041210006900112300001200181490000900193520080500202100002001007700001901027700002001046700001701066856004901083 2009 eng d00aThe NP-completeness of reflected fragments of justification logics0 aThe NPcompleteness of reflected fragments of justification logic a122-1360 v54073 aJustification 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.1 aBuss, Samuel, R1 aKuznets, Roman1 aArtemov, Sergei1 aNerode, Anil uhttp://www.iam.unibe.ch/ltgpub/2009/bk09.pdf