# Blog Archives

# Topic Archive: justification logic

# Some new directions in Epistemic Logic.

We will review research avenues on which we will focus this semester.

1. Applications of Justification Logic: general theory of logical omniscience, new format of handling inconsistent information, argumentation theory, truth maintenance systems, tracking evidence and belief revision.

2. Syntactic Epistemic Logic. There is some well-known tension between a syntactic description of an epistemic scenario and its semantical analysis based on a specific model. Such analysis requires common knowledge of the model which does not usually follow from the assumptions. Syntactic Epistemic Logic offers an approach to epistemic situations which does not rely on the common knowledge of a model.

3. Generic Common Knowledge.The notion of common knowledge of F, as introduced by Lewis in 1969, refers to any situation in which each finite iteration of `agent 1 knows that agent 2 knows that … F’ holds. A similar approach has been offered by McCarthy and others. This situatuion is now called Generic Common Knowledge, GCK, of F. Now dominant notion of Common Knowledge CK was coined by Aumann in 1976 as the least of all GCK’s of F. Now there is a growing number of specific epistemic scenarios which require GCK rather than CK. We are developing the theory of GCK and applying GCK to CK in appropriate situations.

# Realization Semantically

This talk continues my previous one from October 22. In that, I gave justification counterparts for S4.2 and for K4^3, possible world justification semantics, and a completeness proof. The completeness proof used a canonical model construction. Now I’l use that canonical model to prove, non-constructively, realization theorems for the two logics. The methodology is the same as in a paper of mine published in 2005, though the presentation has change somewhat. Primarily my motivation is to explore the range of modal logics having justification counterparts—to discover its extent and limits.

# J-Calc: Justified Modal Types and Functional Programs

In this talk we give a computationally motivated presentation of J-Calc. J-Calc is an extension of simply typed lambda calculus with justifications and justified modal types.

Initiating from textbook examples of modular programs, we will present the modal type theory of J-Calc as a type system corresponding to programming with modular definitions. More specifically, we will show how justified modality offers a logical reading to separate compilation in modular functional programming.

# Justification Logic Semantics: A Little New, but Mostly Old

Possible world semantics was introduced for justification logic in 2005. Initially it was for the Logic of Proofs, but it quickly extended to “nearby” logics, and more slowly to a wider family. Eight years is a long time, and by now people may be generally familiar with the ideas without having gone through any of the details. I will try to remedy that.

# On the Complexity of Multi-agent Justification Logic Under Interacting Justifications II

We introduce a family of multi-agent justification logics with interactions between the agents’ justifications, by extending and generalizing the two-agent versions of LP introduced by Yavorskaya in 2008. Known concepts and tools from the single-agent justification setting are adjusted for this multiple agent case. We present tableau rules and some preliminary complexity results: in several important cases, the satisfiability problem for these logics remains in the second level of the polynomial hierarchy, while for others it is PSPACE or EXP-hard.

This week we will present the general tableau rules for the family. We look more closely at particular examples and complexity bounds and we identify common sources of jumps in their complexity.

# On the Complexity of Multi-agent Justification Logic Under Interacting Justifications

We introduce a family of multi-agent justification logics with interactions between the agents’ justifications, by extending and generalizing the two-agent versions of LP introduced by Yavorskaya in 2008. Known concepts and tools from the single-agent justification setting are adjusted for this multiple agent case. We present tableau rules and some preliminary complexity results: in several important cases, the satisfiability problem for these logics remains in the second level of the polynomial hierarchy, while for others it is PSPACE or EXP-hard.

# Realization Implemented

Justification logics are connected to modal logics via realization theorems. These have both constructive and non-constructive proofs. Here we do two things. First we provide a new path to constructive realization proofs, going through an intermediate quasi-realization stage. Quasi-realizers are easier to produce than realizers, though like them they are constructed from cut-free proofs. Quasi-realizers in turn constructively convert to realizers, and this conversion is independent of the justification logic in question. The construction depends only on the structure of the formula involved.

The second thing we do is provide a Prolog implementation of quasi-realization, and quasi-realization to realization conversion, for the logic LP. Many other justification logics can obviously be treated similarly.

Our quasi-realization algorithm, and its implementation, assumes the underlying modal proof system S4 is based on tableaus. Since these may not be familiar to everybody, we provide a sketch of how tableaus work. Then we present our algorithms, our implementation, and a discussion of implementation behavior and design decisions.

We believe our algorithms are simple and straightforward. The original realization algorithm, for instance, needed the entire cut-free proof as input. Our quasi-realization algorithm works one formal proof step at a time. There is, in the literature, another realization construction that works one step at a time, but it requires extensive use of substitution while our quasi-realization algorithm does not. The conversion algorithm is, as noted above, independent of particular justification logics and so only needs to be understood once. It is only here that substitution is needed.

Both the program to compute realizations, and a tech report discussing the algorithm, necessary background, and the implementation, are available on the speaker’s web page:

http://comet.lehman.cuny.edu/fitting/