Search

This paper explores the relationship between dynamic and truth conditional semantics for epistemic modals. It provides a generalization of a standard dynamic update semantics for modals. This new semantics derives a Kripke semantics for modals and a standard dynamic semantics for modals as special cases. The semantics allows for new characterizations of a variety of principles in modal logic, including the inconsistency of 'p and might not p'. Finally, the semantics provides a construction procedure for transforming any truth conditional semantics for modals into a dynamic semantics for modals with similar properties. [ABSTRACT FROM AUTHOR]

Despite the fact that call-by-value λ-calculus was defined by Plotkin in 1977, we believe that its theory of program approximation is still at the beginning. A problem that is often encountered when studying its operational semantics is that, during the reduction of a λ-term, some redexes remain stuck (waiting for a value). Recently, Carraro and Guerrieri proposed to endow this calculus with permutation rules, naturally arising in the context of linear logic proof-nets, that succeed in unblocking a certain number of such redexes. In the present paper we introduce a new class of models of call-by-value λ-calculus, arising from non-idempotent intersection type systems. Beside satisfying the usual properties as soundness and adequacy, these models validate the permutation rules mentioned above as well as some reductions obtained by contracting suitable λI-redexes. Thanks to these (perhaps unexpected) features, we are able to demonstrate that every model living in this class satisfies an Approximation Theorem with respect to a refined notion of syntactic approximant. While this kind of results often require impredicative techniques like reducibility candidates, the quantitative information carried by type derivations in our system allows us to provide a combinatorial proof. [ABSTRACT FROM AUTHOR]

We study a version of the Stone duality between the Alexandrov spaces and the completely distributive algebraic lattices. This enables us to present lattice-theoretical models of second-order intuitionistic propositional logic which correlates with the Kripke models introduced by Sobolev. This can be regarded as a second-order extension of the well-known correspondence between Heyting algebras and Kripke models in the semantics of intuitionistic propositional logic. [ABSTRACT FROM AUTHOR]

Graph Neural Networks (GNNs) have received considerable attention in recent years due to their unique ability to model both topologies and semantics in the graphs. In this paper, we explore the use of GNNs in learning low-dimensional node representations in Heterogeneous Information Networks (HINs), which retain rich semantic information across multiple types of nodes and relations. Existing methods for HINs generally focus on modeling heterogeneity at either the node level or the relation level, but not both. As a result, these methods often fall short of optimal performance. To address this issue, we propose a novel Semantic- and Relation-aware Heterogeneous Graph neural Network, dubbed SR-HGN, which jointly incorporates rich semantics preserved on nodes and relations. Our approach involves projecting the HINs into a low-dimensional vector space through two steps: node-level aggregation and type-level aggregation. The node-level aggregation employs an attention mechanism to create relation vectors by aggregating messages from neighborhoods connected via the same type of relation. The type-level aggregation leverages relation vectors to aggregate node representations. In particular, we introduce semantic-aware attention and relation-aware attention in the type-level aggregation to model the contributions of relation vectors, in order to simultaneously gain knowledge from node semantics and relational information. Unlike other approaches that rely on pre-defined meta-paths, our model can be readily applied to most real-world applications without requiring any domain knowledge. To validate the effectiveness of our proposed approach, we conducted extensive experiments on three public datasets. Experimental results demonstrate that the SR-HGN significantly outperforms state-of-the-art baselines on node classification and node clustering tasks. [ABSTRACT FROM AUTHOR]

Relational triple extraction is aimed at detecting entity pairs with relations from sentences, which is a key technology for large-scale knowledge graph construction. Recent studies focus on the overlapping triple problem, where multiple relational triples may have overlaps in a sentence. However, these methods disregard the bidirectionality of triple extraction, which may lead to extracting invalid triples. In addition, many relational triples are labeled in datasets of the triple extraction task, implying domain knowledge information of these datasets, but current methods rarely consider it. In this paper, we present a bidirectional relation-guided attention network with semantics and knowledge (BRASK) for relational triple extraction. BRASK is a bidirectional extraction framework that is based on multitask learning and contains forward and backward triple extraction tasks. Forward triple extraction and backward triple extraction are parallel and complementary, which can obtain predicted results with high confidence. We utilize semantic relations and knowledge relations as guidance in forward triple extraction and backward triple extraction, respectively, thus integrating general and domain knowledge into our model. In addition, we adopt an attention mechanism to learn fine-grained sentence representations for different relations. BRASK can solve the triple overlap problem and capture bidirectional dependencies between subjects and objects. Experimental results show that BRASK achieves new state-of-the-art results in two public datasets, which demonstrates its effectiveness. [ABSTRACT FROM AUTHOR]

The sentences employed in semantic paradoxes display a wide range of semantic behaviours. However, the main theories of truth currently available either fail to provide a theory of paradox altogether, or can only account for some paradoxical phenomena by resorting to multiple interpretations of the language, as in (Kripke, 1975). In this article, I explore the wide range of semantic behaviours displayed by paradoxical sentences, and I develop a unified theory of truth and paradox , that is a theory of truth that also provides a unified account of paradoxical sentences. The theory I propose here yields a threefold classification of paradoxical sentences—liar-like sentences, truth-teller–like sentences, and revenge sentences. Unlike existing treatments of semantic paradox, the theory put forward in this article yields a way of interpreting all three kinds of paradoxical sentences, as well as unparadoxical sentences, within a single model. [ABSTRACT FROM AUTHOR]

Modal logic S5 is commonly viewed as an epistemic logic that captures the most basic properties of knowledge. Kripke proved a completeness theorem for the first-order modal logic S5 with respect to a possible worlds semantics. A multiagent version of the propositional S5 as well as a version of the propositional S5 that describes properties of distributed knowledge in multiagent systems has also been previously studied. This article proposes a version of S5-like epistemic logic of distributed knowledge with quantifiers ranging over the set of agents, and proves its soundness and completeness with respect to a Kripke semantics. [ABSTRACT FROM AUTHOR]

In this paper, I propose and defend a solution to Kripke's puzzle about time and thought, which lives in harmony with the axiom schema of separation and does not invoke paraconsistency. I also compare my solution with Parikh's semantic interpretation, and answer to three potential objections. [ABSTRACT FROM AUTHOR]

Conditional logics have traditionally been intended to formalize various intuitively correct modes of reasoning involving (counterfactual) conditional expressions in natural language. Although conditional logics have by now been thoroughly studied in a classical context, they have yet to be systematically examined in an intuitionistic context, despite compelling philosophical and technical reasons to do so. This paper addresses this gap by thoroughly examining the basic intuitionistic conditional logic ICK, the intuitionistic counterpart of Chellas' important classical system CK. I give ICK both worlds semantics and algebraic semantics, and prove that these are equivalent. I give a Gödel-type embedding of ICK into CK (augmented with an S4 box connective) and a Glivenko-type embedding of CK into ICK. I axiomatize ICK and prove soundness, completeness, and decidability results. Finally, I discuss extending ICK. [ABSTRACT FROM AUTHOR]

The classification-cum-explanation Kripke assigns to rigidity requires the notion to apply to singular and general terms alike. But Kripke's own notion of rigidity is tailor-made for singular terms, and an extensive debate has not secured a general notion of rigidity apt to provide the classification-cum-explanation Kripke aims for. I propose that we look for a Kripkean alternative to generalized rigidity. I argue that on Kripkean premises, natural kind terms and proper names belong to the meta-semantic category of paradigm terms. I also argue that the property of being a paradigm term effects precisely the classification-cum-explanation Kripke attributes to rigidity. I conclude that Kripkeans should acknowledge that being a paradigm term, rather than designating rigidly, plays the role Kripke delineates, and that we can stop worrying about generalizing rigidity. Kripke's notion works fine for singular terms. And there is no need for rigidity to apply beyond these. [ABSTRACT FROM AUTHOR]

Frame semantics, given by Kripke or neighborhood frames, do not give completeness theorems for all modal logics extending, respectively, K and E. Such shortcoming can be overcome by means of general frames, i.e., frames equipped with a collection of admissible sets of worlds (which is the range of possible valuations over such frame). We export this approach from the classical paradigm to modal many-valued logics by defining general A-frames over a given residuated lattice A (i.e., the usual frames with a collection of admissible A-valued sets). We describe in detail the relation between general Kripke and neighborhood A-frames and prove that, if the logic of A is finitary, all extensions of the corresponding logic E of A are complete w.r.t. general neighborhood frames. Our work provides a new approach to the current research trend of generalizing relational semantics for non-classical modal logics to circumvent axiomatization problems. [ABSTRACT FROM AUTHOR]

This study aims at discussing the encyclopedic nature of semantic frames and their role in lexicographic practice. In theoretical terms, we try to understand the vision of Charles Fillmore (1982, 1992) with the proposition of Frames Semantics, as well as to seek in Cognitive Linguistics its principles. In applied terms, we focused on the interface between Frames Semantic and Lexicography and presented, in the sequence, two case studies, both highlighting the encyclopedic vision of the frames and their relevance to the lexicographic practice. We emphasize, finally, the occupation of a specific niche of research, as we return only to the semantic frames. It is noteworthy that other topics of Cognitive Semantics also have their relevance for lexicography. [ABSTRACT FROM AUTHOR]

The present study aims to analyze selected internet memes as examples of social communication from the perspective of Cognitive Linguistics, and to examine more closely the relation between their visual and verbal aspects. Internet memes contain a wide range of constructions (necessary for rebuilding the semantic framework and extracting selected content), which are fragmentary but at the same time sufficient to induce a whole framework of meanings by using their salient features. The multimodal context is considered within the frameworks of conceptual metaphor theory (Lakoff & Johnson, 1980), construal (Langacker, 1987, 2008), frame semantics (Fillmore, 1988), conceptual blending theory (Fauconnier & Turner, 2002) and Discourse Viewpoint Space (Dancygier & Vandelanotte, 2016). The paper will present an analysis of the structure of internet memes, which are rich concepts that spread rapidly and widely, and also invite recipients to actively participate in the construction of the message, thus becoming contributors. [ABSTRACT FROM AUTHOR]

In two recent articles, Norihiro Kamide introduces unusual variants of Nelson's paraconsistent logic and its classical extension. Kamide's systems, IP and CP , are unusual insofar as double negations in these logics behave as intuitionistic and classical negations, respectively. In this article we present Hilbert-style axiomatizations of both IP and CP. The axiom system for IP is shown to be sound and complete with respect to a four-valued Kripke semantics, and the axiom system for CP is characterized by four-valued truth tables. Moreover, we note some properties of IP and CP , and emphasize that these logics are unusual also because they are contra-classical and inconsistent but nontrivial. We point out that Kamide's approach exemplifies a general method for obtaining contra-classical logics, and we briefly speculate about a linguistic application of Kamide's logics. [ABSTRACT FROM AUTHOR]

The best we can do is appeal to a set HT ht , the I worlds i of the context. HT ht But perhaps my reasoning was specious on metaphysical grounds - that is, from the very opening move according to which we should see context as selecting a mere set HT ht of candidates for actuality. "Julius" expresses a "cheesy mode of presentation" (Dorr et al., [9]) of one of the available acts HT ht in Figure. Free Choice is provable in this framework given that each embedded disjunct of e.g. (4a) is HT ht -accessible to the agent ( I op. cit i ., Theorem 1). [Extracted from the article]

Orthologic (OL) is non-classical logic and has been studied as a part of quantum logic. OL is based on an ortholattice and is also called minimal quantum logic. Sequent calculus is used as a tool for proof in logic and has been examined for several decades. Although there are many studies on sequent calculus for OL, these sequent calculi have some problems. In particular, they do not include implication connective and they are mostly incompatible with the cut-elimination theorem. In this paper, we introduce new labeled sequent calculus called LGOI, and show that this sequent calculus solve the above problems. It is already known that OL is decidable. We prove that decidability is preserved when the implication connective is added to OL. [ABSTRACT FROM AUTHOR]

Since the advent of BAN logic, many logics have been proposed for verifying authentication protocols. In one line of research, scholars have presented logics that can be utilized in verifying timed requirements of the protocols. Although many temporal epistemic logics have been developed to this end, there is no complete logic of this kind to prevent logical omniscience. Thus, they may lead to misleading judgments about the properties of the protocol being analyzed. In this paper, we propose a complete and omniscience-free temporal epistemic logic for analyzing authentication protocols. The main challenging issue in devising this logic is formulating intuitive models that on one hand reflect what is naturally meant by a protocol execution and on the other hand make it possible to achieve properties such as completeness. We show that such models can build on interpreted systems and that the resulting logic is useful in analyzing authentication protocols. [ABSTRACT FROM AUTHOR]

Abstract Some temporal properties of reactive systems, such as actions with duration and temporal aggregations, which are inherently interval-based, can not be properly expressed by the standard, point-based temporal logics LTL, CTL and CTL⁎, as they give a state-by-state account of system evolution. Conversely, interval temporal logics—which feature intervals, instead of points, as their primitive entities—naturally express them. We study the model checking (MC) problem for Halpern and Shoham's modal logic of time intervals (HS), interpreted on Kripke structures, under the homogeneity assumption. HS is the best known interval-based temporal logic, which has one modality for each of the 13 ordering relations between pairs of intervals (Allen's relations), apart from equality. We focus on MC for some HS fragments featuring modalities for (a subset of) Allen's relations meet, met-by, started-by, and finished-by, showing that it is in P NP. Additionally, we provide some complexity lower bounds to the problem. [ABSTRACT FROM AUTHOR]

Kripke’s theory of truth is arguably the most influential approach to self-referential truth and the semantic paradoxes. The use of a partial evaluation scheme is crucial to the theory and the most prominent schemes that are adopted are the strong Kleene and the supervaluation scheme. The strong Kleene scheme is attractive because it ensures the compositionality of the notion of truth. But under the strong Kleene scheme classical tautologies do not, in general, turn out to be true and, as a consequence, classical reasoning is no longer admissible once the notion of truth is involved. The supervaluation scheme adheres to classical reasoning but violates compositionality. Moreover, it turns Kripke’s theory into a rather complicated affair: to check whether a sentence is true we have to look at all admissible precisification of the interpretation of the truth predicate we are presented with. One consequence of this complicated evaluation condition is that under the supervaluation scheme a more proof-theoretic characterization of Kripke’s theory becomes inherently difficult, if not impossible. In this paper we explore the middle ground between the strong Kleene and the supervaluation scheme and provide an evaluation scheme that adheres to classical reasoning but retains many of the attractive features of the strong Kleene scheme. We supplement our semantic investigation with a novel axiomatic theory of truth that matches the semantic theory we have put forth. [ABSTRACT FROM AUTHOR]

The majority of works on modal many-valued logics consider Kripke-style possible worlds frames as the principal semantics despite their well-known axiomatizability issues when considering non-Boolean accessibility relations. The present work explores a more general semantical picture, namely a many-valued version of the classical neighborhood semantics. We present it in two levels of generality. First, we work with modal languages containing only the two usual unary modalities, define neighborhood frames over algebras of the logic FL ew with operators, and show their relation with the usual Kripke semantics (this is actually the highest level of generality where one can give a straightforward definition of the Kripke-style semantics). Second, we define generalized neighborhood frames for arbitrary modal languages over a given class of algebras for an arbitrary protoalgebraic logic and, assuming certain additional conditions, axiomatize the logic of all such frames (which generalizes the completeness theorem of the classical modal logic E with respect to classical neighborhood frames). [ABSTRACT FROM AUTHOR]

In this paper we study several translations that map models and formulae of the language of second-order arithmetic to models and formulae of the language of truth. These translations are useful because they allow us to exploit results from the extensive literature on arithmetic to study the notion of truth. Our purpose is to present these connections in a systematic way, generalize some well-known results in this area, and to provide a number of new results. Sections 3 and 4 contain some recursion- and proof-theoretic results about Kripke-style fixed-point theories of truth. Section 5 shows how to derive full second-order arithmetic from principles of truth. Section 6 investigates the proof-theoretic strength of disquotation without an arithmetical base theory. [ABSTRACT FROM AUTHOR]

The fragment of the language of modal logic that consists of all implications A → B, where A and B are built from variables, the constant ⊤ (truth), and the connectives ∧ and ◊1,◊2,...,◊m. For the polymodal logic S5m (the logic of m equivalence relations) and the logic K4.3 (the logic of irreflexive linear orders), an axiomatization of such fragments is found and their algorithmic decidability in polynomial time is proved. [ABSTRACT FROM AUTHOR]

We define a Kripke semantics for Intuitionistic Higher-Order Logic with constraints formulated within Church's Theory of Types via the addition of a new constraint base type. We then define an executable fragment, hoHH ( C ) , of the logic: a higher-order logic programming language with typed λ -abstraction, implication and universal quantification in goals and constraints, and give a modified model theory for this fragment. Both formal systems are shown sound and complete for their respective semantics. We also solve the impredicativity problem in λ Prolog semantics, namely how to give a definition of truth without appealing to induction on subformula structure. In the last section we give a simple semantics-based conservative extension proof that the language hoHH ( C ) satisfies a uniformity property along the lines of [39] . [ABSTRACT FROM AUTHOR]

We provide the first algorithm with a polynomial time complexity, O((m + n)2n2), for computing the largest bisimulation-based auto-comparison of a labeled graph in the setting with counting successors, where m is the number of edges and n is the number of vertices. This setting is like the case with graded modalities in modal logics and qualified number restrictions in description logics. Furthermore, by using the idea of Henzinger et al. for computing simulations, we give an efficient algorithm, with complexity O((m + n)n), for computing the largest bisimulation-based auto-comparison and the directed similarity relation of a labeled graph in the setting without counting successors. We also adapt our former algorithm for computing the simulation pre-order of a labeled graph in the setting with counting successors. [ABSTRACT FROM AUTHOR]

Kripke frames (and models) provide a suitable semantics for sub-classical logics; for example, intuitionistic logic (of Brouwer and Heyting) axiomatizes the reflexive and transitive Kripke frames (with persistent satisfaction relations), and the basic logic (of Visser) axiomatizes transitive Kripke frames (with persistent satisfaction relations). Here, we investigate whether Kripke frames/models could provide a semantics for fuzzy logics. For each axiom of the basic fuzzy logic, necessary and sufficient conditions are sought for Kripke frames/models which satisfy them. It turns out that the only fuzzy logics (logics containing the basic fuzzy logic) which are sound and complete with respect to a class of Kripke frames/models are the extensions of the Gödel logic (or the super-intuitionistic logic of Dummett); indeed this logic is sound and strongly complete with respect to reflexive, transitive and connected (linear) Kripke frames (with persistent satisfaction relations). This provides a semantic characterization for the Gödel logic among (propositional) fuzzy logics. [ABSTRACT FROM AUTHOR]

In this paper, we introduce a proof system NQGL for a Kripke complete predicate extension of the logic GL of provability. While GL is defined by K and the Lβb formula ✷(✷p ⊃ p) ⊃ ✷p, NQGL does not have the Lβb formula as its axiom, but has a non-compact rule, that is, a derivation rule with countably many premises, instead. We show that NQGL enjoys cut admissibility and is complete with respect to the class of Kripke frames such that for each world, the supremum of the length of the paths from the world is finite. [ABSTRACT FROM AUTHOR]

We analyze semantically the logical inference rules in cut-free sequent calculi for the modal logics which are obtained from the least normal logic K by adding axioms from T, 4, 5, D and B. This implies Kripke completeness, as well as the cut- elimination property or the subformula property of the calculi. By slightly modifying the arguments, the finite model property of the logics also follows. [ABSTRACT FROM AUTHOR]

I offer a skeptical reading of Saul Kripke's "A Puzzle about Belief." I maintain that Kripke formulates a skeptical paradox about belief that is analogous to the skeptical paradox about meaning and rule-following that, according to Kripke, Wittgenstein formulates in his Philosophical Investigations. [ABSTRACT FROM AUTHOR]

In this paper we develope a Kripke style semantic for the logic of two-valued states on orthomodular lattices. Kripke models are built from Baer semigroups enriched with an unary operation. A completeness theorem with respect to this Kripkean semantic is established. [ABSTRACT FROM AUTHOR]

We consider two classifications of extensions of Johansson's minimal logic J. Logics and then calculi are divided into levels and slices with numbers from 0 to ω. We prove that the first classification is strongly decidable over J, i.e., from any finite list Rul of axiom schemes and inference rules, we can effectively compute the level number of the calculus ( J + Rul). We prove the strong decidability of each slice with finite number: for each n and arbitrary finite Rul, we can effectively check whether the calculus ( J + Rul) belongs to the nth slice. [ABSTRACT FROM AUTHOR]

Recently, we have shown that satisfiability for the temporal logic E C T L with local constraints over (ℤ, <, =) is decidable using a new technique (Carapelle et al., 2013). This approach reduces the satisfiability problem of E C T L with constraints over some structure $\mathcal {A}$ (or class of structures) to the problem whether $\mathcal {A}$ has a certain model theoretic property that we called EHD (for 'existence of homomorphisms is definable'). Here we apply this approach to structures that are tree-like and obtain several results. We show that satisfiability of E C T L with constraints is decidable over (i) semi-linear orders (i.e., tree-like structures where branches form arbitrary linear orders), (ii) ordinal trees (semi-linear orders where the branches form ordinals), and (iii) infinitely branching trees of height h for each fixed $h\in \mathbb {N}$ . We prove that all these classes of structures have the property EHD. In contrast, we introduce Ehrenfeucht-Fraïssé-games for W M S O + B (weak M S O with the bounding quantifier) and use them to show that the infinite (order) tree does not have the EHD-property. As a consequence, our technique cannot be used to establish whether satisfiability of E C T L with constraints over the infinite (order) tree is decidable. A preliminary version of this paper has appeared as (Carapelle et al., 2015). [ABSTRACT FROM AUTHOR]

We present a sound and complete graph calculus for modalities. This calculus is a general framework for expressing modal formulas and frame properties, with a rich repertoire of relations, and reasoning about them in a uniform manner. The calculus employs graphical interpretations of logical operators and builds graphical objects that represent conditions on Kripke structures. [ABSTRACT FROM AUTHOR]

The paper studies completeness and incompleteness of modal predicate logics in Kripke semantics, especially for logics of the form Q Λ , minimal predicate extensions of modal propositional logics. We show that Q Λ is incomplete for a continual family of logics Λ above K + □ (□ p → p) , in particular for well-known K5 and K45. On the other hand, in some cases we find completions of Q Λ ; they are obtained by adding a single extra axiom. Completeness proofs use canonical models, with some modifications, and the case of QK5 is the most interesting from the technical side. We also introduce the "boxing" operation for modal predicate logics and prove transfer results for Kripke and Kripke sheaf completeness with respect to this operation. [ABSTRACT FROM AUTHOR]

Theories of reference are a crucial research topic in analytic philosophy. Since the publication of Kripke's Naming and Necessity, most philosophers have endorsed the causal/historical theory of reference. The goal of this paper is twofold: (i) to discuss a method for testing experimentally the causal theory of reference for proper names by investigating linguistic usage and (ii) to present the results from two experiments conducted with that method. Data collected in our experiments confirm the causal theory of reference for people proper names and for geographical proper names. A secondary but interesting result is that the semantic domain affects reference assignment: while with people proper names speakers tend to assign the semantic reference, with geographical proper names they are prompted to assign the speaker's reference. [ABSTRACT FROM AUTHOR]

We study what languages can be constructed from a non-regular language L using Boolean operations and synchronous or non-synchronous rational transductions. If all rational transductions are allowed, one can construct the whole arithmetical hierarchy relative to L. In the case of synchronous rational transductions, we present non-regular languages that allow constructing languages arbitrarily high in the arithmetical hierarchy and we present non-regular languages that allow constructing only recursive languages. A consequence of the results is that aside from the regular languages, no full trio generated by a single language is closed under complementation. Another consequence is that there is a fixed rational Kripke frame such that assigning an arbitrary non-regular language to some variable allows the definition of any language from the arithmetical hierarchy in the corresponding Kripke structure using multimodal logic. [ABSTRACT FROM AUTHOR]

The main objective of this article is to present a complete finite black-box testing theory for non-deterministic Kripke structures with possibly infinite input domains, but finite domains for internal state variables and outputs. To this end, an abstraction from Kripke structures of this sub-domain to finite state machines is developed. It is shown that every complete black-box testing theory for (deterministic or nondeterministic) finite state machines in the range of this abstraction induces a complete black-box input equivalence class partition testing (IECPT) theory for the Kripke structures under consideration. Additionally, it is shown that each of these IECPT theories can be combined with random testing, such that a random value is selected from an input equivalence class, whenever a representative from this class is required in a test step. Experiments have shown that this combination increases the test strength of equivalence class tests for systems under test (SUT) outside the fault domain, while we show here that this randomisation preserves the completeness property for SUT inside the domain. The investigations lead to several complete IECPT strategies which, to our best knowledge, were not known before for this sub-domain of Kripke structures. The elaboration and presentation of results is performed on a semantic level, so that the testing theories under consideration can be applied to models presented in any concrete formalism, whose behaviour is reflected by a member of our semantic category. [ABSTRACT FROM AUTHOR]

We study the measure semantics for propositional modal logics, in which formulas are interpreted in the Lebesgue measure algebra${\cal M}$, or algebra of Borel subsets of the real interval [0,1] modulo sets of measure zero. It was shown in Lando (2012) and Fernández-Duque (2010) that the propositional modal logic S4 is complete for the Lebesgue measure algebra. The main result of the present paper is that every logic L aboveS4 is complete for some subalgebra of ${\cal M}$. Indeed, there is a single model over a subalgebra of ${\cal M}$ in which all nontheorems of L are refuted. This work builds on recent work by Bezhanishvili, Gabelaia, & Lucero-Bryan (2015) on the topological semantics for logics above S4. In Bezhanishvili et al., (2015), it is shown that there are logics above that are not the logic of any subalgebra of the interior algebra over the real line, ${\cal B}$(ℝ), but that every logic above is the logic of some subalgebra of the interior algebra over the rationals, ${\cal B}$(ℚ), and the interior algebra over Cantor space, ${\cal B}\left( {\cal C} \right)$. [ABSTRACT FROM PUBLISHER]

We discuss relationships among the existence property, the disjunction property, and their weak variants in the setting of intermediate predicate logics. We deal with the weak and sentential existence properties, and the Z-normality, which is a weak variant of the disjunction property. These weak variants were presented in the author's previous paper [16]. In the present paper, the Kripke sheaf semantics is used. [ABSTRACT FROM AUTHOR]

Justification logics are modal-like logics that provide a framework for reasoning about justifications. This paper introduces labeled sequent calculi for justification logics, as well as for combined modal-justification logics. Using a method due to Sara Negri, we internalize the Kripke-style semantics of justification and modal-justification logics, known as Fitting models, within the syntax of the sequent calculus to produce labeled sequent calculi. We show that all rules of these systems are invertible and the structural rules (weakening and contraction) and the cut rule are admissible. Soundness and completeness are established as well. The analyticity for some of our labeled sequent calculi are shown by proving that they enjoy the subformula, sublabel and subterm properties. We also present an analytic labeled sequent calculus for S4LPN based on Artemov–Fitting models. [ABSTRACT FROM AUTHOR]

We show that logics based on linear Kripke frames-with or without constant domains-that have a scattered end piece are not recursively enumerable. This is done by reduction to validity in all finite classical models. [ABSTRACT FROM AUTHOR]

Minimal logic, i.e., intuitionistic logic without the ex falso principle, is investigated in its original form with a negation symbol instead of a symbol denoting the contradiction. A Kripke semantics is developed for minimal logic and its sublogics with a still weaker negation by introducing a function on the upward closed sets of the models. The basic logic is a logic in which the negation has no properties but the one of being a unary operator. A number of extensions is studied of which the most important ones are contraposition logic and negative ex falso, a weak form of the ex falso principle. Completeness is proved, and the created semantics is further studied. The negative translation of classical logic into intuitionistic logic is made part of a chain of translations by introducing translations from minimal logic into contraposition logic and intuitionistic logic into minimal logic, the latter having been discovered in the correspondence between Johansson and Heyting. Finally, as a bridge to the work of Franco Montagna a start is made of a study of linear models of these logics. [ABSTRACT FROM AUTHOR]

Model checking is a powerful method widely explored in formal verification. Given a model of a system, e.g., a Kripke structure, and a formula specifying its expected behaviour, one can verify whether the system meets the behaviour by checking the formula against the model. Classically, system behaviour is expressed by a formula of a temporal logic, such as LTL and the like. These logics are 'point-wise' interpreted, as they describe how the system evolves state-by-state. However, there are relevant properties, such as those constraining the temporal relations between pairs of temporally extended events or involving temporal aggregations, which are inherently 'interval-based', and thus asking for an interval temporal logic. In this paper, we give a formalization of the model checking problem in an interval logic setting. First, we provide an interpretation of formulas of Halpern and Shoham's interval temporal logic HS over finite Kripke structures, which allows one to check interval properties of computations. Then, we prove that the model checking problem for HS against finite Kripke structures is decidable by a suitable small model theorem, and we provide a lower bound to its computational complexity. [ABSTRACT FROM AUTHOR]

Kripke's theory of truth (Kripke, The Journal of Philosophy 72(19), 690-716; 1975) has been very successful but shows well-known expressive difficulties; recently, Field has proposed to overcome them by adding a new conditional connective to it. In Field's theories, desirable conditional and truth-theoretic principles are validated that Kripke's theory does not yield. Some authors, however, are dissatisfied with certain aspects of Field's theories, in particular the high complexity. I analyze Field's models and pin down some reasons for discontent with them, focusing on the meaning of the new conditional and on the status of the principles so successfully recovered. Subsequently, I develop a semantics that improves on Kripke's theory following Field's program of adding a conditional to it, using some inductive constructions that include Kripke's one and feature a strong evaluation for conditionals. The new theory overcomes several problems of Kripke's one and, although weaker than Field's proposals, it avoids the difficulties that affect them; at the same time, the new theory turns out to be quite simple. Moreover, the new construction can be used to model various conceptions of what a conditional connective is, in ways that are precluded to both Kripke's and Field's theories. [ABSTRACT FROM AUTHOR]

I analyse Kripke's modal argument against the mind-brain identity theories. Specifically, he argues against the identity between pain and C-fibres simulation by pointing out the difference between this identity claim and the theoretical identifications, such as 'Water is H2O' and 'Lightning is a motion of electric charges'. Kripke's argument relies on the assumption that the experience of pains is a simple and homogenous phenomenon, but scientific research shows that it is in fact a quite complex one. We can distinguish at least three components: sensory-discriminative, motivational-affective and cognitive. This discovery makes it possible to reject Kripke's argument, but it also uncovers a major flaw that is common to all modal arguments against physicalism. They proclaim to answer the fundamental question about the nature of our world by relying on our powers of imagination and without having the relevant factual knowledge. [ABSTRACT FROM AUTHOR]

In [1], we introduced a classification of extensions of Johansson's minimal logic J by means of slices and proved the decidability of the classification. In this article, we find sufficiently simple necessary conditions for the maximality of logics in the slices formulated in terms of frames. This makes it possible to describe an efficient procedure for computing the slice number of any finitely axiomatizable logic over J. The maximal logics of the upper slices are written down explicitly. [ABSTRACT FROM AUTHOR]

Kripke models, interpreted realistically, have difficulty making sense of the thesis that there might have existed things that do not in fact exist, since a Kripke model in which this thesis is true requires a model structure in which there are possible worlds with domains that contain things that do not exist. This paper argues that we can use Kripke models as representational devices that allow us to give a realistic interpretation of a modal language. The method of doing this is sketched, with the help of an analogy with a Galilean relativist theory of spatial properties and relations. [ABSTRACT FROM AUTHOR]

We present a Kripke logical relation for showing the correctness of program transformations based on a region-polymorphic type-and-effect system for an ML-like programming language with higher-order store and dynamic allocation. We also show how to use our model to verify a number of interesting program transformations that rely on effect annotations. In building the model, we extend earlier work by Benton et al. that treated, respectively dynamically allocated first-order references, and higher-order store for global variables. We utilize ideas from region-based memory management, and on Kripke logical relations for higher-order store. One of the key challenges that we overcome in the construction of the model is treatment of masking of regions (conceptually similar to deallocation). Our approach bears similarities to the one used in Ahmed's unary model of a region calculus in her Ph.D. thesis. [ABSTRACT FROM AUTHOR]