We describe a general logical framework, Justification Logic, for reasoning about epistemic justification. Justification Logic is based on classical propositional logic augmented by justification assertions t: F that read t is a justification for F. Justification Logic absorbs basic principles originating from both mainstream epistemology and the mathematical theory of proofs. It contributes to the studies of the well-known Justified True Belief vs. Knowledge problem. We state a general Correspondence Theorem showing that behind each epistemic modal logic, there is a (...) robust system of justifications. This renders a new, evidence-based foundation for epistemic logic. As a case study, we offer a resolution of the GoldmanRed Barns in Justification Logic. Furthermore, we formalize the well-known Gettier example and reveal hidden assumptions and redundancies in Gettier’s reasoning. (shrink)

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. (shrink)

In 1933 Godel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Godel's provability calculus is nothing but the forgetful projection of LP. This also achieves Godel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which (...) resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus. (shrink)

Sound and complete axiomatizations are provided for a number of different logics involving modalities for the knowledge of multiple agents and operators for branching time, extending previous work of Halpern, van der Meyden and Vardi [to appear, SIAM Journal on Computing] for logics of knowledge and linear time. The paper considers the system constraints of synchrony, perfect recall and unique initial states, which give rise to interaction axioms. The language is based on the temporal logic CTL*, interpreted with respect to (...) a version of the bundle semantics. (shrink)

Justification logics are modal logics that include justifications for the agent's knowledge. So far, there are no decidability results available for justification logics with negative introspection. In this paper, we develop a novel model construction for such logics and show that justification logics with negative introspection are decidable for finite constant specifications.

This paper presents a logic combining Dynamic Epistemic Logic, a framework for reasoning about multi-agent communication, with a new multi-agent version of Justification Logic, a framework for reasoning about evidence and justification. This novel combination incorporates a new kind of multi-agent evidence elimination that cleanly meshes with the multi-agent communications from Dynamic Epistemic Logic, resulting in a system for reasoning about multi-agent communication and evidence elimination for groups of interacting rational agents.

Justification logics provide a framework for reasoning about justifications and evidence. In this article, we study a fuzzy variant of justification logics in which an agent’s justification for a belief has certainty degree between 0 and 1. We replace the classical base of justification logics with Hájek’s rational Pavelka logic. We introduce fuzzy possible world semantics with crisp accessibility relation and also single world models for our logics. We establish soundness and graded-style completeness for both kinds of semantics. We also (...) introduce extensions with product conjunction. Finally, we offer a solution to a variant of the sorites paradox in our fuzzy justification logics. (shrink)

A new semantics is presented for the logic of proofs (LP), [1, 2], based on the intuition that it is a logic of explicit knowledge. This semantics is used to give new proofs of several basic results concerning LP. In particular, the realization of S4 into LP is established in a way that carefully examines and explicates the role of the + operator. Finally connections are made with the conventional approach, via soundness and completeness results.

This much-needed book provides a thorough account of temporal logic, one of the most important areas of logic in computer science today. The book begins with a solid introduction to semantical and axiomatic approaches to temporal logic. It goes on to cover predicate temporal logic, meta-languages, general theories of axiomatization, many dimensional systems, propositional quantifiers, expressive power, Henkin dimension, temporalization of other logics, and decidability results. With its inclusion of cutting-edge results and unifying methodologies, this book is an indispensable reference (...) for both the pure logician and the theoretical computer scientist. (shrink)

Reasoning About Knowledge is the first book to provide a general discussion of approaches to reasoning about knowledge and its applications to distributed ...

Justification logics are a family of modal epistemic logics which enables us to reasoning about justifications and evidences. In this paper, we introduce evidence-based multi-agent distributed knowledge logics, called distributed knowledge justification logics. The language of our justification logics contain evidence-based knowledge operators for individual agents and for distributed knowledge, which are interpreted respectively as “t is a justification that agent i accepts for F‘, and “t is a justification that all agents accept for F if they combine their knowledge (...) and justifications‘. We study basic properties of our logics and prove the conservativity of distributed knowledge justification logics over multi-agent justification logics. We present Kripke style models, pseudo-Fitting and Fitting models, as well as Mkrtychev models and prove soundness and completeness theorems. We also find a class of Fitting models which satisfies the principle of full communication. Finally, we establish the realization theorem, which states that distributed knowledge justification logics can be embedded into the modal distributed knowledge logics, and vise versa. (shrink)