Search

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]

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]

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]

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]

Implicational partial Galois logics and some of their semilinear extensions, such as semilinear extensions satisfying abstract Galois and dual Galois connection properties, have been introduced together with their relational semantics. However, similar extensions satisfying residuated, dual residuated connection properties have not. This paper fills the gaps by introducing those semilinear extensions and their relational semantics. To this end, the class of implicational (dual) residuated-connected prelinear gaggle logics is defined and it is verified that these logics are semilinear. In particular, associated with the contribution of this work, we note the following two: One is that implications can be introduced by residuated connection in semilinear logics. This shows that the residuated, dual residuated connection properties are important and so need to be investigated in semilinear logics. The other is that set-theoretic relational semantics can be provided for semilinear logics. Semilinear logics have been dealt with extensively in algebraic context, whereas they have not yet been performed in the set-theoretic one. [ABSTRACT FROM AUTHOR]

The aim of Medical Knowledge Graph Completion is to automatically predict one of three parts (head entity, relationship, and tail entity) in RDF triples from medical data, mainly text data. Following their introduction, the use of pretrained language models, such as Word2vec, BERT, and XLNET, to complete Medical Knowledge Graphs has become a popular research topic. The existing work focuses mainly on relationship completion and has rarely solved entities and related triples. In this paper, a framework to predict RDF triples for Medical Knowledge Graphs based on word embeddings (named PTMKG-WE) is proposed, for the specific use for the completion of entities and triples. The framework first formalizes existing samples for a given relationship from the Medical Knowledge Graph as prior knowledge. Second, it trains word embeddings from big medical data according to prior knowledge through Word2vec. Third, it can acquire candidate triples from word embeddings based on analogies from existing samples. In this framework, the paper proposes two strategies to improve the relation features. One is used to refine the relational semantics by clustering existing triple samples. Another is used to accurately embed the expression of the relationship through means of existing samples. These two strategies can be used separately (called PTMKG-WE-C and PTMKG-WE-M, respectively), and can also be superimposed (called PTMKG-WE-C-M) in the framework. Finally, in the current study, PubMed data and the National Drug File-Reference Terminology (NDF-RT) were collected, and a series of experiments was conducted. The experimental results show that the framework proposed in this paper and the two improvement strategies can be used to predict new triples for Medical Knowledge Graphs, when medical data are sufficiently abundant and the Knowledge Graph has appropriate prior knowledge. The two strategies designed to improve the relation features have a significant effect on the lifting precision, and the superposition effect becomes more obvious. Another conclusion is that, under the same parameter setting, the semantic precision of word embedding can be improved by extending the breadth and depth of data, and the precision of the prediction framework in this paper can be further improved in most cases. Thus, collecting and training big medical data is a viable method to learn more useful knowledge. [ABSTRACT FROM AUTHOR]

Six interesting variants of the logics BN4 and E4--which can be considered as the 4-valued logics of the relevant conditional and (relevant) entailment, respectively--were previously developed in the literature. All these systems are related to the family of relevant logics and contain Routley and Meyer's basic logic B, which is well-known to be specifically associated with the ternary relational semantics. The aim of this paper is to develop reduced general Routley-Meyer semantics for them. Strong soundness and completeness theorems are proved for each one of the logics. [ABSTRACT FROM AUTHOR]

Dependency trees reflect rich structural information, which can effectively guide models to understand text semantics and are widely used for relation extraction. However, existing dependency-based models suffer from noise in dependency trees, which distorts the modeling of contextual information, particularly when introducing dependency types, further exacerbating the propagation and accumulation of errors. In addition, rule-based pruning strategies used to eliminate noise in dependency trees may lose crucial information for capturing relational patterns, whereas unconstrained learning-based pruning strategies may introduce more noisy edges. These two aspects of dependency trees may cause models to produce semantic confusion, which is detrimental to relation extraction. In this study, we propose a Contextual Dependency-Aware Graph Convolutional Network (C-DAGCN) that works on complete dependency trees and perceives the importance of word dependencies from multiple angles without considering the noise in dependency trees. This study includes three parts. First, the sequence model captures semantic information for the input sentence and its words. We considered the appropriate outputs as word and sentence-level representations based on model characteristics. Second, the structure model enhances the description of the sentence structure and its guidance. We consider that position knowledge implies associations between words; therefore, we propose the Current Word Global Relative Position Knowledge (CW-GRPK) to globally enhance text structure modeling and reduce the models' overreliance on single noisy structure guidance. A dependency-aware module weighs heuristic syntactic knowledge and non-heuristic CW-GRPK to capture fine-grained word-level interactions that effectively distinguish words related to relational semantics. Subsequently, a dependency-guided module, based on the results of the dependency-aware layer, encodes a knowledge-enhanced word graph without losing global linguistic patterns. Third, we constructed high-level linguistic representations based on the results of the sequence and structure model in C-DAGCN as a relational representation and mapped it to the relational decision space for relational prediction. The experimental results demonstrate that our method outperforms nine strong baseline models on two benchmark datasets. Compared with the best baseline Attentive Graph Convolutional Networks (A-GCN) model (Tian et al., 2021), our proposed C-DAGCN model with 90.15 macro-average F1 and 79.52 micro-average F1 achieves 0.28 macro-average F1 and 0.47 micro-average F1 improvement on the SemEval2010-Task8 and ACE2005 datasets, respectively. 1 1 Our code is available at https://github.com/dymyyc/RE%5fC-DAGCN. The released code when run produces results which are the same as those reported in this paper. • A kind of position knowledge globally enhances text structure modeling. • A dependency-aware module captures fine-grained word-level interactions. • Our model constructs a high-level linguistic representation for relation extraction. • Our model outperforms nine strong baselines on the two benchmark datasets. [ABSTRACT FROM AUTHOR]

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

We investigate the relationship between M. De's empirical negation in Kripke and Beth Semantics. It turns out empirical negation, as well as co-negation, corresponds to different logics under different semantics. We then establish the relationship between logics related to these negations under unified syntax and semantics based on R. Sylvan's CCw. [ABSTRACT FROM AUTHOR]

We define Kripke semantics for propositional intuitionistic logic with Suszko's identity (ISCI). We propose sequent calculus for ISCI along with cut-elimination theorem. We sketch a constructive interpretation of Suszko's propositional iden- tity connective. [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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

The Craig interpolation property and interpolation property for deducibility are considered for special kind of normal extensions of the Brouwer logic. [ABSTRACT FROM AUTHOR]

In this work, we combine features from Justification Logics and Logics of Plausibility-Based Beliefs to build a logic for Multi-Agent Systems where each agent can explicitly state his justification for believing in a given sentence. Our logic is a normal modal logic based on the standard Kripke semantics, where we provide a semantic definition for the evidence terms and define the notion of plausible evidence for an agent, based on plausibility relations in the model. As we deal with beliefs, justifications can be faulty and unreliable. In our logic, agents can disagree not only over whether a sentence is true or false, but also on whether some evidence is a valid justification for a sentence or not. After defining our logic and its semantics, we provide a strongly complete axiomatic system for it, show that it has the finite model property, analyze the complexity of its Model-Checking Problem and show that its Satisfiability Problem has the same complexity as the one from basic modal logics. Thus, this logic seems to be a good first step for the development of a dynamic logic that can model the processes of argumentation and debate in Multi-Agent Systems. [ABSTRACT FROM AUTHOR]

By means of a countermodel we show that the homotopy equivalence of the fibers of a Kan fibration over a connected base cannot be proved constructively. [ABSTRACT FROM AUTHOR]

In this paper we show that the satisfaction of timed CTL (TCTL) formulas under the natural continuous semantics for both discrete-time and dense-time timed Kripke structures can be reduced to a model-checking problem in the pointwise semantics for a large class of timed Kripke structures, which includes many discrete-event systems. We then present a TCTL model checking algorithm for the pointwise case. An important consequence of our results is that they together describe a sound and complete TCTL model checking procedure for time-robust real-time rewrite theories also for dense time domains. We have implemented such a TCTL model checker for Real-Time Maude. Our model checker provides for free a sound and complete TCTL model checker for subsets of modeling languages, such as Ptolemy II and (Synchronous) AADL, which have Real-Time Maude analysis integrated into their tool environments. [ABSTRACT FROM AUTHOR]

Recently, algebraic Routley–Meyer-style semantics was introduced for basic substructural logics. This paper extends it to fuzzy logics. First, we recall the basic substructural core fuzzy logic MIAL (Mianorm logic) and its axiomatic extensions, together with their algebraic semantics. Next, we introduce two kinds of ternary relational semantics, called here linear Urquhart-style and Fine-style Routley–Meyer semantics, for them as algebraic Routley–Meyer-style semantics. [ABSTRACT FROM AUTHOR]

Aristotelian diagrams, such as the square of opposition, are well-known in the context of normal modal logics (i.e., systems of modal logic which can be given a relational semantics in terms of Kripke models). This paper studies Aristotelian diagrams for non-normal systems of modal logic (based on neighborhood semantics, a topologically inspired generalization of relational semantics). In particular, we investigate the phenomenon of logic-sensitivity of Aristotelian diagrams. We distinguish between four different types of logic-sensitivity, viz. with respect to (i) Aristotelian families, (ii) logical equivalence of formulas, (iii) contingency of formulas, and (iv) Boolean subfamilies of a given Aristotelian family. We provide concrete examples of Aristotelian diagrams that illustrate these four types of logic-sensitivity in the realm of normal modal logic. Next, we discuss more subtle examples of Aristotelian diagrams, which are not sensitive with respect to normal modal logics, but which nevertheless turn out to be highly logic-sensitive once we turn to non-normal systems of modal logic. [ABSTRACT FROM AUTHOR]

We present a categorical formalization of a variant of first-order logic. Unlike other texts on this topic, the goal of this paper is to give a very transparent and self-contained account without requiring more background than basic logic and set theory. Our focus is to show how the semantics of first-order formulas can be derived from their usual deduction rules. For understanding the core ideas, it is not necessary to investigate the internal term structure of atomic formulas, thus we abstract atomic formulas to (syntactically opaque) relations; in this sense, our variant of first-order logic is "relational". While the derived semantics is based on categorical principles (even the duality that arises from a symmetry between two ways of looking at something where there is no reason to choose one over the other), it is nevertheless "constructive" in that it describes explicit computations of the truth values of formulas. We demonstrate this by modeling the categorical semantics in the RISCAL (RISC Algorithm Language) system which allows us to validate the core propositions by automatically checking them in finite models. [ABSTRACT FROM AUTHOR]

We propose methods to enable the relational model to meet scalability and functionality needs of a large-scale social networking services (SNS) system. NewSQL has emerged recently indicating that shared-nothing parallel relational DBMSs can be used to guarantee the ACID properties of transactions while keeping the high scalability of NoSQL. Leading commercial SNS systems, however, rely on a graph – not relational – data model with key–value storage and, for certain operations, suffer overhead of unnecessarily accessing multiple system nodes. Exploiting higher semantics with the relational data model could be the remedy. The solution we offer aims to perform a transaction as a set of independent local transactions whenever possible based on the conceptual semantics of the SNS database schema. First, it hierarchically clusters entities that are sitting on a path of frequently navigated one-to-many relationships, thereby avoiding inter-node joins. Second, when a multi-node delete transaction is performed over many-to-many relationships, it defers deletion of related references until they are accessed later, thereby amortizing the cost of multi-node updates. These solutions have been implemented in Odysseus/SNS — an SNS system using a shared nothing parallel DBMS. Performance evaluation using synthetic workload that reflects the real SNS workload demonstrates significant improvement in processing time. We also note that our work is the first to present the entity-relationship schema and its relational representation of the SNS database. [ABSTRACT FROM AUTHOR]