Search

This paper presents a unification of interface automata and modal specifications, two radically dissimilar models for interface theories. Interface automata is a game-based model, which allows to make assumptions on the environment and propose an optimistic view for composition : two components can be composed if there is an environment where they can work together. Modal specification is a language theoretic account of a fragment of the modal mu-calculus logic that is more complete but which does not allow to distinguish between the environment and the component. Partial unifications of these two frameworks have been explored recently. A first attempt by Larsen et al. considers modal interfaces, an extension of modal specifications that deals with compatibility issues in the composition operator. However, this composition operator is incorrect. A second attempt by Raclet et al. gives a different perspective, and emphasises on conjunction and residuation of modal specifications, including when interfaces have dissimilar alphabets, but disregards interface compatibility. The present paper contributes a thorougher unification of the two theories by correcting the modal interface composition operator presented in the paper by Larsen et al., drawing a complete picture of the modal interface algebra, and pushing even further the comparison between interface automata, modal automata and modal interfaces.

We present the logic $\textsf{G.STRAT}$ for reasoning about group strategies. To enable a modal semantics for reasoning about group strategies, strategy profiles will be viewed as structured possible worlds. Although the general logic is undecidable and not finitely axiomatizable for systems with 3 agents or more, we identify more well-behaved logics like $\textsf{ATL}$, and temporal \emph{stit}-logics as fragments. We explain our aim to apply the logics to reasoning about multi-agent programs, such as the programs of 2APL. Finally, we discuss several properties of (multi-)agency expressible in the logic. Among these properties is an axiom characterizing a basic form of autonomy.

The formula (†) above is shown not to be first-order definable. The result is obtained by complicating the construction introduced in [4]. Two motivations are given for why the question of the first-order definability of (†) matters, one from theoretical considerations relating to modal logic, the other from applications of modal logic to philosophy, namely logic of ability. Finally a comparison with a cognate notion in the literature is given.

By means of models in toposes of C-sets (where C is a small category), necessary conditions are found for the minimum quantified extension of a propositional (intermediate, modal) logic to be complete with respect to Kripke semantics; in particular, many well-known systems turn out to be incomplete.

Defeasible logic is a non-monotonic formalism that deals with incomplete and conflicting information. Modal logic deals with necessity and possibility, exhibiting defeasibility; thus, it is possible to combine defeasible logic with modal operators. This paper reports on the extension of the DR-DEVICE defeasible reasoner with modal and deontic logic operators. The aim is a practical defeasible reasoner that will take advantage of the expressiveness of modal logics and the flexibility to define diverse agent types and behaviors.

The logic of Chance Discovery(CD) as well as mathematical models for CD, by the very nature of the term chance, are hard to formalize, which poses challenging problems for mathematization of the area. It does not completely prevent us though from studying the logical lawswhich chance discovery and related notions should abide, especially in a carefully chosen and reasonably expressive mathematical formalism. The framework, the authors suggest in this paper, is based on a well-developed area of modal logic, more precisely on Kripke-Hintikka semantics, with a notable distinction: unlike some other hybridization schemes, it leads to decidable logics, while still preserving high expressive power. We demonstrate our approach by an example of the Logic of Discovery and Knowledge, where a regular modal language is augmented with higher level operators intended to model some contrasting aspects of Chance Discovery: uncertain necessity of discoveryand local common knowledgewithin contexts admitting branching time.

We show that propositional dynamic logic and the modal µ-calculus are closed under product modalities, as defined in current dynamic-epistemic logics. Our analysis clarifies the latter systems, while also raising some new questions about fixed-point logics.

In this note, a fully modal proof is given of some conservation results proved in a previous paper by arithmetic means. The proof is based on the extendability of Kripke models.

We consider modal logics whose intermediate fragments lie between the logic of infinite problems [20] and the Medvedev logic of finite problems [15]. There is continuum of such logics [19]. We prove that none of them is finitely axiomatizable. The proof is based on methods from [12] and makes use of some graph-theoretic constructions (operations on coverings, and colourings).

We study a logic LDU (logic of Discovery in Uncertain Situations) generated in a semantic way as the set of all formulas valid in Krike/Hintikka models, which are models of linear discrete time with time clusters imitating possible uncertain states. The possibility of discoveryand uncertain necessity of discoveryare modeled by modal operations. The logic LDU differs from all standard normal and non-normal modal logics because the modalities ate not mutually expressible in standard way. We discuss properties of this logic, i.e. study its fragments, compare LDU with well known modal logics and study the main question about decidability of this logic. We propose an algorithm recognizing theorems of LDU (so we show that LDU is decidable), which is based on verification of validity of special normal reduced forms of rules in models of quadratic polynomial size in the testing rules.

Efficient proof methods for normal modal logics are highly desirable, as such logical systems have been widely used in computer science to represent complex situations. Resolution-based methods are often designed to deal with formulae in a normal form and the efficiency of the method (also) relies on how efficient (in the sense of producing fewer and/or shorter clauses) the translation procedure is. We present a normal form for normal modal logics and show how the use of simplification, for specific normal logics, together with anti-prenexing and prenexing techniques help us to produce better sets of clauses.

In recent years, a tight connection has emerged between modal logic on the one hand and coalgebras, understood as generic transition systems, on the other hand. Here, we prove that (finitary) coalgebraic modal logic has the finite model property. This fact not only reproves known completeness results for coalgebraic modal logic, which we push further by establishing that every coalgebraic modal logic admits a complete axiomatization of rank 1; it also enables us to establish a generic decidability result and a first complexity bound. Examples covered by these general results include, besides standard Hennessy-Milner logic, graded modal logic and probabilistic modal logic.

We introduce the logic of proofs whose modal counterpart is the modal logic S5. The language of Logic of Proofs LP is extended by a new unary operation of negative checker “?”. We define Kripke-style models for the resulting logic in the style of Fitting models and prove the corresponding Completeness theorem. The main result is the Realization theorem for the modal logic S5.

By making use of modal logic techniques, the paper disentangles two semantically different readings of statements of the type X counts as Y in context C (the classificatory and the constitutive readings) showing that, in fact, ‘counts-as is said in many ways'.

This paper will propose a dynamic semantics of quantified modal logic based on the theory of System Transition Systems, which are abstract objects modeling “Kripke models of Kripke models” or graph rewriting systems, by exlpoiting the theory of coalgebras in order to treat modal subordination as a Kripke model change, which requires no ad-hoc informal treatment such as accomodation as in [1] or extra-ontology introduced in [2] [3].

We construct explicit bases of admissible rules for a representative class of normal modal logics (including the systems K4, GL, S4, Grz, and GL.3), by extending the methods of S. Ghilardi and R. Iemhoff. We also investigate the notion of admissible multiple conclusion rules.

We develop semantics for modal logic programs in basic serial multimodal logics, which are parameterized by an arbitrary combination of generalized versions of axioms T, B, 4, 5 (in the form, e.g., 4:□iϕ→□j□kϕ) and I:□iϕ→□jϕ. We do not assume any special restriction for the form of programs and goals. Our fixpoint semantics and SLD-resolution calculus are defined using the direct approach and closely reflect the axioms of the used modal logic. We prove that our SLD-resolution calculus is sound and complete.

The notions of meta-ontology enhance the ability to process knowledge in information systems; in particular, ontological property classification deals with the kinds of properties in taxonomic knowledge based on a philosophical analysis. The goal of this paper is to devise a reasoning mechanism to check the ontological and logical consistency of knowledge bases, which is important for reasoning services on taxonomic knowledge. We first consider an ontological property classification that is extended to capture individual existence and time and situation dependencies. To incorporate the notion into logical reasoning, we formalize an order-sorted modal logic that involves rigidity, sortality, and three kinds of modal operators (temporal/situational/any world). The sorted expressions and modalities establish axioms with respect to properties, implying the truth of properties in different kinds of possible worlds and in varying domains in Kripke semantics. We provide a prefixed tableau calculus to test the satisfiability of such sorted modal formulas, which validates the ontological axioms of properties.

As an extension of the traditional modal logic, the fuzzy first-order modal logic is discussed in this paper. A description of fuzzy first-order modal logic based on constant domain semantics is given, and a formal system of fuzzy reasoning based on the semantic information of models of first-order modal logic is established. It is also introduced in this paper the notion of the satisfiability of the reasoning system and some properties associated with the satisfiability are proved.

The satisfiability checking problem is known to be decidable for a variety of modal/temporal logics such as the modal μ-calculus, but effective implementation has not necessarily been developed for all such logics. In this paper, we propose a decision procedure using the tableau method for the alternation-free two-way modal μ-calculus. Although the size of the tableau set maintained in the method might be large for complex formulas, the set and the operations on it can be expressed using BDD and therefore we can implement the method in an effective way.

The pi-calculus is one of the most important mobile process calculi and has been well studied in literature. Temporal logic is thought of as a good compromise between description convenience and abstraction and can support useful computational applications, such as model-checking. In this paper, we use a symbolic transition graph inherited from pi-calculus to model concurrent systems. A wide class of processes, that is, finite-control processes, can be represented as a finite symbolic transition graph. A new version of modal logic for the pi-calculus, an extension of the modal mu-calculus with Boolean expressions over names, and primitives for name input and output are introduced as an appropriate temporal logic for the pi-calculus. Since we make a distinction between proposition and predicate, the possible interactions between recursion and first-order quantification can be solved. A concise semantics interpretation for our modal logic is given. Based on this work, we provide a model checking algorithm for the logic. This algorithm follows Winskel's well known tag set method to deal with the fixpoint operator. As for the problem of name instantiating, our algorithm follows the 'on-the-fly' style, and systematically employs schematic names. The correctness of the algorithm is shown

We introduce our implemented modal logic programming system MProlog. This system is written in Prolog as a module for Prolog. Codes, libraries, and most features of Prolog can be used in MProlog programs. The system contains a number of built-in SLD-resolution calculi for modal logics, including calculi for useful multimodal logics of belief.

We examine modal logical systems, with generalized operators, for the precise treatment of vague notions such as ‘often’, ‘a meaningful subset of a whole’, ‘most’, ‘generally’ etc. The intuition of ‘most’ as “all but for a ‘negligible’ set of exceptions” is made precise by means of filters. We examine a modal logic, with a new modality for a local version of ‘most’ and present a sound and complete axiom system. We also discuss some variants of this modal logic.

We develop some ideas in order to obtain a nonmonotonic reasoning system based on the modal logic S4. As a consequence we show how to express the well known answer set semantics using a restricted fragment of modal formulas. Moreover, by considering the full set of modal formulas, we obtain an interesting generalization of answer sets for logic programs with modal connectives. We also depict, by the use of examples, possible applications of this inference system.

A Rasiowa-Sikorski proof system is presented for an elementary set theory which can act as a target language for translating propositional modal logics. The proposed system permits a modular analysis of (modal) axioms in terms of deductive rules for the relational apparatus. Such an analysis is possible even in the case when the starting modal logic does not possess a first-order correspondent. Moreover, the formalism enables a fine-tunable and uniform analysis of modal deductions in a simple and purely set-theoretic language.

In order to deal with some vague assertions more efficiently, fuzzy modal logics have been discussed by many researchers. This paper introduces the notation of fuzzy assertion based on propositional modal logic. As an extension of the traditional semantics about the modal logics, the fuzzy Kripke semantics are considered and the formal system of the fuzzy reasoning based on propositional modal logic is established and the properties about the satisfiability of the reasoning system are discussed.

Decision procedures for the propositional cases of two different logical representations for an L-Predicate Logic generalizing Autoepistemic Logic to handle quantified variables over modal scopes are described. The first representation is Second Order Logic. The second is Z Modal Logic which extends its S5 modal laws with laws stating what is logically possible. It is suggested that certain problems are more easily solved using one representation whereas other problems are more easily solved using the other.

The approach presented in this overview paper exploits that modal logics can be seen to be fragments of first-order logic and deductive methods can be developed and studied within the framework of first-order resolution. We focus on a class of extended modal logics very similar in spirit to propositional dynamic logic and closely related to description logics. We review and discuss the development of decision procedures for decidable extended modal logics and look at methods for automatically generating models.

We consider the sabotage modal logic SML which was suggested by van Benthem. SML is the modal logic equipped with a ‘transition-deleting’ modality and hence a modal logic over changing models. It was shown that the problem of uniform model checking for this logic is PSPACE-complete. In this paper we show that, on the other hand, the formula complexity and the program complexity are linear, resp., polynomial time. Further we show that SML lacks nice model-theoretic properties such as bisimulation invariance, the tree model property, and the finite model property. Finally we show that the satisfiability problem for SML is undecidable. Therefore SML seems to be more related to FO than to usual modal logic.

According to the standard definition, a logic is said to be paraconsistent if it fails the (so-called) rule of ex falso: i.e., α, ¬α ∀ β. Thus, paraconsistency captures an important sense in which a logic is inconsistency-tolerant, namely when arbitrary inference is prohibited in the presence of inconsistencies. We investigate a family of notions of paraconsistency within the context of modal logics.

We investigate a simple modal logic of probability with a unary modal operator expressing that a proposition is more probable than its negation. Such an operator is not closed under conjunction, and its modal logic is therefore non-normal. Within this framework we study the relation of probability with other modal concepts: belief and action.

A theory of plan synthesis is proposed that reasons about actions to solve the frame problem. The authors also reason about the plan synthesis to detect possible or impossible orderings of the actions. This theory uses the frame axiom and the modal quantificational logic Z to propagate the facts from the current situation to the next situation. The explicit results of an action are provided only, no delete list is needed. The facts are automatically added and deleted from one situation to the next by the nonmonotonic reasoning as the actions are performed. An example illustrates the plan synthesis algorithm, which is given. >

We reduce the modal mu-calculus model-checking problem for Kripke modal transition systems to the modal mu-calculus modelchecking problem for Kripke structures. This reduction is sound, preserves the alternation-depth fragments of the modal mu-calculus, is linear in the size of formulas and models, and extends the reach of modal mu-calculus model checkers to sound abstraction for the full logic. These results specialize to CTL* model-checking and CTL model checking.

[4] describes a modal logic for coalgebras of certain polynomial endofunctors on Set . This logic is here generalised to endofunctors on categories of sorted sets. The structure of the endofunctors considered is then exploited in order to define ways of moving from (coalgebras of) one endofunctor to (coalgebras of) another, and to equip them with translations between the associated modal languages. Furthermore, the resulting translations are shown to preserve and reflect the satisfaction of modal formulae by coalgebras.

We can couch our modal statements in the language of modal logic (sometimes, anyway) and then have recourse to possible worlds to explain the semantics of that language. Or we can proceed more directly, speaking explicitly of possible worlds from the start. Those who prefer the second course, as I do, have a choice to make. To say that there might be blue swans, for instance, we might provide our everyday descriptive predicates with extra argument places and write

We present two modal typing systems with the approximation modality, which has been proposed by the author to capture selfreferences involved in computer programs and their specifications. The systems are based on the simple and the F-semantics of types, respectively, and correspond to the same modal logic, which is considered the intuitionistic version of the logic of provability. We also show Kripke completeness of the modal logic and its decidability, which implies the decidability of type inhabitance in the typing systems.

We consider an extension of modal logic with an operator for constructing inflationary fixed points, just as the modal µ-calculus extends basic modal logic with an operator for least fixed points. Least and inflationary fixed point operators have been studied and compared in other contexts, particularly in finite model theory, where it is known that the logics IFP and LFP that result from adding such fixed point operators to first order logic have equal expressive power. As we show, the situation in modal logic is quite different, as the modal iteration calculus (MIC) we introduce has much greater expressive power than the µ-calculus. Greater expressive power comes at a cost: the calculus is algorithmically much less manageable.

We consider two systems of constructive modal logic which are computationally motivated. Their modalities admit several computational interpretations and are used to capture intensional features such as notions of computation, constraints, concurrency, etc. Both systems have so far been studied mainly from type-theoretic and category-theoretic perspectives, but Kripke models for similar systems were studied independently. Here we bring these threads together and prove duality results which show how to relate Kripke models to algebraic models and these in turn to the appropriate categorical models for these logics.