Search

The present paper attempts to provide an exact truthmaker semantical analysis of modalized propositions. According to the present proposal, an exact truthmaker for "Necessarily P" is a state that bans every exact truthmaker for "Not P", and an exact truthmaker for "Possibly P" is a state that allows an exact truthmaker for P. Based on this proposal, a formal semantics will be developed; and the soundness and completeness results for a well-known family of the systems of normal modal propositional logic will be established. It shall be seen that the present analysis offers an exactification of the standard Kripke semantics in the sense that it analyzes the accessibility relation between possible worlds in terms of the banning and allowing relations between the constituent states, and thereby gives an account of "truth at a possible world" in terms of exact truthmaking. [ABSTRACT FROM AUTHOR]

Graph-based frames have been introduced as a logical framework which internalises an inherent boundary to knowability (referred to as 'informational entropy'), due, e.g. to perceptual, evidential or linguistic limits. They also support the interpretation of lattice-based (modal) logics as hyper-constructive logics of evidential reasoning. Conceptually, the present paper proposes graph-based frames as a formal framework suitable for generalising Pawlak's rough set theory to a setting in which inherent limits to knowability exist and need to be considered. Technically, the present paper establishes systematic connections between the first-order correspondents of Sahlqvist modal reduction principles on Kripke frames, and on the more general relational environments of graph-based and polarity-based frames. This work is part of a research line aiming at: (a) comparing and inter-relating the various (first-order) conditions corresponding to a given (modal) axiom in different relational semantics; (b) recognising when first-order sentences in the frame-correspondence languages of different relational structures encode the same 'modal content'; (c) meaningfully transferring relational properties across different semantic contexts. The present paper develops these results for the graph-based semantics, polarity-based semantics, and all Sahlqvist modal reduction principles. As an application, we study well known modal axioms in rough set theory (such as those corresponding to seriality, reflexivity, and transitivity) on graph-based frames and show that, although these axioms correspond to different first-order conditions on graph-based frames, their intuitive meaning is retained. This allows us to introduce the notion of hyperconstructivist approximation spaces as the subclass of graph-based frames defined by the first-order conditions corresponding to the same modal axioms defining classical generalised approximation spaces, and to transfer the properties and the intuitive understanding of different approximation spaces to the more general framework of graph-based frames. The approach presented in this paper provides a base for systematically comparing and connecting various formal frameworks in rough set theory, and for the transfer of insights across different frameworks. [ABSTRACT FROM AUTHOR]

The article "Quantification, matching and events" by Richard K. Larson discusses the topic of quantification and matching in natural language semantics. The author explores examples of quantification and argues that the truth conditions of these statements involve matching between different elements. The article proposes that matching in quantification arises from the internal semantic structure of the quantifier and suggests that all quantifiers can be analyzed as having an underlying structure involving injections into events. The author also addresses the role of context, the difference between unbound pronouns and variables bound by existential quantifiers, and different analyses of sentences involving quantification and matching. The text concludes by discussing the connection between quantification, matching, and events, and argues that events, injections, and matching are central to all quantification. The article also explores the need for quantificational states in the semantics of adverbial quantifiers and proposes a neo-Davidsonian approach to understanding quantification. The text discusses semantic rules for quantifiers and provides a framework for understanding quantification in natural language. Finally, the author discusses the topic of quantification in relation to adverbial quantification and argues that all quantifiers involve matching. [Extracted from the article]

We introduce dual counterpart intuitionistic logic (or DCInt): a constructive logic that is a conservative extension of intuitionistic logic, a sublogic of bi-intuitionistic logic, has the logical duality property of classical logic, and also retains the modal character of its interpretation of the connective dual to intuitionistic implication. We define its Kripke semantics along with the corresponding notion of a bisimulation, and then prove that it has both the disjunction property and (its dual) the constructible falsity property. Also, for any class |$ {\mathcal{C}}$| of Kripke frames from our semantics, we identify a condition such that |$ {\mathcal{C}}$| will have the disjunction property if it satisfies the condition. This provides a method for generating extensions of DCInt that retain the disjunction property. [ABSTRACT FROM AUTHOR]

Image-text matching plays an important role in solving the problem of cross-modal information processing. Since there are nonnegligible semantic differences between heterogenous pairwise data, a crucial challenge is how to learn a unified representation. Existing methods mainly rely on the alignment between regional image features and corresponding entity words. However, the regional features in the image are often more concerned with the foreground entity information, and the attribute information of the entities and the relational information are ignored. How to effectively integrate entity-attribute alignment and relationship alignment has not been fully studied. Therefore, we propose a Cross-Modal Semantically Augmented Network for Image-Text Matching (CMSAN), which combines the relationships between entities in the image with the semantics of relational words in the text. CMSAN (1) proposes an adaptive word-type prediction model that classifies the words into four types, i.e., entity word, attribute word, relation word, and unnecessary word. It can align different image features at multiple levels. CMSAN (2) designs a sophisticated relationship alignment module and an entity-attribute alignment module that maximizes the exploitation of the semantic information, which enables the model to have more discriminative power and further improves the matching accuracy. [ABSTRACT FROM AUTHOR]

Graph neural networks (GNNs) excel in modeling relational data such as biological, social, and transportation networks, but the underpinnings of their success are not well understood. Traditional complexity measures from statistical learning theory fail to account for observed phenomena like the double descent or the impact of relational semantics on generalization error. Motivated by experimental observations of "transductive" double descent in key networks and datasets, we use analytical tools from statistical physics and random matrix theory to precisely characterize generalization in simple graph convolution networks on the contextual stochastic block model. Our results illuminate the nuances of learning on homophilic versus heterophilic data and predict double descent whose existence in GNNs has been questioned by recent work. We show how risk is shaped by the interplay between the graph noise, feature noise, and the number of training labels. Our findings apply beyond stylized models, capturing qualitative trends in real-world GNNs and datasets. As a case in point, we use our analytic insights to improve performance of state-of-the-art graph convolution networks on heterophilic datasets. [ABSTRACT FROM AUTHOR]

This paper investigates the implicative conditional, a connective intended to describe the logical behavior of an empirically defined class of natural language conditionals, also named implicative conditionals, which excludes concessive and some other conditionals. The implicative conditional strengthens the strict conditional with the possibility of the antecedent and of the contradictory of the consequent. p ⇒ q is thus defined as ¬ ◊ (p ∧ ¬ q) ∧ ◊ p ∧ ◊ ¬ q . We explore the logical properties of this conditional in a reflexive normal Kripke semantics, provide an axiomatic system and prove it to be sound and complete for our semantics. The implicative conditional validates transitivity and contraposition, which we take to be integral parts of reasoning and communication. But it only validates restricted versions of strengthening the antecedent, right weakening, simplification, and rational monotonicity. Apparent counterexamples to some of these properties are explained as due to contextual factors. Finally, the implicative conditional avoids the paradoxes of material and strict implication, and validates some connexive principles such as Aristotle's theses and weak Boethius' thesis, as well as some highly entrenched principles of conditionals, such as conjunction of consequents, disjunction of antecedents, modus ponens, cautious monotonicity and cut. [ABSTRACT FROM AUTHOR]

We show that intuitionistic propositional logic is Carnap categorical: the only interpretation of the connectives consistent with the intuitionistic consequence relation is the standard interpretation. This holds with respect to the most well-known semantics relative to which intuitionistic logic is sound and complete; among them Kripke semantics, Beth semantics, Dragalin semantics, topological semantics, and algebraic semantics. These facts turn out to be consequences of an observation about interpretations in Heyting algebras. [ABSTRACT FROM AUTHOR]

With mental models based on relational information, the present research shows that the semantics expressed by the relation can determine the structural properties of the constructed model. In particular, we demonstrate a reversal of the classical, well-replicated symbolic distance effect (SDE), as a function of relational semantics. The classical SDE shows that responses are more accurate, and faster, the wider the distance between queried elements on a mentally constructed rank order. We replicate this effect in a study using a relation that expresses a rank hierarchy ("older than," Experiment 4). In contrast, we obtain a clear reversal of the same effect for accuracy data when the relation expresses a number of equivalence classes ("is from the same city," Experiments 1–3). In Experiment 3, we find clear evidence of a reversed SDE for accuracy and latency in the above standard condition, and flat curves of means, across pair distances, for accuracy and latency in a condition that makes equivalence classes salient from the beginning. We discuss these findings in the context of a process model of equivalence class formation based on learned piecemeal information. [ABSTRACT FROM AUTHOR]

In a reactive Kripke model, evaluation of logical operators can cause reconfiguration of the model in which the formula is evaluated. Therefore, in reactive Kripke frames, the evaluation of a logical formula in a world depends both on the world in which the evaluation is made and on the worlds it has passed through previously. The result is an extended semantics, which can specify a class of modal logics more comprehensive than the class specified by ordinary Kripke frames. This paper introduces a metamodel for reactive Kripke frames, based on the concept of categorical sketch. We believe that the categorical sketch is an appropriate metamodel for specifying a Kripke frame model. [ABSTRACT FROM AUTHOR]

Residuated basic logic (RBL) is the logic of residuated basic algebras, which constitutes a conservative extension of basic propositional logic (BPL). The basic implication is a residual of a non-associative binary operator in RBL. The conservativity is shown by relational semantics. A Gentzen-style sequent calculus GRBL , which is an extension of the distributive full non-associative Lambek calculus, is established for residuated basic logic. The calculus GRBL admits the mix-elimination, subformula, and disjunction properties. Moreover, the class of all residuated basic algebras has the finite embeddability property. The consequence relation of GRBL is decidable. [ABSTRACT FROM AUTHOR]

Scade is a domain-specific synchronous functional language used to implement safety-critical real-time software for more than twenty years. Two main approaches have been considered for its semantics: (i) an indirect collapsing semantics based on a source-to-source translation of high-level constructs into a data-flow core language whose semantics is precisely specified and is the entry for code generation; a relational synchronous semantics, akin to Esterel, that applies directly to the source. It defines what is a valid synchronous reaction but hides, on purpose, if a semantics exists, is unique and can be computed; hence, it is not executable. This paper presents, for the first time, an executable, state-based semantics for a language that has the key constructs of Scade all together, in particular the arbitrary combination of data-flow equations and hierarchical state machines. It can apply directly to the source language before static checks and compilation steps. It is constructive in the sense that the language in which the semantics is defined is a statically typed functional language with call-by-value and strong normalization, e.g., it is expressible in a proof-assistant where all functions terminate. It leads to a reference, purely functional, interpreter. This semantics is modular and can account for possible errors, allowing to establish what property is ensured by each static verification performed by the compiler. It also clarifies how causality is treated in Scade compared with Esterel. This semantics can serve as an oracle for compiler testing and validation; to prototype novel language constructs before they are implemented, to execute possibly unfinishedmodels or that are correct but rejected by the compiler; to prove the correctness of compilation steps. The semantics given in the paper is implemented as an interpreter in a purely functional style, in OCaml. [ABSTRACT FROM AUTHOR]

Safety-critical embedded software is routinely programmed in block-diagram languages. Recent work in the Vélus project specifies such a language and its compiler in the Coq proof assistant. It builds on the CompCert verified C compiler to give an end-to-end proof linking the dataflow semantics of source programs to traces of the generated assembly code. We extend this work with switched blocks, shared variables, reset blocks, and state machines; define a relational semantics to integrate these block- and mode-based constructions into the existing stream-based model; adapt the standard source-to-source rewriting scheme to compile the new constructions; and reestablish the correctness theorem. [ABSTRACT FROM AUTHOR]

The theory of stratified institutions is a general axiomatic approach to model theories where the satisfaction is parameterized by states of the models. In this paper we further develop this theory by introducing a new technique for representing stratified institutions, which is based on projecting to such simpler structures. On the one hand this can be used for developing general results applicable to a wide variety of already existing model theories with states, such as those based on some form of Kripke semantics. On the other hand this may serve as a template for defining new such model theories. In this paper we emphasize the former application of this technique by developing general results on model amalgamation and on the existence diagrams for stratified institutions. These are two most useful properties to have in institution theoretic model theory. [ABSTRACT FROM AUTHOR]

We consider relational semantics (R-models) for the Lambek calculus extended with intersection and explicit constants for zero and unit. For its variant without constants and a restriction which disallows empty antecedents, Andr'eka and Mikul'as (1994) prove strong completeness. We show that it fails without this restriction, but, on the other hand, prove weak completeness for non-standard interpretation of constants. For the standard interpretation, even weak completeness fails. The weak completeness result extends to an infinitary setting, for so-called iterative divisions (Kleene star under division). We also prove strong completeness results for product-free fragments. [ABSTRACT FROM AUTHOR]

Non-additive uncertainty theories, typically possibility theory, belief functions and imprecise probabilities share a common feature with modal logic: the duality properties between possibility and necessity measures, belief and plausibility functions as well as between upper and lower probabilities extend the duality between possibility and necessity modalities to the graded environment. It has been shown that the all-or-nothing version of possibility theory can be exactly captured by a minimal epistemic logic (MEL) that uses a very small fragment of the KD modal logic, without resorting to relational semantics. Independently, a belief function logic has been obtained by extending the modal logic S5 to probabilistic graded modalities using Łukasiewicz logic, albeit using relational semantics. This paper shows that a simpler belief function logic can be devised by adding Łukasiewicz logic on top of MEL. It allows for a more natural semantics in terms of Shafer basic probability assignments. [ABSTRACT FROM AUTHOR]

This paper proposes an intuitionistic generalization of van Benthem and Liu's dynamic logic of relation changers, where relation changers are dynamic operators that rewrite each agent's accessibility relation. We employ Nishimura's Kripke semantics for a constructive propositional dynamic logic to define the semantics of relation changers. Strong completeness results of Hilbert-style axiomatizations for constructive dynamic logic of relation changers are established by two types of rewriting strategies via recursion axioms: inside-out and outside-in strategies. To establish the semantic completeness by outside-in strategy, we propose the notion of composition of relation changers and an appropriately defined notion of length of a formula. Moreover, we reveal that recursion axioms have additional two faces: semantic and proof-theoretic ones. As for the semantic face, we introduce an alternative semantics for dynamic logic of relation changers to specify the semantic meaning of recursion axioms used in the inside-out strategy. This leads us to a semantic completeness proof of the axiomatization for the original semantics, which does not require a rewriting strategy based on recursion axioms. As for the proof-theoretic face, we transform each of recursion axioms required in the outside-in strategy into two (left and right) inference rules to provide a sequent calculus for dynamic logic of relation changers. Since the resulting sequent calculus is cut-free but semi-analytic, it still enjoys the Craig interpolation theorem by Maehara's method. [ABSTRACT FROM AUTHOR]

The idealizations resulting from the use of Kripke semantics in Epistemic Logic are inherited by formalizations of group epistemic notions. For example, distributed knowledge is often taken to reflect the potential knowledge of a group: what agents would know if they had unbounded means of communication and deductive ability. However, this does not specify whether/how this potential can be actualized, especially since real people are not unbounded reasoners. Inspired by experiments on group reasoning, we identify two dimensions of actualizing distributed knowledge: communication and inference. We build a dynamic framework with effortful actions accounting for both, combining impossible-worlds semantics and action models , and we provide a method for extracting a sound and complete axiomatization. [ABSTRACT FROM AUTHOR]

Falsification-aware (hyper)sequent calculi and Kripke semantics for normal modal logics including S4 and S5 are introduced and investigated in this study. These calculi and semantics are constructed based on the idea of a falsification-aware framework for Nelson's constructive three-valued logic. The cut-elimination and completeness theorems for the proposed calculi and semantics are proved. [ABSTRACT FROM AUTHOR]

In this article, we introduce and investigate an extension of Halpern and Shoham’s interval temporal logic HS for the specification and verification of branching-time context-free requirements of pushdown systems under a state-based semantics over Kripke structures enforcing visibility of the pushdown operations. The proposed logic, called nested BHS, supports branching-time both in the past and in the future and is able to express non-regular properties of linear and branching behaviours of procedural contexts in a natural way. It strictly subsumes well-known linear time context-free extensions of LTL such as CaRet [4] and NWTL [2]. The main result is the decidability of the visibly pushdown model-checking problem against nested BHS. The proof exploits a non-trivial automata-theoretic construction. [ABSTRACT FROM AUTHOR]

Although various dynamic or temporal logics have been proposed to verify quantum protocols and systems, these two viewpoints have not been studied comprehensively enough. We propose Linear Temporal Quantum Logic (LTQL), a linear temporal extension of quantum logic with a quantum implication, and extend it to Dynamic Linear Temporal Quantum Logic (DLTQL). This logic has temporal operators to express transitions by unitary operators (quantum gates) and dynamic ones to express those by projections (projective measurement). We then prove some logical properties of the relationship between these two transitions expressed by LTQL and DLTQL. A drawback in applying LTQL to the verification of quantum protocols is that these logics cannot express the future operator in linear temporal logic. We propose a way to mitigate this drawback by using a translation from (D)LTQL to Linear Temporal Modal Logic (LTML) and a simulation. This translation reduces the satisfiability problem of (D)LTQL formulas to that of LTML with the classical semantics over quantum states. [ABSTRACT FROM AUTHOR]

We take Carnap's problem to be to what extent standard consequence relations in various formal languages fix the meaning of their logical vocabulary, alone or together with additional constraints on the form of the semantics. This paper studies Carnap's problem for basic modal logic. Setting the stage, we show that neighborhood semantics is the most general form of compositional possible worlds semantics, and proceed to ask which standard modal logics (if any) constrain the box operator to be interpreted as in relational Kripke semantics. Except when restricted to finite domains, no modal logic characterizes exactly the Kripkean interpretations of $\Box $. Moreover, we show that, in contrast with the case of first-order logic, the obvious requirement of permutation invariance is not adequate in the modal case. After pointing out some known facts about modal logics that nevertheless force the Kripkean interpretation, we focus on another feature often taken to embody the gist of modal logic: locality. We show that invariance under point-generated subframes (properly defined) does single out the Kripkean interpretations, but only among topological interpretations, not in general. Finally, we define a notion of bisimulation invariance—another aspect of locality—that, together with a reasonable closure condition, gives the desired general result. Along the way, we propose a new perspective on normal neighborhood frames as filter frames, consisting of a set of worlds equipped with an accessibility relation, and a free filter at every world. [ABSTRACT FROM AUTHOR]

Two algebraic structures, the contrapositionally complemented Heyting algebra (ccHa) and the contrapositionally |$\vee $| complemented Heyting algebra (c |$\vee $| cHa), are studied. The salient feature of these algebras is that there are two negations, one intuitionistic and another minimal in nature, along with a condition connecting the two operators. Properties of these algebras are discussed, examples are given and comparisons are made with relevant algebras. Intuitionistic Logic with Minimal Negation (ILM) corresponding to ccHa s and its extension |${\textrm {ILM}}$| - |${\vee }$| for c |$\vee $| cHa s are then investigated. Besides its relations with intuitionistic and minimal logics, ILM is observed to be related to Peirce's logic and Vakarelov's logic MIN. With a focus on properties of the two negations, relational semantics for ILM and |${\textrm {ILM}}$| - |${\vee }$| are obtained with respect to four classes of frames, and inter-translations between the classes preserving truth and validity are provided. ILM and |${\textrm {ILM}}$| - |${\vee }$| are shown to have the finite model property with respect to these classes of frames and proved to be decidable. Extracting features of the two negations in the algebras, a further investigation is made, following logical studies of negations that define the operators independently of the binary operator of implication. Using Dunn's logical framework for the purpose, two logics |$K_{im}$| and |$K_{im-{\vee }}$| are discussed, where the language does not include implication. The |$K_{im}$| -algebras are reducts of ccHa s and are different from relevant algebraic structures having two negations. The negations in the |$K_{im}$| -algebras and |$K_{im-{\vee }}$| -algebras are shown to occupy distinct positions in an enhanced form of Dunn's kite of negations. Relational semantics for |$K_{im}$| and |$K_{im-{\vee }}$| is provided by a class of frames that are based on Dunn's compatibility frames. It is observed that this class coincides with one of the four classes giving the relational semantics for ILM and |${\textrm {ILM}}$| - |${\vee }$|⁠. [ABSTRACT FROM AUTHOR]

This paper shows that the Hilbert system H(C + J)-, given by del Cerro and Herzig (1996), is semantically incomplete. This system is proposed as a proof theory for a combination of classical and intuitionistic propositional logic, which is called C + J. The Kripke semantics for this combination is obtained by adding the semantic clause of classical implication directly to the Kripke semantics for intuitionistic propositional logic. The Hilbert system H(C + J)- does not contain the classical modus ponens, although it contains the intuitionistic modus ponens as a rule, which makes this system semantically incomplete. This paper gives an argument that the system H(C + J)- is semantically incomplete because of the absence of the classical modus ponens. Our way to prove this is based on the logic of paradox, which is a paraconsistent logic proposed by Priest (1979). [ABSTRACT FROM AUTHOR]

The concept of modernizing outdated systems in critical infrastructure through digital transformation has been a widely discussed topic nowadays. Following the transition of energy systems, the attention has now shifted towards digitalizing the water distribution systems. These systems are large-scale but outdated systems that frequently encounter various issues and upgrading them would enable easier to identify issues and provide smoother, more efficient service. However, this process requires cautious planning and guidance to ensure that the generated data is reliable, and the system remains operational during the transition. Hence, the primary objective of this paper is to propose a formal model based on ternary relational semantics that can guide the digital transformation of water distribution networks. The proposed model provides a flexible transformation process while making the system generate reliable data. Additionally, this paper demonstrates the application of the proposed model by developing a proof of concept based on a real-world scenario. [ABSTRACT FROM AUTHOR]

This article aims at providing some extension of the modal square of opposition in the light of Ockham's account of modal operators. Moreover, we set forth some significant remarks on the de re–de dicto distinction and on the modal operator of contingency by means of a set-theoretic algebra called numbering semantics. This generalization starting from Ockham's account of modalities will allow us to take into consideration whether Ockham's account holds water or not, and in which case it should be changed. [ABSTRACT FROM AUTHOR]

The definition of institution formalizes the intuitive notion of logic in a category-based setting. Similarly, the concept of stratified institution provides an abstract approach to Kripke semantics. This includes hybrid logics, a type of modal logics expressive enough to allow references to the nodes/states/worlds of the models regarded as relational structures, or multi-graphs. Applications of hybrid logics involve many areas of research, such as computational linguistics, transition systems, knowledge representation, artificial intelligence, biomedical informatics, semantic networks, and ontologies. The present contribution sets a unified foundation for developing formal verification methodologies to reason about Kripke structures by defining proof calculi for a multitude of hybrid logics in the framework of stratified institutions. To prove completeness, the article introduces a forcing technique for stratified institutions with nominal and frame extraction and studies a forcing property based on syntactic consistency. The proof calculus is shown to be complete and the significance of the general results is exhibited on a couple of benchmark examples of hybrid logical systems. [ABSTRACT FROM AUTHOR]

This special issue contains extended versions of selected papers presented at the 3rd International Workshop on Dynamic Logic: New Trends and Applications (DaLí 2020). The submissions to DaLí 2020 and to the special issue span across various areas including dynamic logic and dynamic algebra, dynamic logic and public announcement logic and epistemic and modal logic in general. Strong completeness results concerning Hilbert-style axiomatizations of constructive dynamic logic of relation changers are established using two types of rewriting strategies via recursion axioms: inside-out and outside-in strategies. [Extracted from the article]

We show that monadic intuitionistic quantifiers admit the following temporal interpretation: "always in the future" (for $\forall $) and "sometime in the past" (for $\exists $). It is well known that Prior's intuitionistic modal logic ${\sf MIPC}$ axiomatizes the monadic fragment of the intuitionistic predicate logic, and that ${\sf MIPC}$ is translated fully and faithfully into the monadic fragment ${\sf MS4}$ of the predicate ${\sf S4}$ via the Gödel translation. To realize the temporal interpretation mentioned above, we introduce a new tense extension ${\sf TS4}$ of ${\sf S4}$ and provide a full and faithful translation of ${\sf MIPC}$ into ${\sf TS4}$. We compare this new translation of ${\sf MIPC}$ with the Gödel translation by showing that both ${\sf TS4}$ and ${\sf MS4}$ can be translated fully and faithfully into a tense extension of ${\sf MS4}$ , which we denote by ${\sf MS4.t}$. This is done by utilizing the relational semantics for these logics. As a result, we arrive at the diagram of full and faithful translations shown in Figure 1 which is commutative up to logical equivalence. We prove the finite model property (fmp) for ${\sf MS4.t}$ using algebraic semantics, and show that the fmp for the other logics involved can be derived as a consequence of the fullness and faithfulness of the translations considered. [ABSTRACT FROM AUTHOR]

Here, I combine the semantics of Mares and Goldblatt [20] and Seki [29, 30] to develop a semantics for quantified modal relevant logics extending ${\bf B}$. The combination requires demonstrating that the Mares–Goldblatt approach is apt for quantified extensions of ${\bf B}$ and other relevant logics, but no significant bridging principles are needed. The result is a single semantic approach for quantified modal relevant logics. Within this framework, I discuss the requirements a quantified modal relevant logic must satisfy to be "sufficiently classical" in its modal fragment, where frame conditions are given that work for positive fragments of logics. The roles of the Barcan formula and its converse are also investigated. [ABSTRACT FROM AUTHOR]

This article compares classical (or KF-like) and nonclassical (or PKF-like) axiomatisations of the fixed-point semantics developed by Kripke (J Philos 72(19): 690–716, 1975). Following the line of investigation of Halbach and Nicolai (J Philos Logic 47(2): 227–257, 2018), we do not compare KF and PKF qua theories of truth simpliciter, but rather qua axiomatisations of the Kripkean conception of truth. We strengthen the central results of Halbach and Nicolai (2018) and Nicolai (Stud Log 106(1): 101–130, 2018), showing that, on the one hand, there is a stronger sense in which some variants of KF and some variants of PKF can be taken to be, truth-theoretically, equivalent. On the other hand, we show that this truth-theoretical equivalence is not preserved by some other variants of KF and PKF, arguing that the PKF variants are more adequate axiomatisations of the fixed-point semantics than the corresponding KF variants. [ABSTRACT FROM AUTHOR]

We study a version of public announcement logic with common knowledge based on the relevant logic |$\textsf {R}$|⁠. Public announcements, as represented in our framework, are not necessarily truthful and accepted by all agents, nor is it assumed that beliefs are preserved under announcements. We establish a completeness result with respect to a relational semantics, and we show that an alternative semantics based on information states is dual to the relational one. We add a question-forming inquisitive disjunction operator to the language and prove a completeness result with respect to the information semantics. [ABSTRACT FROM AUTHOR]

Due to the increasing use of information technologies by biomedical experts, researchers, public health agencies, and healthcare professionals, a large number of scientific literatures, clinical notes, and other structured and unstructured text resources are rapidly increasing and being stored in various data sources like PubMed. These massive text resources can be leveraged to extract valuable knowledge and insights using machine learning techniques. Recent advancement in neural network-based classification models has gained popularity which takes numeric vectors (aka word representation) of training data as the input to train classification models. Better the input vectors, more accurate would be the classification. Word representations are learned as the distribution of words in an embedding space, wherein each word has its vector and the semantically similar words based on the contexts appear nearby each other. However, such distributional word representations are incapable of encapsulating relational semantics between distant words. In the biomedical domain, relation mining is a well-studied problem which aims to extract relational words, which associates distant entities generally representing the subject and object of a sentence. Our goal is to capture the relational semantics information between distant words from a large corpus to learn enhanced word representation and employ the learned word representation for various natural language processing tasks such as text classification. In this article, we have proposed an application of biomedical relation triplets to learn word representation through incorporating relational semantic information within the distributional representation of words. In other words, the proposed approach aims to capture both distributional and relational contexts of the words to learn their numeric vectors from text corpus. We have also proposed an application of the learned word representations for text classification. The proposed approach is evaluated over multiple benchmark datasets, and the efficacy of the learned word representations is tested in terms of word similarity and concept categorization tasks. Our proposed approach provides better performance in comparison to the state-of-the-art GloVe model. Furthermore, we have applied the learned word representations to classify biomedical texts using four neural network-based classification models, and the classification accuracy further confirms the effectiveness of the learned word representations by our proposed approach. [ABSTRACT FROM AUTHOR]

In this article, I consider the positive logic of Boolean groups (i.e. Abelian groups where every non-identity element has order 2), where these are taken as frames for an operational semantics à la Urquhart. I call this logic BG. It is shown that the logic over the smallest nontrivial Boolean group, taken as a frame, is identical to the positive fragment of a quasi-relevance logic that was developed by Robles and Méndez (an extension of this result where negation is included is also discussed). It is proved that BG satisfies the variable sharing property and is Halldén complete, while failing to satisfy the disjunction property. Sound and complete subscripted tableaux are presented for BG. An axiomatization (in the positive language extended with fusion) is presented, which is sound with respect to BG and, with respect to a related ternary relational semantics, complete; the problem of identifying a complete axiomatization for BG itself is left open. Connections between BG and the quasi-relevance logic KR are also discussed. [ABSTRACT FROM AUTHOR]

Let a priority micro pluralist be someone who holds that particles or other microscopic objects are fundamental. Rivals to priority micro pluralism include priority monism (the view that the only fundamental concrete object is the entire cosmos) as well as the Aristotelian view that some ordinary macroscopic objects are fundamental. Although priority micro pluralism is popular, I show that it encounters great difficulty in even the most straightforward cases. For example, this tennis ball is spherical; how is this fact to be grounded in facts about the microscopic realm? I consider a number of possible answers to this question. The most promising proposals attempt to exploit the close connection emphasized by Kripke between objects and their original material constituents. I argue that these proposals fail. I conclude that it is worth seriously considering alternatives to this sort of pluralism. [ABSTRACT FROM AUTHOR]

The joint logic of problems and propositions QHC introduced by S. A. Melikhov, as well as intuitionistic modal logic QH4, is studied. An immersion of these logics into classical first-order predicate logic is considered. An analog of the Löwenheim–Skolem theorem on the existence of countable elementary submodels for QHC and QH4 is established. [ABSTRACT FROM AUTHOR]

This paper proposes new semantics for propositional dynamic logic (PDL), replacing the standard relational semantics. Under these new semantics, program execution is represented as fundamentally deterministic (i.e., functional), while nondeterminism emerges as an epistemic relationship between the agent and the system: intuitively, the nondeterministic outcomes of a given process are precisely those that cannot be ruled out in advance. We formalize these notions using topology and the framework of dynamic topological logic (DTL) (Kremer and Mints in Ann Pure Appl Logic 131:133–158, 2005). We show that DTL can be used to interpret the language of PDL in a manner that captures the intuition above, and moreover that continuous functions in this setting correspond exactly to deterministic processes. We also prove that certain axiomatizations of PDL remain sound and complete with respect to the corresponding classes of dynamic topological models. Finally, we extend the framework to incorporate knowledge using the machinery of subset space logic (Dabrowski et al. in Ann Pure Appl Logic 78:73–110, 1996), and show that the topological interpretation of public announcements as given in Bjorndahl (in: van Ditmarsch and Sandu (eds) Jaakko Hintikka on knowledge and game theoretical semantics, outstanding contributions to Logic, vol 12, Springer, 2018) coincides exactly with a natural interpretation of test programs. [ABSTRACT FROM AUTHOR]

In this paper, we introduce provability multilattice logic P M L n and multilattice arithmetic M P A n which extends first-order multilattice logic with equality by multilattice versions of Peano axioms. We show that P M L n has the provability interpretation with respect to M P A n and prove the arithmetic completeness theorem for it. We formulate P M L n in the form of a nested sequent calculus and show that cut is admissible in it. We introduce the notion of a provability multilattice and develop algebraic semantics for P M L n on its basis, by the method of Lindenbaum-Tarski algebras we prove the algebraic completeness theorem. We present Kripke semantics for P M L n and establish the Kripke completeness theorem via syntactical and semantic embeddings from P M L n into G L and vice versa. Last but not least, the decidability of P M L n is shown. [ABSTRACT FROM AUTHOR]

We explore two ways of formalizing Kreisel's addendum to the Brouwer–Heyting–Kolmogorov interpretation. To do this, we compare Artemov's justification logic with simply typed |$\lambda $| calculus. First, we provide a completeness result for Kripke style semantics of the implicational fragment of the intuitionistic logic of proofs. Then we introduce a map from justification terms into |$\lambda $| terms, which can be viewed as a method of extracting the computational content of the justification terms. Then we examine the interpretation of Kreisel's addendum in justification logic along with the image of the resulting justification terms under our map. [ABSTRACT FROM AUTHOR]

The paraconsistent and paracomplete 4-valued logic PŁ4 is originally interpreted with a two-valued Belnap-Dunn semantics. In the present paper, PŁ4 is endowed with both a ternary Routley-Meyer semantics and a binary Routley semantics together with their respective restriction to the 2 set-up case. [ABSTRACT FROM AUTHOR]

SQL is the world's most popular declarative language, forming the basis of the multi-billion-dollar database industry. Although SQL has been standardized, the full standard is based on ambiguous natural language rather than formal specification. Commercial SQL implementations interpret the standard in different ways, so that, given the same input data, the same query can yield different results depending on the SQL system it is run on. Even for a particular system, mechanically checked formalization of all widely-used features of SQL remains an open problem. The lack of a well-understood formal semantics makes it very difficult to validate the soundness of database implementations. Although formal semantics for fragments of SQL were designed in the past, they usually did not support set and bag operations, lateral joins, nested subqueries, and, crucially, null values. Null values complicate SQL's semantics in profound ways analogous to null pointers or side-effects in other programming languages. Since certain SQL queries are equivalent in the absence of null values, but produce different results when applied to tables containing incomplete data, semantics which ignore null values are able to prove query equivalences that are unsound in realistic databases. A formal semantics of SQL supporting all the aforementioned features was only proposed recently. In this paper, we report about our mechanization of SQL semantics covering set/bag operations, lateral joins, nested subqueries, and nulls, written in the Coq proof assistant, and describe the validation of key metatheoretic properties. Additionally, we are able to use the same framework to formalize the semantics of a flat relational calculus (with null values), and show a certified translation of its normal forms into SQL. [ABSTRACT FROM AUTHOR]

Relation classification is an important fundamental task in information extraction, and convolutional neural networks have been commonly applied to relation classification with good results. In recent years, due to the proposed pre-training model BERT, the use of which as a feature extraction architecture has become more and more popular, convolutional neural networks have gradually withdrawn from the stage of NLP, and the relation classification/extraction model based on pre-training BERT has achieved state-of-the-art results. However, none of these methods consider how to accurately capture the semantic features of the relationships between entities to reduce the number of noisy words in a sentence that are not helpful for relation classification. Moreover, these methods do not have a systematic prediction structure to fully utilize the extracted features for the relational classification task. To address these problems, a SpanBert-based relation classification model is proposed in this paper. Compared with existing Bert-based architectures, the model is able to understand the semantic information of the relationships between entities more accurately, and it can fully utilize the extracted features to represent the degree of dependency of a pair of entities with each type of relationship. In this paper, we design a feature fusion method called "SRS" (Strengthen Relational Semantics) and an attention-based prediction structure. Compared with existing methods, the feature fusion method proposed in this paper can reduce the noise interference of irrelevant words when extracting relational semantics, and the prediction structure proposed in this paper can make full use of semantic features for relational classification. We achieved advanced results on the SemEval-2010 Task 8 and the KBP37 relational dataset. [ABSTRACT FROM AUTHOR]

I show that the logic $\textsf {TJK}^{d+}$ , one of the strongest logics currently known to support the naive theory of truth, is obtained from the Kripke semantics for constant domain intuitionistic logic by (i) dropping the requirement that the accessibility relation is reflexive and (ii) only allowing reflexive worlds to serve as counterexamples to logical consequence. In addition, I provide a simplified natural deduction system for $\textsf {TJK}^{d+}$ , in which a restricted form of conditional proof is used to establish conditionals. [ABSTRACT FROM AUTHOR]

Information transmission in social networks is riddled with issues of reliability and trustworthiness. One of the main sources of disinformation can be traced back to agents—human or artificial—whose political or cultural agenda is guided by conspiracy theories. Modelling and understanding the behaviour of such agents within social networks is therefore crucial to approach the disinformation problem. In the present paper, we formulate the logic (un)SecureNDsim* , equipped with a proof-theory and a relational semantics in which negative trust relations are defined formalizing the attitude of paranoid agents, i.e. agents distrusting any information originating from the authority and thereby spreading what can be characterized as the content of conspiracy theories. The logic is implemented in a multi-agent simulation aimed at analysing the effects of conspiracy theorists in networks of agents. In particular, we analyse consensus reaching scenarios and the ability of paranoid agents to induce the spread of potentially false information. [ABSTRACT FROM AUTHOR]

The notion of a critical successor [5] in relational semantics has been central to most classic modal completeness proofs in interpretability logics. In this paper we shall work with a more general notion, that of an assuring successor. This will enable more concisely formulated completeness proofs, both with respect to ordinary and generalised Veltman semantics. Due to their interesting theoretical properties, we will devote some space to the study of a particular kind of assuring labels, the so‐called full labels and maximal labels. After a general treatment of assuringness, we shall apply it to obtain a completeness result for the modal logic ILP$\mathsf {ILP}$ w.r.t. generalised semantics for a restricted class of frames. [ABSTRACT FROM AUTHOR]