00500nas a2200169 4500008004100000020002200041245003400063210003400097260004400131300001200175100001900187700002100206700001900227700002000246700001400266856005000280 2018 eng d a978-3-319-72056-200aA Logic of Blockchain Updates0 aA Logic of Blockchain Updates aChambSpringer International Publishing a107-1191 aBrünnler, Kai1 aFlumini, Dandolo1 aStuder, Thomas1 aArtemov, Sergei1 aNerode, A uhttp://www.iam.unibe.ch/ltgpub/2018/bfs18.pdf00427nas a2200145 4500008004100000245003800041210003800079260001300117100002200130700002300152700001900175700002000194700001700214856005000231 2016 eng d00aProbabilistic Justification Logic0 aProbabilistic Justification Logic bSpringer1 aKokkinis, Ioannis1 aOgnjanović, Zoran1 aStuder, Thomas1 aArtemov, Sergei1 aNerode, Anil uhttp://www.iam.unibe.ch/ltgpub/2016/kos16.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.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.pdf00439nas a2200157 4500008004100000245004100041210004100082260001300123300001200136490000900148100002100157700001900178700002000197700001400217856005000231 2009 eng d00aData Privacy for ALC Knowledge Bases0 aData Privacy for ALC Knowledge Bases bSpringer a409-4210 v54071 aStouppa, Phiniki1 aStuder, Thomas1 aArtemov, Sergei1 aNerode, A uhttp://www.iam.unibe.ch/ltgpub/2009/ss09b.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.pdf00420nas a2200157 4500008004100000245003100041210003100072260001300103300001200116490000900128100001900137700001900156700002000175700001700195856005000212 2007 eng d00aTotal public announcements0 aTotal public announcements bSpringer a498-5110 v45141 aSteiner, David1 aStuder, Thomas1 aArtemov, Sergei1 aNerode, Anil uhttp://www.iam.unibe.ch/ltgpub/2007/ss07a.pdf00454nas a2200133 4500008004100000245005400041210005400095260005200149300001200201100001900213700002000232700001800252856005000270 2006 eng d00aA system for consistency preserving belief change0 aA system for consistency preserving belief change bAssociation for Logic, Language and Information a133-1441 aSteiner, David1 aArtemov, Sergei1 aParikh, Rohit uhttp://www.iam.unibe.ch/ltgpub/2006/ste06.pdf00932nas a2200121 4500008004100000245004700041210004700088260005500135520051100190100002000701700001900721856007000740 1993 eng d00aFunctionality in the Basic Logic of Proofs0 aFunctionality in the Basic Logic of Proofs bInstitut für Informatik und angewandte Mathematik3 aThis report describes the elimination of the injectivity restriction for functional arithmetical interpretations as used in the systems $\mathcal{PF}$ and $\mathcal{PFM}$ in the Basic Logic of Proofs. An appropriate axiom system $\mathcal{PU}$ in a language with operators ``$x$ is a proof of $y$'' is defined and proved to be sound and complete with respect to all arithmetical interpretations based on functional proof predicates. Unification plays a major role in the formulation of the new axioms.1 aArtemov, Sergei1 aStrassen, Tyko uhttp://www.iam.unibe.ch/publikationen/techreports/1993/iam-93-00400867nas a2200205 4500008004100000245003000041210003000071260001300101300001000114490000800124520036300132100002000495700001900515700001500534700002000549700002200569700001500591700001700606856003800623 1993 eng d00aThe Basic Logic of Proofs0 aThe Basic Logic of Proofs bSpringer a14-280 v7023 aPropositional Provability Logic was axiomatized in [Sol76]. This logic describes the behaviour of the arithmetical operator ``$y$ is provable''. The aim of the current paper is to provide propositional axiomatizations of the predicate ``$x$ is a proof of $y$'' by means of modal logic, with the intention of meeting some of the needs of computer science.1 aArtemov, Sergei1 aStrassen, Tyko1 aBörger, E1 aJäger, Gerhard1 aKleine Büning, H1 aMartini, S1 aRichter, M M uhttp://www.ltg.unibe.ch/node/151900832nas a2200181 4500008004100000245004400041210004400085260001300129300001000142490000800152520035000160100002000510700001900530700001900549700002300568700002100591856003800612 1993 eng d00aThe Logic of the Gödel Proof Predicate0 aThe Logic of the Gödel Proof Predicate bSpringer a71-820 v7133 aWe discuss the logics of the operators ``$p$ is a proof of $A$'' and ``$p$ is a proof containing $A$'' for the standard Gödel proof predicate in Peano Arithmetic. Decidabillty and arithmetical completeness of these logics are proved. We use the same semantics as for the Provability Logic where the operator ``$A$ is provable'' is studied.1 aArtemov, Sergei1 aStrassen, Tyko1 aGottlob, Georg1 aLeitsch, Alexander1 aMundici, Daniele uhttp://www.ltg.unibe.ch/node/152200764nas a2200121 4500008004100000245003000041210003000071260005500101520036300156100002000519700001900539856008400558 1992 eng d00aThe Basic Logic of Proofs0 aThe Basic Logic of Proofs bInstitut für Informatik und angewandte Mathematik3 aPropositional Provability Logic was axiomatized in [Sol76]. This logic describes the behaviour of the arithmetical operator ``$y$ is provable''. The aim of the current paper is to provide propositional axiomatizations of the predicate ``$x$ is a proof of $y$'' by means of modal logic, with the intention of meeting some of the needs of computer science.1 aArtemov, Sergei1 aStrassen, Tyko uhttps://www.iam.unibe.ch/de/forschung/publikationen/techreports/1992/iam-92-018