ABSTRACT. In this paper, we establish the Craig interpolation theorems of awareness logics by introducing analytic sequent calculi for them. For a semantic clause for an awareness operator, we choose an idea of propositional awareness, which is introduced by Fagin and Halpern and means that an agent is aware of a formula if and only if she is aware of all the atomic propositions contained in it. Although our sequent calculi are not cut-free (due to the fact that our epistemic logic is based on S5), we are able to restrict all applications of the rule of cut to analytic ones. This enables us to employ the Maehara method in order to compute Craig interpolants.

ABSTRACT. This article introduces a new semantics for the basic modal language, motivated by rough set theory. Additionally, a sound and complete deductive system relative to two important classes of models are obtained.

ABSTRACT. Arbitrary Public Announcement Logic (APAL) and its variants are proposed to formalize knowability dynamically based on public announcements as the means to update knowledge. In this paper, we introduce yet another variant HAPAL of APAL, which is based on questions instead of announcements, and captures knowability as knowing how to know by asking questions. Therefore, the prime modality in our language can also be viewed as a know-how operator sharing the same exist-box bundled structure as logics of knowing how in the literature. This change in the semantics of the arbitrary announcement operator results in a highly non-trivial logic, which departs from the existing versions of APAL. As we will show, it is already strictly more expressive than APAL and epistemic logic on S5 models in the single-agent case. Moreover, it lacks compactness and Craig interpolation property. We also provide a sound and weakly complete axiomatization.

ABSTRACT. In this paper, we introduce a sound and complete neighborhood semantics based on polarities for basic lattice-based monotone modal logic by generalizing duality between neighborhood frames and complete atomic Boolean algebras with monotone operators to a duality between complete lattice with monotone operators and polarity-based neighborhood frames. We also show that, similarly to the case of monotone modal logic on a classical base, monotone modal operators in lattice-based monotone modal logic can be represented as the composition of suitable normal modal operators via a multi-type representation of complete lattices with monotone operators.

ABSTRACT. In this paper, we are interested in weighted one-counter automata whose transitions are assigned a weight from a fixed field. In particular, we consider deterministic weighted real-time one-counter automaton (DWROCA). A DWROCA is a deterministic real-time one-counter automaton whose transitions are assigned a weight. Two DWROCAs are equivalent if every word accepted by one is accepted by the other with the same weight. DWROCA is a sub-class of weighted one-counter automata with counter determinacy. It is known that the equivalence problem for this model is in P. This paper gives a simpler proof for checking the equivalence of two DWROCAs. This gives a better polynomial-time algorithm for checking the equivalence of DWROCAs.

ABSTRACT. We propose and investigate a new model of a distributed game played on a non-deterministic asynchronous transition system over two processes. This game is played between an environment and a distributed team of the two processes where each process has only partial information of the ongoing play – namely complete information up to the last synchronization and only its own local evolution since this last synchronization. The key algorithmic decision problem, for a given winning objective, is the existence of a distributed cooperative winning strategy for the team to meet that objective. We address this question for global safety, local reachability and global/simultaneous reachability objectives. We carry out a thorough analysis of these games and present natural fix-point based algorithms for solving them. This allows us to construct distributed winning strategies with an explicit distributed finite-memory in the form of key past information, and also yields near optimal decision procedures. Specifically, our analysis shows that the decision problems for global safety and local reachability objectives are NP-complete. We also establish that the decision problem for global reachability objective is PSPACE-hard and provide an NEXPTIME algorithm for the same.

ABSTRACT. We present a proof-theoretic study of Contraction Free Arithmetic $(\mathsf{CFA})$. We introduce $\mathsf{CFA}$ as a first order arithmetical theory based on a logic $(\mathsf{GQC})$ which is the multiplicative fragment of $\mathsf{LK}$ without the structural rules of contraction. We justify our choice of axiomatization and demonstrate some key properties of the arithmetic. We eventually show that the class of provably recursive functions of $\mathsf{CFA}$ exactly correspond to the class of primitive recursive functions. Consequently, the essential result of the present work is that $\mathsf{CFA}$ not only expands the class of provably recursive functions beyond those of $\mathsf{I\Delta_0}$, but also establishes its distinctiveness from $\mathsf{PA}$.

ABSTRACT. Ludwig Wittgenstein’s remarks on Gödel’s First Incompleteness Theorem and specifically his discussion of the significance and interpretation of the undecidable sentence constructed in the proof of the Theorem have come in for much criticism. Gödel himself was dismissive of those remarks. Critics have argued that Wittgenstein misunderstood the Theorem and its proof and conflated the notions of truth and provability. On the other hand, Juliet Floyd & Hilary Putnam argue that these remarks contain a philosophical claim of great interest. Several scholars have responded to Floyd & Putnam. There has been a reply by Floyd & Putnam. I offer my own contribution to this debate.

ABSTRACT. An account of progress to modern Foundations.