Ontologies often involve complex logical structures, so changes to individual classes or the addition of new axioms can have significant implications for other parts of the ontology. Due to this complexity, dependencies between symbols in the vocabulary of the ontology are not always immediately apparent. In this paper, we define three semantics-based approaches for establishing dependency relationships between these symbols and explore their specific properties. Additionally, we apply these dependency relations in a case study.

Complex systems are full of unpredictable and uncertain behaviours that depend on many factors. Various fields of science have set themselves the task of studying these systems and predicting their behaviour under various premises with the help of computer models. Kwakkel et al. [1] published an uncertainty matrix to systematically record and communicate uncertainties about systems. This paper takes up the matrix, analyses the concepts of model and uncertainty in literature, and models them ontologically in the Modelling Uncertainties Ontology (MUNO), a BFO-based mid-level ontology for modelling uncertainties in models for many domains. MUNO is evaluated against requirements and competency questions. Based on the ontology, an RDF-shape is created and used as an example in a case study to annotate the uncertainties for an energy system model.

ULLER (Unified Language for LEarning and Reasoning) provides a single first-order logic (FOL) syntax, enabling its knowledge bases to be used directly across a wide range of neurosymbolic systems. The original specification endows this syntax with three pairwise independent semantics—classical, fuzzy, and probabilistic—each accompanied by dedicated semantic rules. We show that these seemingly disparate semantics are all instances of one categorical framework based on monads, the very construct that models side effects in func- tional programming. This enables the modular addition of new semantics and systematic translations between them. As example, we outline the addition of generalized quantifi- cation in Logic Tensor Networks (LTN) to arbitrary (also infinite) domains by extending the Giry monad to probability spaces. In particular, our approach allows a modular imple- mentation of ULLER in Python and Haskell, of which we have published initial versions on GitHub.

UML allows the multi-viewpoint modelling of systems. One important question is whether an interaction as specified by a sequence diagram can be actually realised in the system. Here, the latter is specified as a combination of several state machines (one for each lifeline in the interaction) by a composite structure diagram. In order to tackle this question, we formalise the involved UML diagram types as institutions, and their relations as institution (co)morphisms.

Solid decision making should be ideally based on clear arguments that can be justified by trustworthy information sources. However, argument spaces can quickly get quite complex and it is very often hard to trace the line of arguments found in literature or social media such as blogs and forums. In this paper, we propose a framework for a decision supporting interactive information retrieval system using methods for argument exploration based on textual documents. This concept is supported by a prototype that focuses on the actual analysis of the retrieved arguments in order to obtain a justified decision. For that we use a simplified argumentation graph with nodes as arguments and simple attacking and supporting relations. A web-based plausibility value is propagated (using ranked-based argumentation semantics) through the network for estimating the quality of the arguments. This is based on a web search for documents that support these arguments. The final decision can further be supported by chosing certain preferred interpretations of an abstract dialectical framework, leading to an integrated view of searching, creating, analysing and deciding.

A qualitative representation of space and/or time provides mechanisms which characterize the essential properties of objects or configurations. The advantages over quantitative representations can be: (1) a better match with human concepts related to natural language, and (2) better efficiency for reasoning. The two main trends in qualitative spatial constraint reasoning are topological reasoning about regions and reasoning about directions between points and straight lines and orientations of straight lines or configurations derived from points. In this work, we apply universal algebraic tools to binary qualitative calculi and their relations.

OWL API is a high level API for working with ontologies. Despite of its functionalities and numerous advantages, it is restricted to a set of users due to its platform dependency. Being built as a java API the OWL API can only be used by java or related platform users. The major goal of this paper is to design a RESTful web interface of OWL API methods, such that ontology developers and researchers independent of platform could work with OWL API. This RESTful OWL API tool is designed to exhibit all the functionalities of OWL API that do not deal with rendering the input ontology such that it doesn't behave as an ontology editor, instead supports web ontology developers and open ontology repositories such as Ontohub.

Qualitative spatial descriptions characterize essential properties of spatial objects or configurations by relying on relative comparisons rather than measuring. Typically, in qualitative approaches only relatively coarse distinctions between configurations are made. Qualitative spatial knowledge can be used to represent incomplete and underdetermined knowledge in a systematic way. This is especially useful if the task is to describe features of classes of configurations rather than individual configurations. Although reasoning with them is generally NP-hard, relative directions are important because they play a key role in human spatial descriptions and there are several approaches how to represent them using qualitative methods. In these approaches directions between spatial locations can be expressed as constraints over infinite domains, e.g. the Euclidean plane. The theory of relation algebras has been successfully applied to this field. Viewing relation algebras as universal algebras and applying and modifying standard tools from universal algebra in this work, we (re)define notions of qualitative constraint calculus, of homomorphism between calculi, and of quotient of calculi. Based on this method we derive important properties for spatial calculi from corresponding properties of related calculi. From a conceptual point of view these formal mappings between calculi are a means to translate between different granularities.

The Distributed Ontology Language DOL, which is currently being standardised as ISO WD 17347 within the OntoIOp (Ontology Integration and Interoperability) activity of ISO/TC 37/SC 3, aims at providing a unified framework for (1) ontologies formalised in heterogeneous logics, (2) modular ontologies, (3) links between ontologies, and (4) annotation of ontologies.

We propose a novel technique for proving the consistency of large, complex and heterogeneous theories for which ‘standard’ automated reasoning methods are considered insufficient. In particular, we exemplify the applicability of the method by establishing the consistency of the foundational ontology DOLCE, a large, first-order ontology. The approach we advocate constructs a global model for a theory, in our case DOLCE, built from smaller models of subtheories together with amalgamability properties between such models. The proof proceeds by (i) hand-crafting a so-called architectural specification of DOLCE which reflects the way models of the theory can be built, (ii) an automated verification of the amalgamability conditions, and (iii) a (partially automated) series of relative consistency proofs.

Abstract For a number of programming languages, among them Eiffel, C, Java, and Ruby, Hoare-style logics and dynamic logics have been developed. In these logics, pre- and postconditions are typically formulated using potentially effectful programs. In order to ensure that these pre- and postconditions behave like logical formulae (that is, enjoy some kind of referential transparency), a notion of purity is needed. Here, we introduce a generic framework for reasoning about purity and effects. Effects are modelled abstractly and axiomatically, using Moggi’s idea of encapsulation of effects as monads. We introduce a dynamic logic (from which, as usual, a Hoare logic can be derived) whose logical formulae are pure programs in a strong sense. We formulate a set of proof rules for this logic, and prove it to be complete with respect to a categorical semantics. Using dynamic logic, we then develop a relaxed notion of purity which allows for observationally neutral effects such writing on newly allocated memory.

Using category theoretic notions, in particular diagrams and their colimits, we provide a common semantic backbone for various notions of modularity in structured ontologies, and outline a general approach for representing (heterogeneous) combinations of ontologies through interfaces of various kinds, based on the theory of institutions. This covers theory interpretations, (definitional) language extensions, symbol identifications, and conservative extensions. In particular, we study the problem of inheriting conservativity between sub-theories in a diagram to its colimit ontology, and apply this to the problem of localisation of reasoning in ‘modular ontology languages’ such as DDLs or ℰ-connections.

Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. In previous work, we have introduced a Hoare calculus for partial correctness of monadic programs. All this has been done in an entirely monad-independent way. Here, we extend this to a monad-independent dynamic logic (assuming a moderate amount of additional infrastructure for the monad). Dynamic logic is more expressive than the Hoare calculus; in particular, it allows reasoning about termination and total correctness. The background formalism for these concepts is the logic of HasCasl, a higher-order language for functional specification and programming. As an example application, we develop a monad-independent Hoare calculus for total correctness based on our dynamic logic, and illustrate this calculus by a termination proof for Dijkstra's nondeterministic implementation of Euclid's algorithm.

Security policies play an important role in today's computer systems. We show some severe limitations of the wide-spread standard role-based access control (RBAC) model, namely that object-based dynamic separation of duty as introduced by Nash and Poland cannot be expressed with it. We suggest to overcome these limitations by extending the RBAC model with an execution history. The natural next step is then to add temporal logic for the specification of execution orders. We show that with this, object-based dynamic separation of duty, as well as other policies, can be adequately specified.

In this paper, we investigate several logical frameworks whose expressiveness lies between Conditional Equational Logic and Horn Clause Logic. The main result deals with thePART-construction, which interprets total based algebras as partial algebras. This construction can be viewed as a simulation of Horn Clause Theories by means of Conditional Equational Theories. Other constructions in other frameworks are extendable to simulations in a similar way. The notion of categorical retractive simulation captures some essential properties of these, which allows us to measure the equivalence and difference between institutions.