Epistemic logic is usually employed to model two aspects of a situation: the factual and the epistemic aspects. Truth, however, is not always attainable, and in many cases we are forced to reason only with whatever information is available to us. In this paper, we will explore a four-valued epistemic logic designed to deal with these situations, where agents have only knowledge about the available information, which can be incomplete or conflicting, but not explicitly about facts. This layer of available (...) information or evidence, which is the object of the agents’ knowledge, can be seen as a database. By adopting this sceptical posture in our semantics, we prepare the ground for logics where the notion of knowledge—or more appropriately, belief—is entirely based on evidence. The technical results include a set of reduction axioms for public announcements, correspondence proofs, and a complete tableau system. In summary, our contributions are twofold: on the one hand we present an intuition and possible application for many-valued modal logics, and on the other hand we develop a logic that models the dynamics of evidence in a simple and intuitively clear fashion. (shrink)

When agents know a protocol, this leads them to have expectations about future observations. Agents can update their knowledge by matching their actual observations with the expected ones. They eliminate states where they do not match. In this paper, we study how agents perceive protocols that are not commonly known, and propose a semantics-driven logical framework to reason about knowledge in such scenarios. In particular, we introduce the notion of epistemic expectation models and a propositional dynamic logic-style epistemic logic for (...) reasoning about knowledge via matching agentsÊ expectations to their observations. It is shown how epistemic expectation models can be obtained from epistemic protocols. Furthermore, a characterization is presented of the effective equivalence of epistemic protocols. We introduce a new logic that incorporates updates of protocols and that can model reasoning about knowledge and observations. Finally, the framework is extended to incorporate fact-changing actions, and a worked-out example is given. © 2013 Elsevier B.V. (shrink)

In this paper, I develop a new set of doxastic logical systems and I show how they can be used to solve several well-known problems in doxastic logic, for example the so-called problem of logical omniscience. According to this puzzle, the notions of knowledge and belief that are used in ordinary epistemic and doxastic symbolic systems are too idealised. Hence, those systems cannot be used to model ordinary human or human-like agents' beliefs. At best, they can describe idealised individuals. The (...) systems in this paper can be used to symbolise not only the doxastic states of perfectly rational individuals, but also the beliefs of finite humans. Proof-theoretically, I will use a tableau technique. Every system is combined with predicate logic with necessary identity and ‘possibilist’ quantifiers and modal logic with two kinds of modal operators for relative and absolute necessity. The semantics is a possible world semantics. Finally, I prove that every tableau system in the paper is sound and complete with respect to its semantics. (shrink)

This paper combines a non-contingency logic with an epistemic logic by means of fusions and products of modal systems. Some consequences of these interplays are pointed out.

We investigate an aspect of defeasibility that has somewhat been overlooked by the non-monotonic reasoning community, namely that of defeasible modes of reasoning. These aim to formalise defeasibility of the traditional notion of necessity in modal logic, in particular of its different readings as action, knowledge and others in specific contexts, rather than defeasibility of conditional forms. Building on an extension of the preferential approach to modal logics, we introduce new modal osperators with which to formalise the notion of defeasible (...) necessity and distinct possibility, and that can be used to represent expected effects, refutable knowledge, and so on. We show how KLM-style conditionals can smoothly be integrated with our richer language. We also propose a tableau calculus which is sound and complete with respect to our modal preferential semantics, and of which the computational complexity remains in the same class as that of the underlying classical modal logic. (shrink)

In the basic modal language and in the basic modal language with the added universal modality, first-order definability of all formulas over the class of all frames is shown. Also, it is shown that the problems of modal definability of first-order sentences over the class of all frames in the languages and are both PSPACE-complete.

We analyse the computational complexity of comparing informational structures. Intuitively, we study the complexity of deciding queries such as the following: Is Alice’s epistemic information strictly coarser than Bob’s? Do Alice and Bob have the same knowledge about each other’s knowledge? Is it possible to manipulate Alice in a way that she will have the same beliefs as Bob? The results show that these problems lie on both sides of the border between tractability (P) and intractability (NP-hard). In particular, we (...) investigate the impact of assuming information structures to be partition-based (rather than arbitrary relational structures) on the complexity of various problems. We focus on the tractability of concrete epistemic tasks and not on epistemic logics describing them. (shrink)

Hybrid languages are expansions of propositional modal languages which can refer to worlds. The use of strong hybrid languages dates back to at least [Pri67], but recent work has focussed on a more constrained system called $\mathscr{H}$. We show in detail that $\mathscr{H}$ is modally natural. We begin by studying its expressivity, and provide model theoretic characterizations and a syntactic characterization. The key result to emerge is that $\mathscr{H}$ corresponds to the fragment of first-order logic which is invariant for generated (...) submodels. We then show that $\mathscr{H}$ enjoys interpolation, provide counterexamples for its finite variable fragments, and show that weak interpolation holds for the sublanguage $\mathscr{H}$. Finally, we provide complexity results for $\mathscr{H}$ and other fragments and variants, and sharpen known undecidability results for $\mathscr{H}$. (shrink)

We develop a conceptually clear, intuitive, and feasible decision procedure for testing satisfiability in the full multi\-agent epistemic logic \CMAELCD\ with operators for common and distributed knowledge for all coalitions of agents mentioned in the language. To that end, we introduce Hintikka structures for \CMAELCD\ and prove that satisfiability in such structures is equivalent to satisfiability in standard models. Using that result, we design an incremental tableau-building procedure that eventually constructs a satisfying Hintikka structure for every satisfiable input set of (...) formulae of \CMAELCD\ and closes for every unsatisfiable input set of formulae. (shrink)

Recently predominant forms of anti-realism claim that all truths are knowable. We argue that in a logical explanation of the notion of knowability more attention should be paid to its epistemic part. Especially very useful in such explanation are notions of group knowledge. In this paper we examine mainly the notion of distributed knowability and show its effectiveness in the case of Fitch’s paradox. Proposed approach raised some philosophical questions to which we try to find responses. We also show how (...) we can combine our point of view on Fitch’s paradox with the others. Next we give an answer to the question: is distributed knowability factive? At the end, we present some details concerning a construction of anti-realist modal epistemic logic. (shrink)

This work introduces a two-dimensional modal logic to represent agents' Concurrent Common Knowledge in distributed systems. Unlike Common Knowledge, Concurrent Common Knowledge is a kind of agreement reachable in asynchronous environments. The formalization of such type of knowledge is based on a model for asynchronous systems and on the definition of Concurrent Knowledge introduced before in paper [5]. As a proper semantics, we review our concept of closed sub-product of modal logics which is based on the product of modal logics. (...) The key idea is to reason about Concurrent Knowledge under a two-dimensional approach, regarding asynchronous runs and consistent global states as dimensions. We present an axiomatic system for the logic and issue the corresponding soundness and completeness proofs. (shrink)

ABSTRACT This paper follows on previous papers which present and evaluate various decision procedures for modal logics. We consider new test sets and systems that have been recently proposed in the literature. This new experimental analysis confirm previous experimental results in showing that SAT based decision procedures, i.e., the procedures built on top of decision procedures for propositional satisfiability, are more efficient than tableau based decision procedures. They also confirm previous evidence of an easy-hard-easy pattern in the satisfiability curve for (...) modal K. Finally, on these tests, SAT based decision procedures are also more efficient than the recently proposed decision procedures based on translation methods. These results contradict some of the claims presented in previous papers by other authors. (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)

We show that a 0–1 law holds for propositional modal logic, both for structure validity and frame validity. In the case of structure validity, the result follows easily from the well-known 0–1 law for first-order logic. However, our proof gives considerably more information. It leads to an elegant axiomatization for almost-sure structure validity and to sharper complexity bounds. Since frame validity can be reduced to a Π11 formula, the 0–1 law for frame validity helps delineate when 0–1 laws exist for (...) second-order logics. (shrink)

In a previous work we introduced the algorithm \SQEMA\ for computing first-order equivalents and proving canonicity of modal formulae, and thus established a very general correspondence and canonical completeness result. \SQEMA\ is based on transformation rules, the most important of which employs a modal version of a result by Ackermann that enables elimination of an existentially quantified predicate variable in a formula, provided a certain negative polarity condition on that variable is satisfied. In this paper we develop several extensions of (...) \SQEMA\ where that syntactic condition is replaced by a semantic one, viz. downward monotonicity. For the first, and most general, extension \SSQEMA\ we prove correctness for a large class of modal formulae containing an extension of the Sahlqvist formulae, defined by replacing polarity with monotonicity. By employing a special modal version of Lyndon's monotonicity theorem and imposing additional requirements on the Ackermann rule we obtain restricted versions of \SSQEMA\ which guarantee canonicity, too. (shrink)

We investigate an axiomatization of the notion of common belief that makes use of no rules of inference and highlight the property of the set of accessibility relations that characterizes each axiom.

ABSTRACT In this paper we define two logics, KLn and BLn, and present tableau-based decision procedures for both. KLn is a temporal logic of knowledge. Thus, in addition to the usual connectives of linear discrete temporal logic, it contains a set of unary modal connectives for representing the knowledge possessed by agents. The logic BLn is somewhat similar; it is a temporal logic that contains connectives for representing the beliefs of agents. In addition to a complete formal definition of the (...) two logics and their decision procedures, the paper includes a brief review of their applications in AI and mainstream computer science, correctness proofs for the decision procedures, a number of worked examples illustrating the decision procedures, and some pointers to further work. (shrink)

It is known that a theory in S5‐epistemic logic with several agents may have numerous models. This is because each such model specifies also what an agent knows about infinite intersections of events, while the expressive power of the logic is limited to finite conjunctions of formulas. We show that this asymmetry between syntax and semantics persists also when infinite conjunctions (up to some given cardinality) are permitted in the language. We develop a strengthened S5‐axiomatic system for such infinitary logics, (...) and prove a strong completeness theorem for them. Then we show that in every such logic there is always a theory with more than one model. (shrink)

We propose a dynamic logic of lying, wherein a ‘lie that $\varphi $ ’ (where $\varphi $ is a formula in the logic) is an action in the sense of dynamic modal logic, that is interpreted as a state transformer relative to the formula $\varphi $ . The states that are being transformed are pointed Kripke models encoding the uncertainty of agents about their beliefs. Lies can be about factual propositions but also about modal formulas, such as the beliefs of (...) other agents or the belief consequences of the lies of other agents. We distinguish two speaker perspectives: (Obs) an outside observer who is lying to an agent that is modelled in the system, and (Ag) an agent who is lying to another agent, and where both are modelled in the system. We distinguish three addressee perspectives: (Cred) the credulous agent who believes everything that it is told (even at the price of inconsistency), (Skep) the skeptical agent who only believes what it is told if that is consistent with its current beliefs, and (Rev) the belief revising agent who believes everything that it is told by consistently revising its current, possibly conflicting, beliefs. The logics have complete axiomatizations, which can most elegantly be shown by way of their embedding in what is known as action model logic or in the extension of that logic to belief revision. (shrink)

The paper surveys the currently available axiomatizations of common belief (CB) and common knowledge (CK) by means of modal propositional logics. (Throughout, knowledge- whether individual or common- is defined as true belief.) Section 1 introduces the formal method of axiomatization followed by epistemic logicians, especially the syntax-semantics distinction, and the notion of a soundness and completeness theorem. Section 2 explains the syntactical concepts, while briefly discussing their motivations. Two standard semantic constructions, Kripke structures and neighbourhood structures, are introduced in Sections (...) 3 and 4, respectively. It is recalled that Aumann's partitional model of CK is a particular case of a definition in terms of Kripke structures. The paper also restates the well-known fact that Kripke structures can be regarded as particular cases of neighbourhood structures. Section 3 reviews the soundness and completeness theorems proved w.r.t. the former structures by Fagin, Halpern, Moses and Vardi, as well as related results by Lismont. Section 4 reviews the corresponding theorems derived w.r.t. the latter structures by Lismont and Mongin. A general conclusion of the paper is that the axiomatization of CB does not require as strong systems of individual belief as was originally thought- only monotonicity has thusfar proved indispensable. Section 5 explains another consequence of general relevance: despite the "infinitary" nature of CB, the axiom systems of this paper admit of effective decision procedures, i.e., they are decidable in the logician's sense. (shrink)

While dynamic epistemic logics with common knowledge have been extensively studied, dynamic epistemic logics with distributed knowledge have so far received far less attention. In this paper we study extensions of public announcement logic ( $\mathcal{PAL }$ ) with distributed knowledge, in particular their expressivity, axiomatisations and complexity. $\mathcal{PAL }$ extended only with distributed knowledge is not more expressive than standard epistemic logic with distributed knowledge. Our focus is therefore on $\mathcal{PACD }$ , the result of adding both common and (...) distributed knowledge to $\mathcal{PAL }$ , which is more expressive than each of its component logics. We introduce an axiomatisation of $\mathcal{PACD }$ , which is not surprising: it is the combination of well-known axioms. The completeness proof, however, is not trivial, and requires novel combinations and extensions of techniques for dealing with $S5$ knowledge, distributed knowledge, common knowledge and public announcements at the same time. We furthermore show that $\mathcal{PACD }$ is decidable, more precisely that it is $\textsc {exptime}$ -complete. This result also carries over to $\mathcal{S 5\mathcal CD }$ with common and distributed knowledge operators for all coalitions (and not only the grand coalition). Finally, we propose a notion of a trans-bisimulation to generalise certain results and give deeper insight into the proofs. (shrink)

The problem of finding sufficient doxastic conditions for backward induction in games of perfect information is analyzed in a syntactic framework with subjunctive conditionals. This allows to describe the structure of the game by a logical formula and consequently to treat beliefs about this structure in the same way as beliefs about rationality. A backward induction and a non-Nash equilibrium result based on higher level belief in rationality and the structure of the game are derived.

We here describe research into the formal specification and implementation of resource-bounded agents. In particular, we provide an overview of our work on incorporating resource limitations into executable agent specifications. In addition, we outline future directions, highlighting both their promise and their problems.

We define a tableau calculus for the logic of only knowing and knowing at most ON, which is an extension of Levesque's logic of only knowing O. The method is based on the possible-world semantics of the logic ON, and can be considered as an extension of known tableau calculi for modal logic K45. From the technical viewpoint, the main features of such an extension are the explicit representation of "unreachable" worlds in the tableau, and an additional branch closure condition (...) implementing the property that each world must be either reachable or unreachable. The calculus allows for establishing the computational complexity of reasoning about only knowing and knowing at most. Moreover, we prove that the method matches the worst-case complexity lower bound of the satisfiability problem for both ON and O. With respect to [22], in which the tableau calculus was originally presented, in this paper we both provide a formal proof of soundness and completeness of the calculus, and prove the complexity results for the logic ON. (shrink)

We show the faithful embedding of common knowledge logic CKL into game logic GL, that is, CKL is embedded into GL and GL is a conservative extension of the fragment obtained by this embedding. Then many results in GL are available in CKL, and vice versa. For example, an epistemic consideration of Nash equilibrium for a game with pure strategies in GL is carried over to CKL. Another important application is to obtain a Gentzen-style sequent calculus formulation of CKL and (...) its cut-elimination. The faithful embedding theorem is proved for the KD4-type propositional CKL and GL, but it holds for some variants of them. (shrink)

This paper provides a logic framework for investigations of game theoretical problems. We adopt an infinitary extension of classical predicate logic as the base logic of the framework. The reason for an infinitary extension is to express the common knowledge concept explicitly. Depending upon the choice of axioms on the knowledge operators, there is a hierarchy of logics. The limit case is an infinitary predicate extension of modal propositional logic KD4, and is of special interest in applications. In Part I, (...) we develop the basic framework, and show some applications: an epistemic axiomatization of Nash equilibrium and formal undecidability on the playability of a game. To show the formal undecidability, we use a term existence theorem, which will be proved in Part II. (shrink)

We study a knowledge logic that assumes that to each set of agents, an indiscernibility relation is associated and the agents decide the membership of objects or states up to this indiscernibility relation. Its language contains a family of relative knowledge operators. We prove the decidability of the satisfiability problem, we show its EXPTIME-completeness and as a side-effect, we define a complete Hilbert-style axiomatization.

In this paper a unified framework for dealing with a broad family of propositional multimodal logics is developed. The key tools for presentation of the logics are the notions of closure relation operation and monotonous relation operation. The two classes of logics: FiRe-logics (finitely reducible logics) and LaFiRe-logics (FiRe-logics with local agreement of accessibility relations) are introduced within the proposed framework. Further classes of logics can be handled indirectly by means of suitable translations. It is shown that the logics from (...) these classes have the finite model property with respect to the class of -formulae, i.e. each -formula has a -model iff it has a finite -model. Roughly speaking, a -formula is logically equivalent to a formula in negative normal form without occurrences of modal operators with necessity force. In the proof we introduce a substantial modification of Claudio Cerrato's filtration technique that has been originally designed for graded modal logics. The main core of the proof consists in building adequate restrictions of models while preserving the semantics of the operators used to build terms indexing the modal operators. (shrink)

In this paper, I develop a syntactic framework for the analysis ofstrategic form games that is based on a straightforward combination ofstandard systems of doxastic, probabilistic and conditionalpropositional logic. In particular, for the probabilistic part I makeuse of the axiomatization provided in Fagin and Halpern (1994). The use ofconditionals allows to represent a strategic form game by a logicalformula in a very natural way. Also expected utility maximization can benaturally captured. I use this framework to prove a version of a (...) resulton Nash equilibrium conjectures first presented in Aumann and Brandenburger (1995). (shrink)

Description logics are a family of knowledge representation formalisms that are descended from semantic networks and frames via the system Kl-one. During the last decade, it has been shown that the important reasoning problems (like subsumption and satisfiability) in a great variety of description logics can be decided using tableau-like algorithms. This is not very surprising since description logics have turned out to be closely related to propositional modal logics and logics of programs (such as propositional dynamic logic), for which (...) tableau procedures have been quite successful.Nevertheless, due to different underlying institutions and applications, most description logics differ significantly from run-of-the-mill modal and program logics. Consequently, the research on tableau algorithms in description logics led to new techniques and results, which are, however, also of interest for modal logicians. In this article, we will focus on three features that play an important rôle in description logics (number restrictions, terminological axioms, and role constructors), and show how they can be taken into account by tableau algorithms. (shrink)

Since the early days of artificial intelligence (AI), many logics have been explored as tools for knowledge representation and reasoning. In the spirit of the Crossley Festscrift and recognizing John Crossley’s diverse interests and his legacy in both mathematical logic and computer science, I discuss examples from my own research that sit in the overlap of logic and AI, with a focus on supporting human–AI interactions.

S4.2 is the modal logic of directed partial pre-orders and/or the modal logic of reflexive and transitive relational frames with a final cluster. It holds a distinguished position in philosophical...

This paper introduces the logics of super-strict implications, where a super-strict implication is a strengthening of C.I. Lewis' strict implication that avoids not only the paradoxes of material implication but also those of strict implication. The semantics of super-strict implications is obtained by strengthening the (normal) relational semantics for strict implication. We consider all logics of super-strict implications that are based on relational frames for modal logics in the modal cube. it is shown that all logics of super-strict implications are (...) connexive logics in that they validate Aristotle's Theses and (weak) Boethius's Theses. A proof-theoretic characterisation of logics of super-strict implications is given by means of G3-style labelled calculi, and it is proved that the structural rules of inference are admissible in these calculi. It is also shown that validity in the S5-based logic of super-strict implications is equivalent to validity in G. Priest's negation-as-cancellation-based logic. Hence, we also give a cut-free calculus for Priest's logic. (shrink)