RESEARCH GROUP

THEORETICAL

COMPUTER SCIENCE

Deep learning models are often unaware of the inherent constraints of the task they are applied to. However, many downstream tasks require logical consistency. For ontology classification tasks, such constraints include subsumption and disjointness relations between classes. In order to increase the consistency of deep learning models, we propose a fuzzy loss that combines label-based loss with terms penalising subsumption- or disjointness-violations. Our evaluation on the ChEBI ontology shows that the fuzzy loss is able to decrease the number of consistency violations by several orders of magnitude without decreasing the classification performance. In addition, we use the fuzzy loss for unsupervised learning. We show that this can further improve consistency on data from a distribution outside the scope of the supervised training.

Connecting chemical structural representations with meaningful categories and semantic annotations representing existing knowledge enables data-driven digital discovery from chemistry data. Ontologies are semantic annotation resources that provide definitions and a classification hierarchy for a domain. They are widely used throughout the life sciences. ChEBI is a large-scale ontology for the domain of biologically interesting chemistry that connects representations of chemical structures with meaningful chemical and biological categories. Classifying novel molecular structures into ontologies such as ChEBI has been a longstanding objective for data scientific methods, but the approaches that have been developed to date are limited in several ways: they are not able to expand as the ontology expands without manual intervention, and they are not able to learn from continuously expanding data. We have developed an approach for automated classification of chemicals in the ChEBI ontology based on a neuro-symbolic AI technique that harnesses the ontology itself to create the learning system. We provide this system as a publicly available tool, Chebifier, and as an API, ChEB-AI. We here evaluate our approach and show how it constitutes an advance towards a continuously learning semantic system for chemical knowledge discovery.

Integrating human knowledge into neural networks has the potential to improve their robustness and interpretability. We have developed a novel approach to integrate knowledge from ontologies into the structure of a Transformer network which we call ontology pre-training: we train the network to predict membership in ontology classes as a way to embed the structure of the ontology into the network, and subsequently fine-tune the network for the particular prediction task. We apply this approach to a case study in predicting the potential toxicity of a small molecule based on its molecular structure, a challenging task for machine learning in life sciences chemistry. Our approach improves on the state of the art, and moreover has several additional benefits. First, we are able to show that the model learns to focus attention on more meaningful chemical groups when making predictions with ontology pre-training than without, paving a path towards greater robustness and interpretability. Second, the training time is reduced after ontology pre-training, indicating that the model is better placed to learn what matters for toxicity prediction with the ontology pre-training than without. This strategy has general applicability as a neuro-symbolic approach to embed meaningful semantics into neural networks.

Chemical data is increasingly openly available in databases such as PubChem, which contains approximately 110 million compound entries as of February 2021. With the availability of data at such scale, the burden has shifted to organisation, analysis and interpretation. Chemical ontologies provide structured classifications of chemical entities that can be used for navigation and filtering of the large chemical space. ChEBI is a prominent example of a chemical ontology, widely used in life science contexts. However, ChEBI is manually maintained and as such cannot easily scale to the full scope of public chemical data. There is a need for tools that are able to automatically classify chemical data into chemical ontologies, which can be framed as a hierarchical multi-class classification problem. In this paper we evaluate machine learning approaches for this task, comparing different learning frameworks including logistic regression, decision trees and long short-term memory artificial neural networks, and different encoding approaches for the chemical structures, including cheminformatics fingerprints and character-based encoding from chemical line notation representations. We find that classical learning approaches such as logistic regression perform well with sets of relatively specific, disjoint chemical classes, while the neural network is able to handle larger sets of overlapping classes but needs more examples per class to learn from, and is not able to make a class prediction for every molecule. Future work will explore hybrid and ensemble approaches, as well as alternative network architectures including neuro-symbolic approaches.

Generic ontologies were introduced as an extension (GenericDOL) of the Distributed Ontology, Modeling and Specification Language, DOL, with the aim to provide a language for Generic Ontology Design Patterns. In this paper we present a number of new language constructs that increase the expressivity and the generality of Generic DOL, among them sequential and optional parameters, list parameters with recursion, and local sub-patterns. These are illustrated with non-trivial patterns: generic value sets and (nested) qualitatively graded relations, demonstrated as definitional building blocks in an application domain.

Databases and the query language SQL play a major role in modern applications. In this paper we present an institution-based formalisation of relational databases that uses structures close to those used in SQL. This is the essential difference to other category-theoretical formalisations of databases, which often depart quite far from the SQL standard. We also study SQL queries, using institutional monads, and prove cocompleteness and amalgamation results for the institution.

Generic Ontology Design Patterns, GODPs, are defined in Generic DOL, an extension of the Distributed Ontology, Model and Specification Language, and implemented using the Heterogeneous Tool Set. Parameters such as classes, properties, individuals, or whole ontologies may be instantiated with arguments in a host ontology. The potential of Generic DOL is illustrated with GODPs for an example from the literature, namely Role. We will also discuss how larger GODPs may be composed by instantiating smaller GODPs.

In cognitive science the theory of conceptual blending provides an explanation of the human ability to invent concepts. This cognitive theory provides an inspiration for computational concept invention theory, which has the goal of building creative systems that generate new concepts automatically. In Chapter 3 we discuss a workflow for a system that (a) creatively blends two concepts into a new concept, (b) identifies conflicts, (c) resolves conflicts by generalising the input spaces, and (d) evaluates the new concept against requirements. One critical question for the development of such a system is the choice of an appropriate representation of the conceptual blend and the other steps in the workflow. For this purpose we use the Distributed Ontology, Model and Specification Language (DOL). DOL is a metalanguage that enables the reuse of existing ontologies as building blocks for new ontologies and, further, allows the specification of intended relationships between ontologies. One important feature of DOL is the ability to combine (blend) ontologies that are written in different languages without changing their semantics.

We study the question of consistency of multi-view models in UML and OCL. We first critically survey the large amount of literature that already exists. We find that only limited subsets of the UML/OCL have been covered so far and that consistency checks mostly only cover structural aspects, whereas only few methods also address behaviour. We also give a classification of different techniques for multi"=view UML/OCL consistency: consistency rules, the system model approach, dynamic meta-modelling, universal logic, and heterogeneous transformation. Finally, we elaborate cornerstones of a comprehensive distributed semantics approach to consistency using OMG's Distributed Ontology, Model and Specification Language (DOL).

We combine CASL’s pushout-style generic specification with DOL’s filtering, the latter being a syntactic removal of parts of a specification. The challenge is that now the body of a generic specification can remove parts of the formal parameter. This cannot be handled with usual pushout semantics, but calls for a semantics of “match, delete, glue in” as used in the theory of graph grammars. We hence employ Heindel’s theory of MipMap categories as a basis for the use of pushouts in categories of partial maps. We introduce a notion of MipMap institution that can serve as a semantic background for a partial pushout semantics of generics with filtering.

We propose and study a framework for systematic development of software systems (or models) from their formal specification. We introduce a language for refinement and branching of formal developments. We complement it with a notion of refinement tree and present proof calculi for checking correctness of refinements as well as their consistency. Both calculi have been implemented in the Heterogeneous Tool Set (Hets), and have been integrated with other tools like model finders and conservativity checkers.

Metaphors are an undeniable part of many forms of art and they hint at the underlying conceptualisation that takes place in the silent conversation between an art piece and its perceiver. Abstract art, in particular, requires the viewer not only to analyse the colour palette and the shapes of the strokes but to subconsciously react to the underlying structures that often define the metaphors. After introducing a few cognitive theories involved in perception and knowledge transfer the paper introduces the reader to the painting ``Beneath the Paint''. It is an abstract acrylic painting that plays on the two conceptual metaphor structures `UP is GOOD' and `DARK is BAD' and by presenting them in contradiction force the viewer to subconsciously choose its primary conceptualisation.

Abstract In cognitive science, image schemas are identified as fundamental patterns of cognition. They are schematic prelinguistic conceptualisations of events and serve as conceptual building blocks for concepts. This paper proposes that image schemas can play an important role in computational concept invention, namely within the computational realisation of conceptual blending. We propose to build a library of formalised image schemas, and illustrate how they can guide the search for a base space in the concept invention work flow. Their schematic nature is captured by the idea of organising image schemas into families. Formally, they are represented as heterogeneous, interlinked theories.

We have defined a unified environment that allows formal verification within the Model-Driven Engineering (MDE) paradigm us- ing heterogeneous verification approaches. The environment is based on the Theory of Institutions, which provides a sound basis for representing MDE elements and a way for specifying translations from these elements to other logical domains used for verification, such that formal experts can choose the domain in which they are more skilled to address a formal proof. In this paper we present how this environment can be supported in practice by the Heterogeneous Tool Set (Hets). We define semantic- preserving translations from the MDE elements to the core language of Hets, and we also show how it is possible to move from it to other log- ics, both to supplement the original specification with other verification properties and to perform a heterogeneous verification.

Conceptual blending has been employed very successfully to understand the process of concept invention, studied particularly within cognitive psychology and linguistics. However, despite this influential research, within computational creativity little effort has been devoted to fully formalise these ideas and to make them amenable to computational techniques. Unlike other combination techniques, blending aims at creatively generating (new) concepts on the basis of input theories whose domains are thematically distinct but whose specifications share structural similarity based on a relation of analogy, identified in a generic space, called the base ontology. We here introduce the basic formalisation of conceptual blending, as sketched by the late Joseph Goguen, and discuss some of its variations. We illustrate the vast array of conceptual blends that may be covered by this approach and discuss the theoretical and conceptual challenges that ensue. Moreover, we show how the Distributed Ontology Language DOL can be used to declaratively specify blending diagrams of various shapes, and discuss in detail how the workflow and creative act of generating and evaluating a new, blended concept can be managed and computationally supported within Ontohub, a DOL-enabled theory repository with support for a large number of logical languages and formal linking constructs.

Ontology matching and alignment is a key mechanism for linking the diverse datasets and ontologies arising in the Semantic Web. We show that category theory provides the powerful abstractions needed for a uniform treatment at various levels: semantics, language design, reasoning and tools. The Distributed Ontology Language DOL is extended in a natural way with constructs for networks of ontologies. We in particular show how the three semantics of Zimmermann and Euzenat can be uniformly and faithfully represented using these DOL language constructs. Finally, we summarise how the DOL alignment features are currently being implemented in the Ontohub/Hets ecosystem, including support for the OWL and Alignment APIs.

In this essay we analyse and elucidate the method to establish and clarify the scope of logic theorems offered within the theory of institutions. The method presented pervades a lot of abstract model theoretic developments carried out within institution theory. The power of the proposed general method is illustrated with the examples of (Craig) interpolation and (Beth) definability, as they appear in the literature of institutional model theory. Both case studies illustrate a considerable extension of the original scopes of the two classical theorems. Our presentation is rather narrative with the relevant logic and institution theory concepts introduced and explained gradually to the non-expert reader

We present a framework for formal software development with UML. In contrast to previous approaches that equip UML with a formal semantics, we follow an institution based heterogeneous approach. This can express suitable formal semantics of the different UML diagram types directly, without the need to map everything to one specific formalism (let it be first-order logic or graph grammars). We show how different aspects of the formal development process can be coherently formalised, ranging from requirements over design and Hoare-style conditions on code to the implementation itself. The framework can be used to verify consistency of different UML diagrams both horizontally (e.g., consistency among various requirements) as well as vertically (e.g., correctness of design or implementation w.r.t. the requirements).

Conceptual blending has been employed very successfully to understand the process of concept invention, studied particularly within cognitive psychology and linguistics. However, despite this influential research, within computational creativity little effort has been devoted to fully formalise these ideas and to make them amenable to computational techniques. We here present the basic formalisation of conceptual blending, as sketched by the late Joseph Goguen, and show how the Distributed Ontology Language DOL can be used to declaratively specify blending diagrams. Moreover, we discuss in detail how the workflow and creative act of generating and evaluating a new, blended concept can be managed and computationally supported within Ontohub, a DOL-enabled theory repository with support for a large number of logical languages and formal linking constructs.

Conceptual blending has been employed very successfully to understand the process of concept invention, studied particularly within cognitive psychology and linguistics. However, despite this influential research, within computational creativity little effort has been devoted to fully formalise these ideas and to make them amenable to computational techniques. We here present the basic formalisation of conceptual blending, as sketched by the late Joseph Goguen, and show how the Distributed Ontology Language DOL can be used to declaratively specify blending diagrams. Moreover, we discuss in detail how the workflow and creative act of generating and evaluating a new, blended concept can be managed and computationally supported within Ontohub, a DOL-enabled theory repository with support for a large number of logical languages and formal linking constructs.

Proof calculi for structured specifications have been developed independently of the underlying logical system (formalised as institution). Typically, completeness of these calculi requires interpolation properties of the underlying logic. We develop a relatively complete calculus for structured heterogeneous specifications that does not need interpolation.

Ontohub is a repository engine for managing distributed heterogeneous ontologies. The distributed nature enables communities to share and exchange their contributions easily. The heterogeneous nature makes it possible to integrate ontologies written in various ontology languages. It supports a wide range of formal logical and ontology languages building on the OntoIOp.org project and allows for complex inter-theory (concept) mappings and relationships with formal semantics. Ontohub aims at satisfying a subset of the requirements for an Open Ontology Repository (OOR). OOR is a long-term international initiative, which has not resulted in a complete implementation so far, but established requirements and designed an architecture. Furthermore, Ontohub is being developed in close connection with the Distributed Ontology Language, which is going to be submitted as response to the Object Management Group's Ontology, Model and Specification Integration and Interoperability (OntoIOp) Request For Proposal.

This paper addresses issues arising in the systematic construction of large logical systems. We rely on a model-theoretic view of logical systems, captured by institutions that are in turn presented by parchments. We define their categories, and study constructions that may be carried out in these categories. In particular we show how limits of parchments may be used to combine features involved in various logical systems, sometimes necessarily augmenting the universal construction by additional systematic adjustments. We illustrate these developments by sketching how the logical systems that form the logical foundations of CafeOBJ may be built in this manner.

We present the theoretical background for an extension of the Heterogeneous Tool Set HETS that enables proof support for Common Logic. This is achieved via logic translations that relate Common Logic and some of its sublogics to already supported logics and automated theorem proving systems. We thus provide the first theorem proving support for Common Logic covering the full language, including the possibility of verifying meta-theoretical relationships between Common Logic theories.

The theory of conceptual blending has been applied very successfully in cognitive science to explain the process of concept generation. In previous work, we have shown a formalisation and implementation of conceptual blending that is borrowing techniques from logic, ontological engineering, and algebraic specification. However, so far our attempts (and similar approaches in the literature) have been reconstructive; that is they show how a particular concept (e.g., houseboat) can be ‘discovered’ by computationally blending two carefully selected input spaces (e.g, a house and a boat) and a suitable base. This paper describes an attempt to take the next step and automate the concept generation based on a database of input spaces. Particularly, we attempt to create monsters from a library of animals formalised as OWL ontologies.

The theory of conceptual blending has been applied very successfully in cognitive science to explain the process of concept generation. In previous work, we have shown a formalisation and implementation of conceptual blending that is borrowing techniques from logic, ontological engineering, and algebraic specification. However, so far our attempts (and similar approaches in the literature) have been reconstructive; that is they show how a particular concept (e.g., houseboat) can be `discovered' by computationally blending two carefully selected input spaces (e.g, a house and a boat) and a suitable base. This paper describes an attempt to take the next step and automate the concept generation based on a database of input spaces. Particularly, we attempt to create monsters from a library of animals formalised as OWL ontologies.

In this paper we present a (sound, but incomplete) algorithm for deciding conservativity of extensions of specifications in CASL as part of the Heterogeneous Tool Set (Hets).

We present an architecture that permits compiling declara- tive logic specifications (given in some type theory like LF) into implementations of that logic within the Heterogeneous Tool Set Hets. The central contributions are the use of declaration patterns for singling out a suitable subset of signatures for a particular logic, and the automatic generation of datatypes and functions for parsing and static analysis of declaratively specified logics.

We present the integration of the refinement method of the VSE verification tool, successfully used in industrial applications, in the Heterogeneous Tool Set Hets. The connection is done via introducing the dynamic logic underlying VSE and two logic translations in the logic graph of Hets. Thus the logic-independent layers of Hets are not modified and its proof management formalism can be applied to VSE specifications.

Qualitative spatial and temporal reasoning is based on so-called qualitative calculi. Algebraic properties of these calculi have several implications on reasoning algorithms. But what exactly is a qualitative calculus? And to which extent do the qualitative calculi proposed meet these demands? The literature provides different answers to the first question but only few facts about the second. In this paper we identify the minimal requirements to binary spatio-temporal calculi and we discuss the relevance of the according axioms for representation and reasoning. We also analyze existing qualitative calculi and provide a classification involving different notions of a relation algebra.

Domain modelling based on UML Class Diagrams is an established industrial practice. In the context of the Railway industry, we show how to utilize such diagrams for verification. This involves the translation of UML Class Diagrams into the algebraic specification language CASL. To this end, we define new Class Diagram institutions and provide suitable institution comorphisms.

Novel auction schemes are constantly being designed. Their design has significant consequences for the allocation of goods and the revenues generated. But how to tell whether a new design has the desired properties, such as efficiency, i.e. allocating goods to those bidders who value them most? We say: by formal, machine-checked proofs. We investigated the suitability of the Isabelle, Theorema, Mizar, and Hets/CASL/TPTP theorem provers for reproducing a key result of auction theory: Vickrey's 1961 theorem on the properties of second-price auctions. Based on our formalisation experience, taking an auction designer's perspective, we give recommendations on what system to use for formalising auctions, and outline further steps towards a complete auction theory toolbox.

The Distributed Ontology Language (DOL) is a recent development within the ISO standardisation initiative 17347 Ontology Integration and Interoperability (OntoIOp). In DOL, heterogeneous and distributed ontologies can be expressed, i.e. ontologies that are made up of parts written in ontology languages based on various logics. In order to make the DOL meta-language and its semantics more easily accessible to the wider ontology community, we have developed a notion of institute which are like institutions but with signature partial orders and based on standard set-theoretic semantics rather than category theory. We give an institute-based semantics for the kernel of DOL and show that this is compatible with institutional semantics. Moreover, as it turns out, beyond their greater simplicity, institutes have some further surprising advantages over institutions.

There is a diversity of ontology languages in use, among them OWL, RDF, OBO, Common Logic, and F-logic. Related languages such as UML class diagrams, entity-relationship diagrams and object role modelling provide bridges from ontology modelling to applications, e.g. in software engineering and databases. Another diversity appears at the level of ontology modularity and relations among ontologies. There is ontology matching and alignment, module extraction, interpolation, ontologies linked by bridges, interpretation and refinement, and combination of ontologies. The Distributed Ontology, Modelling and Specification Language (DOL) aims at providing a unified meta language for handling this diversity. In particular, DOL provides constructs for (1) “as-is” use of ontologies formulated in a specific ontology language, (2) ontologies formalised in heterogeneous logics, (3) modular ontologies, and (4) links between on- tologies. This paper sketches the design of the DOL language. DOL will be submitted as a proposal within the OntoIOp (Ontology Integration and Interoperability) standardisation activity of the Object Management Group (OMG).

The Distributed Ontology Language DOL, currently being standardized as ISO WD 17347 within the OntoIOp (Ontology Integration and Interoperability) activity of ISO/TC 37, provides a unified framework for ontologies formalized in heterogeneous logics, modular ontologies, links between ontologies, and ontology annotation. A DOL ontology consists of modules formalized in languages such as OWL or Common Logic, serialized in the existing syntaxes of these languages. On top, DOL's meta level allows for expressing heterogeneous ontologies and links between ontologies, including (heterogeneous) imports and alignments, conservative extensions, and theory interpretations. We present the abstract syntax of these meta-level constructs, with three alternative semantics: direct, translational, and collapsed semantics.

Reasoning over spatial descriptions involving relations that can be described as left, right and inline has been studied extensively during the last two decades. While the fundamental nature of these relations makes reasoning about them applicable to a number of interesting problems, it also makes reasoning about them computationally hard. The key question of whether a given description using these relations can be realized is as hard as deciding satisfiability in the existential theory of the reals. In this paper we summarize the semi-decision procedures proposed so far and present the results of a random benchmark illustrating the relative effectiveness and efficiency of these procedures.

We develop a web service for route finding in OpenStreetMap (OSM) following an activity-centred approach: the aim is not only to assist the user in travelling from A to B, but also to perform a series of specified activities along the way. This is particularly important e.g. for electric mobility, where activities can take place while the battery of the car is recharging. For specifying activities, our tool uses an ontology of spatially-located activities. This ontology then needs to be related to OSM which provides semantic metadata in form of tags. We organised the tags into another ontology (which is then connected to the first one via an ontology mapping), providing thus not only better reference for the OSM community, but also allowing to enrich the ontological semantics of the tags, to deal with their evolving nature and to extract implicit information using ontology- based data access. Moreover, we report first results on an ongoing query corpus experiment involving the OSM community targeted at improving the automated understanding of free text input for certain route finding tasks.

With dramatically increasing volumes of chemical data becoming available in recent years, finding automated means to manage the deluge becomes ever more urgent. Traditional automated classification of chemical entities depends on identifying interesting parts and properties of the molecules. However, classes of chemical entities which are highly symmetrical and which contain large numbers of homogeneous parts (such as carbon atoms) are not straightforwardly classified in this fashion. One such class of molecules is the recently developed fullerene family, discovery of which led to the award of the Nobel prize for chemistry in 1996. Fullerene molecules show potential for many novel applications including in biomedicine. Standard cheminformatics approaches to classification do not easily allow the automatic classification of chemical entities as members of the fullerene class based on their chemical structure, and neither does OWL, due to the tree model requirement. Furthermore, while individual members of the fullerene class can be modelled in standard FOL, expressing the properties of the class as a whole (independent of the count of atoms of the members) requires second-order quantification over the set of atoms in a molecule. Yet, given the size of chemical ontologies such as ChEBI, using second-order expressivity in the general case is prohibitively expensive to practical applications. To address these conflicting requirements, we introduce a novel framework in which we heterogeneously integrate standard ontological modelling with monadic second-order reasoning over chemical graphs, enabling various kinds of information flow between these distinct representational layers.

The Distributed Ontology Language (DOL) is currently being standardised within the OntoIOp (Ontology Integration and Interoper ability) activity of ISO/TC 37/SC 3. It aims at providing a unified framework for ontologies formalised in heterogeneous logics, modular ontologies, links between ontologies, and annotation of ontologies. This paper focuses on building an ontology that formally describes DOL's vocabulary for logics, ontology languages (and their serialisations), as well as logic translations, called LoLa. Interestingly, to adequately formalise the logical relationships between these notions, LoLa itself needs to be axiomatised heterogeneously - a task for which we choose DOL. Namely, we use the logic RDF for Abox assertions, OWL for basic axiomatisations of various modules concerning logics, languages, and translations, FOL for capturing certain closure rules that are not expressible in OWL, and circumscription for minimising the extension of concepts describing default translations.

The Distributed Ontology Language (DOL) is currently being standardized within the OntoIOp (Ontology Integration and Interoperability) activity of ISO/TC 37/SC 3. It aims at providing a unified framework for ontologies formalized in heterogeneous logics, modular ontologies, links between ontologies, and annotation of ontologies. This paper focuses on an application of DOL's meta-theoretical features in mathematical formalization: validating relationships between ontological formalizations of mathematical concepts in COLORE (Common Logic Repository), which provide the foundation for formalizing real-world notions such as spatial and temporal relations.

An important issue in qualitative spatial reasoning is the representation of relative directions. In this paper we present simple geometric rules that enable reasoning about the relative direction between oriented points. This framework, the oriented point algebra OPRA_m, has a scalable granularity m. We develop a simple algorithm for computing the OPRA_m composition tables and prove its correctness. Using a composition table, algebraic closure for a set of OPRA_m statements is sufficient to solve spatial navigation tasks. It turns out that scalable granularity is useful in these navigation tasks.

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 * ontologies formalised in heterogeneous logics, * modular ontologies, * links between ontologies, and * annotation of ontologies. A DOL ontology consists of modules formalised in basic ontology languages, such as OWL or Common Logic, which are serialised in the existing syntaxes of these languages. On top of this, DOL provides a meta-level which allows for expressing heterogeneous ontologies and links between ontologies. Such links include (heterogeneous) imports and alignments, conservative extensions, and theory interpretations. This paper focuses on the abstract syntax and semantics of these meta-level constructs. It introduces three alternative semantics for the meta-level, namely direct, translational, and collapsed semantics (the latter is only briefly sketched), and studies their respective pros and cons.

The language CspCASL combines specifications of data and processes. We give an institution based semantics to CspCASL that allows us to re-use the institution independent structuring mechanisms of CASL. Furthermore, we extend CspCASL with a notion of refinement that reconciles the differing philosophies behind the refinement notions for CSP and CASL. We develop a compositional proof calculus for refinement along the CASL structuring mechanisms, and demonstrate that compositional proof techniques along parallel process composition from the context of CSP lifts to structured CspCASL specifications.

Motivation: Advancing our understanding of how nervous systems work will require the ability to store and annotate 3D anatomical datasets, recording morphology, partonomy and connectivity at multiple levels of granularity from subcellular to gross anatomy. It will also require the ability to integrate this data with other data-types including functional, genetic and electrophysiological data. The web ontology language OWL2 provides the means to solve many of these problems. Using it, one can rigorously define and relate classes of anatomical structure using multiple criteria. The resulting classes can be used to annotate datasets recording, for example, gene expression or electrophysiology. Reasoning software can be used to automate classification and error checking and to construct and answer sophisticated combinatorial queries. But for such queries to give consistent and biologically meaningful results, it is important that both classes and the terms (relations) used to relate them are carefully defined. Results: We formally define a set of relations for recording the spatial and connectivity relationships of neuron classes and brain regions in a broad range of species, from vertebrates to arthropods. We illustrate the utility of our approach via its application in the ontology that drives the Virtual Fly Brain web resource.

We develop a web service focusing on finding places not (only) by their address, but by systematically relating the places to activities that a person could perform there. This is helpful if a person wants to explore a new city, or plans leisure activities. OpenStreetMap provides a rich set of tags that can be used for activity-oriented search. We propose the use of several ontologies that are related to each other using matching tools to cope with the evolving nature of the tags available in social media.

We provide an ontology for OpenStreetMap tags, called OSMonto, which can be used in different ways: (1) browsing of the hierarchy of tags is eased, (2) tags can be related with other ontologies, let it be tool-specific ontologies or more general ontologies like the recent Schema.org ontology supported by the dominant search engines, and (3) concepts can be unified, even if they are tagged in various ways. This will foster the integration of OpenStreetMap into the semantic web.

We recall a language for refinement and branching of formal developments. We introduce a notion of refinement tree and present proof calculi for checking correctness of refinements as well as their consistency. Both calculi have been implemented in the Heterogeneous Tool Set (Hets), and have been integrated with other tools like model finders and conservativity checkers. This technique has already been applied for showing the consistency of a first-order ontology that is too large to be tackled directly by model finders.

Classification of chemical entities is generally based on identifying the interesting parts and properties of the molecules. However, classes of chemical entities which are highly symmetrical and which contain large numbers of homogeneous parts (such as carbon atoms) are not straightforwardly classified in this fashion. One such class of molecules is the recently developed fullerene family, discovery of which led to the award of the Nobel prize for chemistry in 1996. Fullerene molecules show potential for many novel applications including in biomedicine. Whilst standard knowledge representation approaches in chemistry are inadequate to allow the automatic classification of chemical entities as members of the fullerene class based on their chemical structure, standard OWL representations are insufficient for this task as well. We here sketch an alternative framework in which we heterogeneously integrate ontological modelling with monadic second-order reasoning over chemical graphs and topological features of the molecules, enabling a threefold information flow between these distinct representational layers, namely a debugging of the ontology, an abductive enrichment of the ontology, and an inductive learning of new graph classes.

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.

The Hyperontology framework has been recently introduced to provide a general methodology for heterogeneous ontology design, i.e. the construction of ontologies that have parts, or modules, written in dierent formalisms, and which are interlinked in complex ways. We here present a brief outline of this framework, discuss its features and merits, and illustrate its usefulness for the domain of biomedical ontology design by providing and discussing a number of examples.

We present an overview of the landscape of ontology languages, mostly pertaining to the first-order paradigm. In particular, we present a uniform formalisation of these languages based on the institution theoretical framework, allowing a systematic treatment and analysis of the translational relationships between the various languages and a general analysis of properties of such translations. We also discuss the importance of language translation from the point of view of ontological modularity and logical pluralism, and for the borrowing of tools and reasoners between languages.

Even though ontologies are widely being used to enable interoperability in information-rich endeavours, there is currently no unified framework for ontology interoperability itself. Surprisingly little of the state of the art in modularity and structuring, e.g. in software engineering, has been applied to ontology engineering so far. However, application areas like Ambient Assisted Living (AAL), which require synchronisation and orchestration of interoperable services, are in dire need of safe and secure ontology interoperability. OntoIOp (Ontology Integration and Interoperability), a new international standard proposed in ISO/TC 37/SC 3, aims at filling this gap.

Qualitative spatial calculi offer a method to describe spatial configurations in a framework based on a finite set of relations that abstracts from the underlying mathematical theory. But an open issue is whether they can be employed in applications. Further their cognitive adequacy is questionable or not investigated at all. In this paper we investigate the applicability of OPRA to navigation in street networks that are described via local observations. Further we scrutinize whether a description of directions that is deemed cognitively adequate and can be described in OPRA can perform that task. We are using an environment that we developed ourselves for these experiments, the used algorithms and the program itself are explained in detail.

More than 15 years ago, a set of qualitative spatial relations between oriented straight line segments (dipoles) was suggested by Schlieder. However, it turned out to be difficult to establish a sound constraint calculus based on these relations. In this paper, we present the results of a new investigation into dipole constraint calculi which uses algebraic methods to derive sound results on the composition of relations of dipole calculi. This new method, which we call condensed semantics, is based on an abstract symbolic model of a specific fragment of our domain. It is based on the fact that qualitative dipole relations are invariant under orientation preserving affine transformations. The dipole calculi allow for a straightforward representation of prototypical reasoning tasks for spatial agents. As an example, we show how to generate survey knowledge from local observations in a street network. The example illustrates the fast constraint-based reasoning capabilities of dipole calculi. We integrate our results into two reasoning tools which are publicly available.

The error-prone process of formal specification and verification of large systems requires an efficient, evolutionary formal development approach. Development graphs have been designed to support such an approach. They can formally represent the actual state of a software development comprising specification and verification work in a structured way and assist the user in her evolutionary development by the incorporated change management support. In this paper we extend this work with respect to heterogeneous development graphs allowing one to make use of different institutions, i.e. logics, for specifying and verifying large developments. We also push forward the idea of stringent locality of definitions by introducing pre-signatures and pre-signature morphisms, which allow us to build up signatures in an incremental and parametric way.

A prerequisite for the practical use of a specification language is the existence of a set of predefined specifications. Although the Common Algebraic Specification Language (CASL) has a library with such predefined specifications, its higher order extension, named HASCASL, still lacks a library with basic higher order data types and functions. In this paper, we describe the specification and verification of a library for the HASCASL language. Our library covers a subset of the Haskell Prelude library, including data types and classes representing Booleans, lists, characters, strings, equality, and ordering functions. We use the Heterogeneous Tool Set (HETS) for parsing specifications, generating proof obligations, and translating between the HASCASL and HOL languages. To discharge the arising proof obligations, we use the Isabelle/HOL interactive theorem prover.

Maude modules can be understood as models that can be formally analyzed and verified with respect to different properties expressing various formal requirements. However, Maude lacks the formal tools to perform some of these analyses and thus they can only be done by hand. The Heterogeneous Tool Set Hets is an institution-based combination of different logics and corresponding rewriting, model checking and proof tools. We present in this paper an integration of Maude into Hets that allows to use the logics and tools already integrated in Hets with Maude specifications. To achieve such integration we have dened an institution for Maude based on preordered algebras and a comorphism between Maude and CASL, the central logic in Hets.

We introduce ontological blending as a new method for combining ontologies. In contrast to other combination techniques that aim at integrating or assimilating categories and relations of thematically closely related ontologies, blending aims at `creatively' generating new categories and ontological definitions on the basis of input ontologies whose domains are thematically distinct but whose specifications share structural or logical properties. As a result, ontological blending can generate new ontologies and concepts and it allows a more flexible technique for ontology combination than existing methods. The approach is inspired by conceptual blending in cognitive science, and draws on methods from ontological engineering, algebraic specification, and computational creativity in general.

We present a general framework for the design of formal ontologies, resting on two main principles: firstly, we endorse Rudolf Carnap's principle of logical tolerance by giving central stage to the concept of logical heterogeneity, i.e. the use of a plurality of logical languages within one ontology design. Secondly, to structure and combine heterogeneous ontologies in a semantically well-founded way, we base our work on abstract model theory in the form of institutional semantics, as forcefully put forward by Joseph Goguen and Rod Burstall. The theoretical foundation in institution theory establishes a close link to algebraic specification theory. We explore this link by systematically applying tools and techniques from this area to corresponding ontology structuring and design tasks, in particular employ the structuring mechanisms of the heterogeneous algebraic specification language HetCASL for defining an abstract notion of structured heterogeneous ontology, leading to the idea of a hyperontology, a heterogeneous, distributed, highly modular and structured ontology. This approach enables the designer to split up a heterogeneous ontology into semantically meaningful parts and employ dedicated reasoning tools to them. Moreover, we distinguish, on a structural and semantic level, several different kinds of combining and aligning heterogeneous ontologies, namely integration, connection, and refinement. The notion of heterogeneous refinement can, in particular, be used to provide both a general notion of sub-ontology as well as a notion of heterogeneous equivalence of ontologies. Finally, we sketch how different modes of reasoning over ontologies are related to these different structuring aspects.

This paper investigates the idea to treat repositories of ontologies as interlinked networks of ontologies, formally captured by the notion of a hyperontology. We apply standard matching algorithms to automatically create the linkage structure of the repository by performing pairwise matching. Subsequently, we define a modular workflow to construct combinations of alignments for any finite number of ontologies. This workflow employs and makes interoperable several tools from the ontology engineering world, comprising matching, reasoning, and structuring tools, and supports in particular modular ontology extraction based on alignment, and a study and empirical analysis of (in)consistency propagation in connected alignments (the Chinese Whispers problem).

In the area of qualitative spatial reasoning, the LR calculus is a quite simple constraint calculus that forms the core of several orientation calculi like the dipole calculi and the OPRA-1 calculus. For many qualitative spatial calculi, algebraic closure is applied as standard polynomial time decision procedure. For a long time it was believed that this can decide the consistency of scenarios of the quite simple and basic LR calculus (a refinement of Ligozat's flip-flop calculus). However, Lücke et al. showed that algebraic closure is a quite bad approximation of consistency of LR scenarios: scenarios in the base relations "Left" and "Right" are always algebraically closed. So algebraic closure is completely useless here. Furthermore, Wolter and Lee have proved that the consistency problem for any calculus with relative orientation containing the relations "Left" and "Right" is NP-hard. In this paper we propose a new polynomial time approximation procedure for this NP-hard problem. It is based on the angles of triangles in the Euclidean plane. LR scenarios are translated to sets of linear inequations over the real numbers. We evaluate the quality of this procedure by comparing it both to the old approximation using algebraic closure and to the (exact but exponential time) Buchberger algorithm for Gröbner bases.

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.

An important issue in Qualitative Spatial Reasoning is the representation of relative direction. In this paper we present simple geometric rules that enable reasoning about relative direction between oriented points. This framework, the Oriented Point Algebra OPRA_m, has a scalable granularity m. We develop a simple algorithm for computing the OPRA_m composition tables and prove its correctness. Using a composition table, algebraic closure for a set of OPRA statements is sufficient to solve spatial navigation tasks. And it turns out that scalable granularity is useful in these navigation tasks.

We present the integration of refinement method of VSE verification tool, successfully used in industrial applications, in the Heterogeneous Tool Set Hets. The connection is done via introducing the dynamic logic underlying VSE and two logic translations in the logic graph of Hets. Thus the logic-independent layers of Hets are not modified and its proof management formalism can be applied to VSE specifications.

Nearly 15 years ago, a set of qualitative spatial relations between oriented straight line segments (dipoles) was suggested by Schlieder. This work received substantial interest amongst the qualitative spatial reasoning community. However, it turned out to be difficult to establish a sound constraint calculus based on these relations. In this paper, we present the results of a new investigation into dipole constraint calculi which uses algebraic methods to derive sound results on the composition of relations and other properties of dipole calculi. Our results are based on a condensed semantics of the dipole relations. In contrast to the points that are normally used, dipoles are extended and have an intrinsic direction. Both features are important properties of natural objects. This allows for a straightforward representation of prototypical reasoning tasks for spatial agents. As an example, we show how to generate survey knowledge from local observations in a street network. The example illustrates the fast constraint-based reasoning capabilities of the dipole calculus. We integrate our results into two reasoning tools which are publicly available.

We use the theory of institutions to capture the concept of a heterogeneous logical environment as a number of institutions linked by institution morphisms and comorphisms. We discuss heterogeneous specifications built in such environments, with inter-institutional specification morphisms based on both institution morphisms and comorphisms. We distinguish three kinds of heterogeneity: (1) specifications in logical environments with universal logic (2) heterogeneous specifications focused at a particular logic, and (3) heterogeneous specifications distributed over a number of logics.

We study logic translations from an abstract perspective, without any commitment to the structure of sentences and the nature of logical entailment, which also means that we cover both proof- theoretic and model-theoretic entailment. We show how logic translations induce notions of logical expressiveness, consistency strength and sublogic, leading to an explanation of paradoxes that have been described in the literature. Connectives and quantifiers, although not present in the definition of logic and logic translation, can be recovered by their abstract properties and are preserved and reflected by translations under suitable conditions.

We lay out the design of HasCASL, a higher order extension of the algebraic specification language CASL that serves both as a wide-spectrum language for the rigorous specification and development of software, in particular but not exclusively in modern functional programming languages, and as an expressive standard language for higher-order logic. Distinctive features of HasCASL include partial higher order functions, higher order subtyping, shallow polymorphism, and an extensive type-class mechanism. Moreover, HasCASL provides dedicated specification support for monad-based functional-imperative programming with generic side effects, including a monad-based generic Hoare logic.

Colimits are a useful tool for the combination of specifications and logical theories. We generalize the notion of colimit to a heterogeneous multi-logic setting. For practically realistic cases, the notion has to be weakened. We describe an algorithm that approximates the weaker notion but obtains a colimit whenever possible. This algorithm is being implemented as part of the Heterogeneous Tool Set Hets.

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 E-connections.

This paper systematically applies tools and techniques from the area of algebraic specification theory to corresponding ontology structuring and design tasks. We employ the heterogeneous structuring mechanisms of the heterogeneous algebraic specification language HetCASL for defining an abstract notion of structured heterogeneous ontology. This approach enables the designer to split up a heterogeneous ontology into semantically meaningful parts and employ dedicated reasoning tools to them. In particular, we distinguish three fundamentally different kinds of combining heterogeneous ontologies: integration, connection, and refinement.

We present a general approach for representing and combining alignments and computing these combinations, based on the category theoretic notions of diagram, pushout, and colimit. This generalises the possible `shapes' of alignments that have been introduced previously in similar approaches. We use the theory of institutions to represent heterogeneous ontologies, and show how the tool Hets can be employed to compute the colimit ontology of an alignment diagram.

Various calculi have been designed for qualitative constraint-based representation and reasoning. Especially for orientation calculi, it happens that the well-known method of algebraic closure cannot decide consistency of constraint networks, even when considering networks over base relations (= scenarios) only. We show that this is the case for all relative orientation calculi capable of distinguishing between ``left of'' and ``right of''. Indeed, for these calculi, it is not clear whether efficient (i.e. polynomial) algorithms deciding scenario-consistency exist. As a partial solution of this problem, we present a technique to decide global consistency in qualitative calculi. It is applicable to all calculi that employ convex base relations over the real-valued space R^n and it can be performed in polynomial time when dealing with convex relations only. Since global consistency implies consistency, this can be an efficient aid for identifying consistent scenarios. This complements the method of algebraic closure which can identify a subset of inconsistent scenarios.

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 modeled 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.

CASL is an expressive specification language that has been designed to supersede many existing algebraic specification languages and provide a standard. CASL consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications; the latter are used to prescribe the modular structure of implementations. We describe a simplified version of the CASL syntax, semantics and proof calculus for each of these three layers and state the corresponding soundness and completeness theorems. The layers are orthogonal in the sense that the semantics of a given layer uses that of the previous layer as a ``black box'', and similarly for the proof calculi. In particular, this means that CASL can easily be adapted to other logical systems. We conclude with a detailed example specification of a warehouse, which serves to illustrate the application of both CASL and the proof calculi for the various layers.

In this paper we propose that adequate treatments of space need to be multiperspectival and related to sound foundational ontologies. To support this, we show that natural spatial descriptions commonly appeal to diverse theories of space and these need to be formally combined to be fully interpreted. Our account draws particularly on the foundational ontology DOLCE and the algebraic specification language CASL. We show how the structuring mechanisms of CASL suggest mechanisms for both building and combining multiperspectival ontologies of space. We also suggest that these mechanisms provide a natural link both with currently emerging cognitive principles such as blending and with developments in ontology mediation and mapping.

We introduce a generic notion of propositional categorical logic and provide a construction of an institution with proofs out of such a logic, following the Curry-Howard-Tait paradigm. We then prove logic-independent soundness and completeness theorems. The framework is instantiated with a number of examples: classical, intuitionistic, linear and modal propositional logics. Finally, we speculate how this framework may be extended beyond the propositional case.

Several modularity concepts for ontologies have been studied in the literature. Can they be brought to a common basis? We propose to use the language of category theory, in particular diagrams and their colimits, for answering this question. We outline a general approach for representing combinations of logical theories, or ontologies, through interfaces of various kinds, based on diagrams and the theory of institutions. In particular, we consider theory interpretations, language extensions, symbol identification, and conservative extensions. We study the problem of inheriting conservativity between sub-theories in a diagram to its colimit ontology. Finally, we apply this to the problem of conservativity when composing DDLs or E-connections.

We connect the algebraic specification language CASL with a variety of automated first-order provers. The heart of this connection is an institution comorphism from CASL to SoftFOL (softly typed first-order logic); the latter is then translated to the provers' input syntaxes. We also describe a GUI integrating the translations and the provers into the Heterogeneous Tool Set. We report on experiences with provers, which led to fine-tuning of the translations. This framework can also be used for checking consistency of specifications.

We introduce two institutions for the process algebra CSP, one for the traces model, and one for the stable failures model. The construction is generic and should be easily instantiated with further models. As a consequence, we can use structured specification constructs like renaming, hiding and parameterisation (that have been introduced over an arbitrary institution) also for CSP. With a small example we demonstrate that structuring indeed makes sense for CSP.

Heterogeneous specification becomes more and more important because complex systems are often specified using multiple viewpoints, involving multiple formalisms. Moreover, a formal software development process may lead to a change of formalism during the development. However, current research in integrated formal methods only deals with ad-hoc integrations of different formalisms. The heterogeneous tool set (Hets) is a parsing, static analysis and proof management tool combining various such tools for individual specification languages, thus providing a tool for heterogeneous multi-logic specification. Hets is based on a graph of logics and languages (formalized as so-called institutions), their tools, and their translations. This provides a clean semantics of heterogeneous specifications, as well as a corresponding proof calculus. For proof management, the calculus of development graphs (known from other large-scale proof management systems) has been adapted to heterogeneous specification. Development graphs provide an overview of the (heterogeneous) specification module hierarchy and the current proof state, and thus may be used for monitoring the overall correctness of a heterogeneous development. We illustrate the approach with a sample heterogeneous proof proving the correctness of the composition table of a qualitative spatial calculus. The proof involves two different provers and logics: an automated first-order prover solving the vast majority of the goals, and an interactive higher-order prover used to prove a few bridge lemmas.

This paper builds on the theory of institutions, a version of abstract model theory that emerged in computer science studies of software specification and semantics. To handle proof theory, our institutions use an extension of traditional categorical logic with sets of sentences as objects instead of single sentences, and with morphisms representing proofs as usual. A natural equivalence relation on institutions is defined such that its equivalence classes are logics. Several invariants are defined for this equivalence, including a Lindenbaum algebra construction, its generalization to a Lindenbaum category construction that includes proofs, and model cardinality spectra; these are used in some examples to show logics inequivalent. Generalizations of familiar results from first order to arbitrary logics are also discussed, including Craig interpolation and Beth definability.

We propose to extend the algebraic-coalgebraic specification language CoCASL by full coalgebraic modal logic based on predicate liftings for functors. This logic is more general than the modal logic previously used in CoCASL and supports the specification of a variety of modal logics, such as graded modal logic, majority logic, and probabilistic modal logic. CoCASL thus becomes a modern modal language that covers a wide range of Kripke and non-Kripke semantics of modal logics via the coalgebraic interpretation.

We present partial translations of Haskell programs to Isabelle that have been implemented as part of the Heterogeneous Tool Set. The the target logic is Isabelle/HOLCF, and the translation is based on a shallow embedding approach.

In the domain of qualitative constraint reasoning, a subfield of AI which has evolved in the past 25 years, a large number of calculi for efficient reasoning about spatial and temporal entities have been developed. Reasoning techniques developed for these constraint calculi typically rely on the respective composition table of the calculus at hand, but often these composition tables are developed in a quite informal manner only and hence are prone to errors. In view of possible safety critical applications of qualitative calculi it is desirable to formally verify these composition tables. In general, however, the verification of composition tables is a tedious task, in particular, in those cases where the semantics of the calculus depends on higher-order constructs such as sets. In this paper we address this problem by presenting a heterogeneous proof method that allows for combining a higher-order proof assistance system (such as Isabelle) with an automatic (first order) reasoner (such as SPASS). The benefit of this method is that the number of proof obligations that is to be proven by hand with a semi-automatic reasoner can be minimized to an acceptable level.

Monads serve the abstract encapsulation of side effects in semantics and functional programming. Various monad-based specification languages have been introduced in order to express requirements on generic side-effecting programs. A basic role is played here by global evaluation logic, concerned with formulae which may be thought of as being universally quantified over the state space; this formalism is the fundament of more advanced logics such as monad-based Hoare logic or dynamic logic. We prove completeness of global evaluation logic for models in cartesian categories with a distinguished Heyting algebra object.

Recently, various process calculi have been introduced which are suited for the modelling of mobile computation and in particular the mobility of program code; a prominent example is the ambient calculus. Due to the complexity of the involved spatial reduction, there is --- in contrast to the situation in standard process algebra --- up to now no satisfying coalgebraic representation of a mobile process calculus. Here, we discuss a coalgebraic denotational semantics for the ambient calculus, viewed as a step towards a generic coalgebraic framework for modelling mobile systems. Crucial features of our modelling are a set of GSOS style transition rules for the ambient calculus, a hardwiring of the so-called hardening relation in the functorial signature, and a set-based treatment of hidden name sharing. The formal representation of this framework is cast in the algebraic-coalgebraic specification language CoCASL.

Development graphs are a tool for dealing with structured specifications in a formal program development in order to ease the management of change and reusing proofs. In this work, we extend development graphs with hiding (e.g. hidden operations). Hiding is a particularly difficult to realize operation, since it does not admit such a good decomposition of the involved specifications as other structuring operations do. We develop both a semantics and proof rules for development graphs with hiding. The rules are proven to be sound, and also complete relative to an oracle for conservative extensions. We also show that an absolutely complete set of rules cannot exist. The whole framework is developed in a way independent of the underlying logical system (and thus also does not prescribe the nature of the parts of a specification that may be hidden). We also show how various other logic independent specification formalisms can be mapped into development graphs; thus, development graphs can serve as a kernel formalism for management of proofs and of change.

In the domain of qualitative constraint reasoning, a subfield of AI which has evolved in the last 25 years, a large number of calculi for efficient reasoning about space and time has been developed. Reasoning problems in such calculi are usually formulated as constraint satisfaction problems. For temporal and spatial reasoning, these problems often have infinite domains, which need to be abstracted to (finite) algebras in order to become computationally feasible. Ligozat has argued that the notion of weak representation plays a crucial role: it not only captures the correspondence between abstract relations (in a relation algebra or non-associative algebra) and relations in a concrete domain, but also corresponds to algebraically closed constraint networks. In this work, we examine properties of the category of weak representations and treat the relations between partition schemes, non-associative algebras and concrete domains in a systematic way. This leads to the notion of semi-strong representation, which captures the correspondence between abstract and concrete relations better than the notion of weak representation does. The slogan is that semi-strong representations avoid unnecessary loss of information. Furthermore, we hope that the categorical perspective will help in the future to provide new insights on the important problem of determining whether algebraic closedness decides consistency of constraint networks.

We introduce CoCASL as a light-weight but expressive coalgebraic extension of the algebraic specification language CASL. CoCASL allows the nested combination of algebraic datatypes and coalgebraic process types. Moreover, it provides syntactic sugar for an observer-indexed modal logic that allows e.g. expressing fairness properties. This logic includes a generic definition of modal operators for observers with structured equational result types. We prove existence of final models for specifications in a format that allows the use of certain initial datatypes, as well as modal axioms. The use of CoCASL is illustrated by specifications of the process algebras CSP and CCS.

The Heterogeneous Tool Set (Hets) is the main analysis tool for the specification language heterogeneous CASL. Heterogeneous CASL (HetCASL) combines the specification language CASL with CASL extensions and sublanguages, as well as completely different logics and even programming languages such as Haskell. HetCASL extends the structuring mechanisms of CASL: Basic specifications are unstructured specifications or modules written in a specific logic. HEts is based on a graph of logics and logic translations (the latter are also called comorphisms). With heterogeneous structured specifications, it is possible to combine and rename specifications, hide parts thereof, and also translate them to other logics. Hets consists of logic-specific tools for the parsing and static analysis of the different involved logics, as well as a logic-independent parsing and static analysis tool for structured and architectural specifications and libraries. The latter of course needs to call the logic-specific tools whenever a basic specification is encountered.

We propose to use Grothendieck institutions based on 2-categorical diagrams as a basis for heterogeneous specification. We prove a number of results about colimits and (some weak variants of) exactness. This framework can also be used for obtaining proof systems for heterogeneous theories involving institution semi-morphisms.

The presence of computational effects, such as state, store, exceptions, input, output, non-determinism, backtracking etc., complicates the reasoning about programs. In particular, usually for each effect (or each combination of these), an own logic needs to be designed. Monads are a well-known tool from category theory that originally has been invented for studying algebraic structures. Monads have been used very successfully by Moggi to model computational effects (in particular, all of those mentioned above) in an elegent way. This has been applied both to the semantics of programming languages and to the encapsulation of effects in pure functional languages such as Haskell. Several logics for reasoning about monadic programs have been introduced, such as evaluation logic, Hoare logic and dynamic logic. Some of these logics have a semantics and proof calculus given in a completely monad independent (and hence, effect independent) way. We give an overview of these logics, discuss completeness of their calculi, as well as some application of these logics to the reasoning about Haskell and Java programs, and a coding in the theorem prover Isabelle.

Coalgebra has in recent years been recognized as the framework of choice for the treatment of reactive systems at an appropriate level of generality. Proofs about the reactive behavior of a coalgebraic system typically rely on the method of coinduction. In comparison to `traditional' coinduction, which has the disadvantage of requiring the invention of a bisimulation relation, the method of emphcircular coinduction allows a higher degree of automation. As part of an effort to provide proof support for the algebraic-coalgebraic specification language textmdtextscCoCasl, we develop a new coinductive proof strategy which iteratively constructs a bisimulation relation, thus arriving at a new variant of circular coinduction. Based on this result, we design and implement tactics for the theorem prover Isabelle which allow for both automatic and semiautomatic coinductive proofs. The flexibility of this approach is demonstrated by means of examples of (semi-)automatic proofs of consequences of textmdtextscCoCasl specifications, automatically translated into Isabelle theories by means of the Bremen heterogeneous CASL tool set Hets.

Recently, various process calculi have been introduced which are suited for the modelling of mobile computation and in particular the mobility of program code; a prominent example is the ambient calculus. Due to the complexity of the involved spatial reduction, there is - in contrast to the situation in standard process algebra - up to now no satisfying coalgebraic representation of a mobile process calculus. Here, we discuss work towards a unifying coalgebraic framework for the denotational semantics of mobile systems. The connection between the ambient calculus and a coalgebraic approach which uses an extension of labelled transition systems in the representation of the reduction relation is analyzed in more detail. The formal representation of this framework is cast in the algebraic-coalgebraic specification language CoCASL.

High-Level net models following the paradigm “nets as tokens” have been studied already in the literature with several interesting applications. In this paper we propose the new paradigm “nets and rules as tokens”, where in addition to nets as tokens also rules as tokens are considered. The rules can be used to change the net structure. This leads to the new concept of high-level net and rule systems, which allows to integrate the token game with rule-based transformations of P/T-systems. The new concept is based on algebraic high-level nets and on the main ideas of graph transformation systems. We introduce the new concept with the case study “House of Philosophers”, a dynamic extension of the well-known dining philosophers. In the main part we present a basic theory for rule-based transformations of P/T-systems and for high-level nets with nets and rules as tokens leading to the concept of high-level net and rule systems.

This paper describes a sublanguage of CASL, called CASL-DL, that corresponds to the Web Ontology Language (OWL) being used for the semantic web. OWL can thus benefit from CASL's strong typing discipline and powerful structuring concepts. Vice versa, the automatic decision procedures available for OWL DL (or more precisely, the underlying description logic SHOIN(D)) become available for a sublanguage of CASL. This is achieved via translations between CASL-DL and SHOIN(D), formalized as so-called institution comorphisms.

We extend CASL architectural specifications with a simple refinement language that allows the formalization of developments as refinement trees. The essence of the extension is to allow refinements of unit specifications in CASL architectural specifications.

This paper builds on the theory of institutions, a version of abstract model theory that emerged in computer science studies of software specification and semantics. To handle proof theory, our institutions use an extension of traditional categorical logic with sets of sentences as objects instead of single sentences, and with morphisms representing proofs as usual. A natural equivalence relation on institutions is defined such that its equivalence classes are logics. Several invariants are defined for this equivalence, including a Lindenbaum algebra construction, its generalization to a Lindenbaum category construction that includes proofs, and model cardinality spectra; these are used in some examples to show logics inequivalent. Generalizations of familiar results from first order to arbitrary logics are also discussed, including Craig interpolation and Beth definability.

We present a semantics for architectural specifications in CASL, including an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for CASL models. To circumvent this problem, we extend the CASL logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor satisfies the amalgamation property as well as its converse, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Moreover, amalgamation for enriched CASL means that a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for CASL.

Higher-order logic with ML-style type class polymorphism is widely used as a specification formalism. Its polymorphic entities (types, operators, axioms) can easily be equipped with a `naive' semantics defined in terms of collections of instances. However, this semantics has the unpleasant property that while model reduction preserves satisfaction of sentences, model expansion generally does not. In other words, unless further measures are taken, type class polymorphism fails to constitute a proper institution, being only a so-called rps preinstitution; this is unfortunate, as it means that one cannot use institution-independent or heterogeneous structuring languages, proof calculi, and tools with it. Here, we suggest to remedy this problem by modifying the notion of model to include information also about its potential future extensions. Our construction works at a high level of generality in the sense that it provides, for any preinstitution, an institution in which the original preinstitution can be represented. The semantics of polymorphism used in the specification language HasCASL makes use of this result. In fact, HasCASL's polymorphism is a special case of a general notion of polymorphism in institutions introduced here, and our construction leads to the right notion of semantic consequence when applied to this generic polymorphism. The appropriateness of the construction for other frameworks that share the same problem depends on methodological questions to be decided case by case. In particular, it turns out that our method is apparently unsuitable for observational logics, while it works well with abstract state machine formalisms such as state-based CASL.

Following the paradigm of encapsulation of side effects via monads, the Java execution mechanism has been described by the so-called Java monad, encorporating essentially stateful computation and exceptions, which are heavily used in Java control flow. A technical problem that appears in this model is the fact that the return exception in Java is parametrized by the return value, so that method calls actually move between slightly different monads, depending on the type of the return value. We provide a treatment of this problem in the general framework of exception monads as introduced in earlier work by some of the authors; this framework includes generic partial and total Hoare calculi for abrupt termination. Moreover, we illustrate this framework by means of a verification of a pattern match algorithm.

In AI a large number of calculi for efficient reasoning about spatial and temporal entities have been developed. The most prominent temporal calculi are the point algebra of linear time and Allen's interval calculus. Examples of spatial calculi include mereotopological calculi, Frank's cardinal direction calculus, Freksa's double cross calculus, Egenhofer and Franzosa's intersection calculi, and Randell, Cui, and Cohn's region connection calculi. These calculi are designed for modeling specific aspects of space or time, respectively, to the effect that the class of intended models may vary widely with the calculus at hand. But from a formal point of view these calculi are often closely related to each other. For example, the spatial region connection calculus RCC5 may be considered a coarsening of Allen's (temporal) interval calculus. And vice versa, intervals can be used to represent spatial objects that feature an internal direction. The central question of this paper is how these calculi as well as their mutual dependencies can be axiomatized by algebraic specifications. This question will be investigated within the framework of the Common Algebraic Specification Language (CASL), a specification language developed by the Common Framework Initiative for algebraic specification and development (CoFI). We explain scope and expressiveness of CASL by discussing the specifications of some of the calculi mentioned before.

This paper proposes to use CASL (Common Algebraic Specification Language; designed by CoFI -- Common Framework Initiative) for formalising ontologies in FOL. The major advantage of CASL over other specification techniques is its static strong typing and subtyping. Namely, using sorts (types) instead of unary predicates for the ontological categories gives the possibility to find unintended application of n-ary predicates during the type checking of CASL. Another advantage of CASL is its structuring facilities that provide renaming and hiding of symbols used in specifications and the instantiation of parametrised specifications. All this is supported by an evolving tool set for syntax and type analysis, called HETS (Heterogeneous Tool Set), that provides the connection to various provers (interactive and automatic). The tool set allows the combination and detection of various different logics and sublogics. There is a further specialisation of CASL related to the Semantic Web ontology language OWL-DL called CASL-DL (CASL-Description Logic). It gives, as a sublanguage of CASL, the ability to use automatic reasoners like Racer for inferences while using HETS for type checking of the predicates. A consistent view of the same ontology in CASL (for expressiveness) and CASL-DL (for easier automated reasoning with tools like Fact and Racer) is provided by using HETS. Moreover, the first-order axioms can be kept when using a first-order prover. It is well known that there are first-order provers that are as fast as Fact or Racer on description logic fragments, thus combining the best of both worlds. We use HETS as a tool to exploit this possibility.

The purpose of this paper is threefold: (1) to show a methodology for introducing formality step-by-step, starting from a "light-weight'' ontology, (2) to apply it to the generic Route Graph model, instantiated here to Tramway Networks, and (3) to demonstrate that separation of concerns into layers of abstraction and application of generic formal notions such as graph abstraction lead to a useful decomposition of safety properties.

Heterogeneous CASL (HetCASL) allows mixing specifications written in different logics (using translations between the logics). It extends CASL only at the level of structuring constructs, by adding constructs for choosing the logic and translating specifications among logics. HetCASL is needed when combining specifications written in CASL with specifications written in its sublanguages and extensions. HetCASL also allows the integration of logics that are completely different from the CASL logic. This document provides a detailed definition of the HetCASL syntax and an informal description of the semantics, building on the existing CASL Summary.

ModalCASL extends CASL by modal operators. Syntax for ordinary modalities, multi-modal logics as well as term-modal logic (also covering dynamic logic) is provided. Specific modal logics can be obtained via restrictions to sublanguages. This document provides a detailed definition of the ModalCASL syntax and an informal description of the semantics, building on the existing CASL Summary.

This part of the CASL reference manual describes a library of elementary specifications called the Basic Datatypes. This library has been developed with two main purposes in mind: on the one hand, it provides the user with a handy set of off-the-shelf specifications to be used as building blocks in the same way as library functions in a programming language, thus avoiding continuous reinvention of the wheel. On the other hand, it serves as a large reservoir of example specifications that illustrate both the use of CASL at the level of basic and structured specifications.

We develop an equational definition of exception monads that characterizes Moggi's exception monad transformer. This axiomatization is then used to define an extension of previously described monad-independent computational logics by abnormal termination. Instantiating this generic formalism with the Java monad used in the LOOP project yields in particular the known Hoare calculi with abnormal termination and JML's method specifications; this opens up the possibility of extending these formalisms by hitherto missing computational features such as I/O and nondeterminism.

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. As the background formalism for these concepts, we use the logic of HasCASL, a higher-order language for functional specification and programming.

Petri nets and Algebraic High-Level Nets are well-known to model parallel and concurrent systems. In this paper, we introduce the concept of Algebraic Higher-Order Nets, which allow to have dynamical tokens like graphs or (ordinary low-level) Petri nets. For this purpose, we specify graphs and Petri nets in the higher-order algebraic specification language HasCASL such that graphs and Petri nets become first-class citizens, i.e. members of algebras (rather than algebras themselves). As an example, we model hospital therapeutic processes by a single higher-order net. Individual care plans for each patient are tokens modeled by low-level nets.

We provide a semantic basis for heterogeneous specifications that not only involve different logics, but also different kinds of translations between these. We show that Grothendieck institutions based on spans of (co)morphisms can serve as a unifying framework providing a simple but powerful semantics for heterogeneous specification.

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 specication of execution orders. We show that with this, object-based dynamic separation of duty, as well as other policies, can be adequately specied.

We introduce CoCASL as a simple coalgebraic extension of the algebraic specification language CASL. CoCASL allows the nested combination of algebraic datatypes and coalgebraic process types. We show that the well-known coalgebraic modal logic can be expressed in CoCASL. We present sufficient criteria for the existence of cofree models, also for several variants of nested cofree and free specifications. Moreover, we describe an extension of the existing proof support for CASL (in the shape of an encoding into higher-order logic) to CoCASL.

CASL is an expressive specification language that has been designed to supersede many existing algebraic specification languages and provide a standard. CASL consists of several layers, including basic (unstructured) specifications, structured specifications and architectural specifications (the latter are used to prescribe the structure of implementations). We describe an simplified version of the CASL syntax, semantics and proof calculus at each of these three layers and state the corresponding soundness and completeness theorems. The layers are orthogonal in the sense that the semantics of a given layer uses that of the previous layer as a "black box", and similarly for the proof calculi. In particular, this means that CASL can easily be adapted to other logical systems.

CoCASL, a recently developed coalgebraic extension of the algebraic specification language CASL, allows for modelling systems in terms of inductive datatypes as well as of co-inductive process types. Here, we demonstrate how to specify process algebras, namely CCS and CSP, within such an algebraic-coalgebraic framework. It turns out that CoCASL can deal with the fundamental concepts of process algebra in a natural way: The type system of communications, the syntax of processes and their structural operational semantics fit well in the algebraic world of CASL, while the additional coalgebraic constructs of CoCASL cover the various process equivalences (bisimulation, weak bisimulation, observational congruence, and trace equivalence) and provide fully abstract semantic domains. CoCASL hence becomes a meta-framework for studying the semantics and proof theory of reactive systems.

The development of programs in modern functional languages such as Haskell calls for a wide-spectrum specification formalism that supports the type system of such languages, in particular higher order types, type constructors, and polymorphism, and that contains a functional language as an executable subset in order to facilitate rapid prototyping. We lay out the design of HasCASL, a higher order extension of CASL that is geared towards precisely this purpose. Its semantics is tuned to allow program development by specification refinement, while at the same time staying close to the set-theoretic semantics of first order CASL. The number of primitive concepts in the logic has been kept as small as possible; advanced concepts, in particular general recursion, can be formulated within the language itself. This document provides a detailed definition of the HasCASL syntax and an informal description of the semantics, building on the existing CASL Summary.

Monads have been recognized by Moggi as an elegant device for dealing with stateful computation in functional programming languages. It is thus natural to develop a Hoare calculus for reasoning about computational monads. While this has previously been done only for the state monad, we here provide a generic, monad-independent approach, which applies also to further computational monads such as exceptions, input/output, and non-determinism. All this is formalized within the logic of HasCASL, a higher-order language for functional specification and programming. Combination of monadic features can be obtained by combining their loose specifications. As an application, we prove partial correctness of Dijkstra's nondeterministic version of Euclid's algorithm in a monad with nondeterministic dynamic references.

For the recently developed specification language CASL, there exist two different kinds of proof support: while HOL-CASL has its strength in proofs about specifications in-the-small, MAYA has been designed for management of proofs in (CASL) specifications in-the-large, within an evolutionary formal software development process involving changes of specifications. In this work, we discuss our integration of HOL-CASL and MAYA into a powerful system providing tool support for CASL, which will also serve as a basis for the integration of further proof tools.

The use of formal methods is propagated to increase the security and safety of developed software. However, the logical formalization of software systems is error-proned. As even the verification of small-sized industrial developments require several person months, specification errors revealed in late verification phases pose an incalculable risk for the overall project costs. Thus, an evolutionary formal development approach is absolutely indispensable in all applications so far, as it was hardly ever the case that the development steps were correctly designed in the first attempt. The search for formally correct software and the corresponding proofs is more like a formal reflection of partial developments rather than just a way to assure and prove more or less evident facts. The MAYA-system supports an evolutionary formal development as it allows the user to specify and verify his/her development and maintain and reuse the verification work already done when changing the specification. MAYA supports the use of various (structured) specification languages like CASL and VSE-SL to formalize the software development. Moreover, MAYA provides a generic interface to plugin additional parsers for the support of other specification languages.

In order to obtain a semantic foundation for heterogeneous specification, we extend Diaconescu's morphism-based Grothendieck institutions to the case of comorphisms. This is not just a dualization, because we obtain more general results, especially concerning amalgamation properties. We also introduce a proof calculus for structured heterogeneous specifications and study its soundness and completeness (where amalgamation properties play a role for obtaining the latter).

Development graphs are a tool for dealing with structured specifications in a formal program development in order to ease the management of change and reusing proofs. Often, different aspects of a software system have to be specified in different logics, since the construction of a huge logic covering all needed features would be too complex to be feasible. Therefore, we introduce em heterogeneous development graphs as a means to cope with heterogeneous specifications. We cover both the semantics and the proof theory of heterogeneous development graphs. A proof calculus can be obtained either by combining proof calculi for the individual logics, or by representing these in some ``universal'' logic like higher-order logic in a coherent way and then ``borrowing'' its calculus for the heterogeneous language.

We describe a way to make the static analysis for the in-the-large part of the Common Algebraic Specification Language (CASL) independent of the underlying logic that is used for specification in-the-small. The logic here is formalized as an institution with some extra components. Following the institution independent semantics of CASL in-the-large, we thus get an institution independent static analysis for CASL in-the-large. With this, it is possible to re-use the CASL static analysis for extensions of CASL, or even completely different logics. One only has to provide a static analysis for specifications in-the-small for the given logic. This then can be plugged into the generic static analysis for CASL in-the-large.

In this work, we consider various specification specification languages and their relation to CASL, the recently developed Common Algebraic Specification Language. In particular, we consider the languages Larch, OBJ3, ACT, ASF, and HEP-theories. We also consider various sublanguages of CASL that more or less directly correspond to these. All these languages are translated to an appropriate sublanguage of CASL. The translation considers only the level of specification in-the-small: the logics underlying the languages are formalized as institutions, and representations among the institutions are developed. The institution representations concern on one hand the translation of the CASL institution (and some of its subinstitutions) to simpler subinstitutions. Given a theorem proving tool for such a simpler subinstitutions, with the help of such a representation, it can also be used for the more complex institution. Thus, first-order theorem provers or conditional term rewriting tools become usable for CASL. On the other hand, we set up institution representations between the underlying institution of any of the abovementioned specification languages and an appropriate subinstitution of CASL. This allows to take libraries and case studies that have been developed for other languages and re-use them in CASL.

This note provides a style guide how to write specifications in CASL. The guidelines presented here were developed writing the note "Basic Datatypes in CASL" [4]. Thus they have proven to be useful in practice. The aim of this note is twofold: on the one hand it documents the methodology behind the "Basic Datatypes in CASL" [4] and thus helps to understand the design decision behind them. On the other hand the here presented "Methodological Guidelines" may be useful as a starting point for other methodologies.

The development of programs in modern functional languages such as Haskell calls for a wide-spectrum specification formalism that supports the type system of such languages, in particular higher order types, type constructors, and parametric polymorphism, and that contains a functional language as an executable subset in order to facilitate rapid prototyping. We lay out the design of HasCASL, a higher order extension of the algebraic specification language CASL that is geared towards precisely this purpose. Its semantics is tuned to allow program development by specification refinement, while at the same time staying close to the set-theoretic semantics of first order CASL. The number of primitive concepts in the logic has been kept as small as possible; we demonstrate how various extensions to the logic, in particular general recursion, can be formulated within the language itself.

Development graphs are a tool for dealing with structured specifications in a way easing management of change and reusing proofs. In this work, we extend development graphs with hiding. Hiding is a particularly difficult to realize operation, since it does not admit such a good decomposition of the involved specifications as other structuring operations do. We develop both a semantics and proof rules for development graphs with hiding. The rules are proven to be sound, and also complete relative to an oracle for conservative extensions. We also show that an absolute complete set of rules cannot exist. The whole framework is developed in a way independent of the underlying logical system.

We construct a representation of the institution of the algebraic specification language CASL in an institution called enriched CASL. Enriched CASL satisfies the amalgamation property, which fails in the CASL institution, as well as its converse. Thus, the previously suggested institution-independent semantics of architectural specifications is actually applicable to CASL. Moreover, a variety of results for institutions with amalgamation, such as computation of normal forms and theorem proving for structured specifications, can now be used for CASL.

We present a semantics for architectural specifications in CASL, including an extended static analysis compatible with model-theoretic requirements. The main obstacle here is the lack of amalgamation for CASL models. To circumvent this problem, we extend the CASL logic by introducing enriched signatures, where subsort embeddings form a category rather than just a preorder. The extended model functor has amalgamation, which makes it possible to express the amalgamability conditions in the semantic rules in static terms. Using these concepts, we develop the semantics at various levels in an institution-independent fashion. Concretizing to the CASL institution, we discuss a calculus for discharging the static amalgamation conditions. These are in general undecidable, but can be dealt with by approximative algorithms in all practically relevant cases.

We develop a notion of institution with symbols and a kernel language for writing structured specifications in CASL. This kernel language has a semantics in an arbitrary but fixed institution with symbols. Compared with other institution-independent kernel languages, the advantage is that translations, hidings etc. can be written in a symbol-oriented way (rather than being based on signature morphisms as primitive notion), while still being institution-independent. The semantics of the kernel language has been used as the basis for the semantics of structured specifications in CASL.

CASL is a specification language combining first-order logic, partiality and subsorting. This paper generalizes the CASL logic to also include higher-order functions and predicates. The logic is presented in a modular step-by-step reduction: the logic is defined in terms of a generalized subsorted partial logic which in turn is defined in terms of many-sorted partial first-order logic. A new notion of homomorphism is introduced to meet the need to get a faithful embedding of first-order CASL into higher-order CASL. Finally, it is discussed how a proof calculus for the proposed logic can be developed.

CASL, the common algebraic specification language, has been developed as a language that subsumes many previous algebraic specification frameworks and also provides tool interoperability. CASL is a complex language with a complete formal semantics. It is therefore a challenge to build good tools for CASL. In this work, we present and discuss the Bremen HOL-CASL system, which provides parsing, static checking, conversion to LaTeX and theorem proving for CASL specifications. To make tool construction manageable, we have followed some guidelines: re-use of existing tools, interoperability of tools developed at different sites, and construction of generic tools that can be used for several languages. We describe the structure of and the experiences with our tool and discuss how the guidelines work in practice.

We emphasize the role of consistency in the development process and in particular the need to write consistent design specifications. CASL takes an axiomatic approach, as opposed to model-oriented approaches like VDM or Z. This means that it is possible to specify loose requirements at a very high level. Moreover, it is possible to decribe abstract data types only w.r.t. their properties, without giving any intended implementation.

We present a weak theory of the real numbers in the first order specification language CASL. The aim is to provide a datatype for practical purposes, including the central notions and results of basic analysis. Our theory captures for instance e and pi, as well as the trigonometric and other standard functions. Concepts such as continuity, differentiation and integration are shown to be definable and tractable in this setting; Newton's Method is presented as an example of a numerical application. Finally, we provide a proper connection between the specified datatype and specifications of the real numbers in higher order logic and various set theories.

The problem of combining logics has been attracting much attention. Among the most interesting mechanisms, fibring deserves close attention. Herein, we extend our earlier work to logics with variables, terms and binding operators. For example, in order to obtain first order temporal logic by fibring first order logic and propositional temporal logic. Our main goal is to provide a categorial characterization of both proof and model theoretic fibring of such logics. Following the approach proposed in earlier work, we define free unconstrained fibring as a coproduct and constrained (by sharing of symbols) fibring as a cocartesian lifting in the appropriate categories (of Hilbert calculi and interpretation systems). Furthermore, we establish that soundness is preserved by the construction and that completeness is not always preserved. The extension of the approach to logics with variables, terms and binding operators is by no means trivial, at both proof and model theoretic levels. At the level of the Hilbert calculi, we need an abstract solution to deal with the meta requirements in inference rules related to binding (such as, term t is free for variable x in formula F) having in mind that inference rules should be preserved by morphisms of Hilbert calculi. We are able to do so by dealing with binding on the terminal signature where binding operators of the same kind are confused. Indeed, we consider two quite different kinds of binding operators: those that bind variables (like quantifiers and lambda abstraction) and those that bind flexible symbols (like modal operators). At the level of the interpretation systems, the main problem was to cope with the different semantics of rigid and flexible symbols at the envisaged degree of generality. In this paper, we assume that values of variables are rigid. This assumption makes the semantics simpler but is the key reason for not achieving preservation of completeness. Indeed, by fibring first order logic and propositional temporal logic we obtain a logic where the Barcan formulae are valid but are not obtained from the axioms. The proposed categorial approach was essential in finding a suitably abstract treatment of binding. Furthermore, for the simpler case of propositional logics, the categorial imperative was very helpful in fine tuning the envisaged semantics of fibring with explicit models and satisfaction and in establishing the technical lemmata for preservation of soundness. We compare our semantics to model-theoretic parchments that are also defined in a categorial way.

The focus of this Chapter is the incremental presentation of partial first-order logic, seen as a powerful framework where the specification of most data types can be directly represented in the most natural way. Both model theory and logical deduction are described in full detail. Alternatives to partiality, like (variants of) error algebras and order-sortedness are also discussed, showing their uses and limitations. Moreover, both the total and the partial (positive) conditional fragment are investigated in detail, and in particular the existence of initial (free) models for such restricted logical paradigms is proved. Some more powerful algebraic frameworks are sketched at the end.

We translate OBJ3 to CASL. At the level of basic specifications, we set up several institution representations between the underlying institutions. They correspond to different methodological views of OBJ3. The translations can be the basis for automated tools translating OBJ3 to CASL.

Real (and, to some degree, also complex) numbers should be a part of the CASL standard library, since they occur in many applications and programming languages. In this note, we address the specification of real and complex numbers at two levels: at the mathematical level and at the computer representation level. [RM99a][RM99b] can be seen as complementary notes, since they contain basic datatypes resp. describe annotations and syntax extensions we frequently use here.

In this note, we propose a set of (parsing and semantic) annotations and some syntax extensions for literals in CASL. The parsing annotations (for precedences and associativity) and syntax extensions (for lists, characters, strings, and numbers) influence the parsing of CASL specifications. The semantic annotations express some requirements on extensions, namely to be conservative or definitional. [RM99][MR99] can be seen as complementary notes, since they contain a rich fund of specifications using the annotations and syntax extensions.

We present a proposal for the design of the higher-order extension of CASL. For each design step, we have tried to find the best of several possible alternatives, give a motivation for the preferred alternative and argue why the other alternatives are not taken. This note discusses function spaces, product types, partial functions, predicates, subsorting, signature morphisms and -abstraction. A forthcoming note will be devoted to polymorphism, type constructors and dependent types. A companion note, replacing L-2, will explain the formal details of the proposal made in this note.

CASL is a specification language combining first-order logic, partiality and subsorting. This paper generalizes the CASL logic to higher-order functions and predicates. The logic is presented in a modular step-by-step reduction. Several possible design alternatives are discussed in the light of the need to get a faithful embedding of first-order CASL into higher-order CASL.

We prove cocompleteness of the category of CASL signatures, of monotone signatures, of strongly regular signatures and of strongly locally filtered signatures. This shows that using these signature categories is compatible with a pushout or colimit based module system.

The paper addresses important problems of building complex logical systems and their representations in universal logics in a systematic way. We adopt the model-theoretic view of logic as captured in the notions of institution and of parchment (an algebraic way of presenting institutions). We propose a new, modified notion of parchment together with parchment morphisms and representations. In contrast to the original parchment definition and our earlier work, in model-theoretic parchments introduced here the universal semantic structure is distributed over individual signatures and models. We lift formal properties of the categories of institutions and their representations to this level: the category of model-theoretic parchments is complete, and their representations may be put together using categorical limits as well. However, model-theoretic parchments provide a more adequate framework for systematic combination of logical systems than institutions. We indicate how the necessary invention for combination of various logical features may be introduced either on an ad hoc basis or via representations in a universal logic.

We argue that tools for parsing and static semantic analysis of CASL specifications should be usable as a front-end for tools that act only only well-formed specifications (like theorem provers, rewriters). Therefore, standard annotations for abstract syntax trees containing the static semantic (and other) information are needed. A proposal for what these annotations should contain is made. Note that this is to some degree independent of the question which interchange format to choose. The note was revised according to the discussion on the CoFI Tools meeting in Lisbon at April 3rd 1998.

We define two sublanguages of CASL that can be easily mapped to functional programs. One of them allows to specify arbitrary partial recursive functions, the other one is restricted to total recursive functions.

The paper addresses important problems of building complex logical systems and their representations in universal logics in a systematic way. Following Goguen and Burstall, we adopt the model-theoretic view of logic as captured in the notion of institution and of parchment (a certain algebraic way of presenting institutions). We propose a modified notion of parchment together with a notion of parchment morphism and representation, respectively. We lift formal properties of the categories of institutions and their representations to this level: the category of parchments is complete, and parchment representations may be put together using categorical limits as well. However, parchments provide a more adequate framework for systematic combination of logical systems than institutions. We indicate how the necessary invention for proper combination of various logical features may be introduced either on an ad hoc basis (when putting parchments together using limits in the category of parchments) or via representations in a universal logic (when parchment combination is driven by their representations).

We define various sublanguages of CASL by identifying a number of orthogonal features. Each of these features can be included or left out in a sublanguage. This leads to a concise notation for sublanguages. The sublanguages can be identified purely syntactically, thus tools can determine to which sublanguages a particular specification belongs. Two graphs show relations among the sublanguages. The relation of the sublanguages to other specification languages is addressed briefly.

There is a variety of specification languages for the formal specification and development of correct software systems. They differ in purpose, expressiveness, level of abstraction (requirement, design, implementation), notation, available tools etc. It has been argued that one should not construct one universal all-purpose specification language (which would be very clumsy), but rather relate different languages based on different logical frameworks. Thus there is a need for a meta-notion of logical framework and a notion of map between logical frameworks in order to relate them. This leads to a category of logical frameworks. In the literature, there are described not only one, but many categories of logical frameworks: institutions with maps of institutions, specification frames, institutions with simulations, pre-institutions with transformations, institutional frames, pi- and tau-institutions, institutions with contexts, etc. Some of these were related by Maura Cerioli in her thesis. Thus, there are quite different types of logical frameworks, and each type of logical framework (together with a type of arrow between logical frameworks) leads to a new category of logical frameworks. The purpose of the morphisms in the above mentioned categories of logical frameworks is that of encoding, or representing one logical framework into another one. With this, one can # write heterogeneous specifications with components written in different logical frameworks, # switch between different types of logical framework by borrowing missing logical structure along maps, e.g. endow an institution with an entailment relation and a proof calculus, # compare expressiveness of different logical frameworks (within one type of logical framework, of course), # use logical framework independent specification language constructs being preserved by maps. But if we do not follow some neat structuring principle in the meta theory (i. e. types of logical framework), there is the danger to end in the same Babylonian realm of different languages as in the object theories (i. e. different logical frameworks). After all, the meta theory should help us to structure and compare the object theories, and not to produce the same diversity of notions! The main argument for having several types of logical framework is the distinction between proof theory and model theory. Except for the case of specification frames, this was examined by Cerioli and Meseguer. A second argument is the observation that different degrees of more or less good representation of one logical framework in another are possible. Many examples require some intermediate notion between map of institutions and map of specification frames. This has to do with the distinction of signatures and sentences in an institution. This distinction is necessary (using just specification frames abandons the notion of sentence and of theorem proving), but there are many choices for what should be included into the signature part, and what into the sentences. Therefore the need of types of arrow which may mix up this distinction. In this paper we argue that these different types of arrow can be generated by one basic type of arrow and monadic constructions on categories of logical frameworks, with the effect of automatically having functors relating the new categories of logical frameworks with the old ones.

We examine a variety of liberal logical frameworks of partial algebras. Therefore we use simple, conjunctive and weak embeddings of institutions which preserve model categories and may map sentences to sentences, finite sets of sentences, or theory extensions using unique-existential quantifiers, respectively. They faithfully represent theories, model categories, theory morphisms, colimit of theories, reducts etc. Moreover, along simple and conjunctive embeddings, theorem provers can be re-used in a way that soundness and completeness is preserved. Our main result states the equivalence of all the logical frameworks with respect to weak embeddability. This gives us compilers between all frameworks. Thus it is a chance to unify the different branches of specification using liberal partial logics. This is important for reaching the goal of formal interoperability of different specification languages for software development. With formal interoperability, a specification can contain parts written in different logical frameworks using a multiparadigm specification language, and one can re-use tools which are available for one framework also for other frameworks.

For the specification of abstract data types, quite a number of logical systems have been developed. In this work, we will try to give an overview over this variety. As a prerequisite, we first study notions of representation and embedding between logical systems, which are formalized as institutions here. Different kinds of representations will lead to a looser or tighter connection of the institutions, with more or less good possibilities of faithfully embedding the semantics and of re-using proof support. In the second part, we then perform a detailed ``empirical'' study of the relations among various well-known institutions of total, order-sorted and partial algebras and first-order structures (all with Horn style, i.e. universally quantified conditional, axioms). We thus obtain a graph of institutions, with different kinds of edges according to the different kinds of representations between institutions studied in the first part. We also prove some separation results, leading to a hierarchy of institutions, which in turn naturally leads to five subgraphs of the above graph of institutions. They correspond to five different levels of expressiveness in the hierarchy, which can be characterized by different kinds of conditional generation principles. We introduce a systematic notation for institutions of total, order-sorted and partial algebras and first-order structures. The notation closely follows the combination of features that are present in the respective institution. This raises the question whether these combinations of features can be made mathematically precise in some way. In the third part, we therefore study the combination of institutions with the help of so-called parchments (which are certain algebraic presentations of institutions) and parchment morphisms.

It has been widely accepted that partial algebras are an important semantical basis for the specification of software systems. The motivation for this work grew out of a systematic study of institutions capturing partiality in different ways. When constructing an institution of partial algebras, one usually redefines every concept for total algebras from scratch, and generalizes it to the partial case. This may become a tedious process. Moreover, often one has to choose between different generalizations, but the design decisions are scattered all over the definitions. In this work, we try to systematize the combination of different institutions. Goguen and Burstall have argued that combinations can be done via (co-)limits. Now the category of institutions and institution morphisms is complete, but limits in this category put together different concepts only without true interaction. Therefore, we move to Goguen's and Burstall's parchments , which allow defining institutions using # initial algebra semantics for the definition of sentence syntax, # a special signature for the definition of models and # a semantical algebra for the definition of semantical evaluation of sentences. We introduce a notion of morphism between parchments, which allows us to combine different concepts with interaction, using limits. Now there is the problem that, in many cases, the limit contains unwanted ``junk'' truth values and thus the space of truth values need not be preserved. This problem can be solved by imposing a congruence relation on the semantical algebra of the limit. The congruence can usually be generated from a small number of axioms, which state how different concepts interact. Thus, we cannot expect a combination to be done automatically (as in the case of combining theories), but we have to use a two-step semi-automatic method: first specify the components to be combined, and then specify interaction of concepts. These ideas are illustrated by generalizing several concepts from total to partial algebras. The role of the congruence relation here is to decide whether we want a two- or three-valued logic and to determine which concept of equality to use.

In this paper, we investigate several logical frameworks whose expressiveness lies between Conditional Equational Logic and Horn Clause Logic. The main result deals with the PART-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 allow to measure the equivalence and difference between institutions.

A hierarchy of institutions ranging form equational logic to partial conditional existence-equational logic with relations is built. The different levels of the hierarchy can be separated by properties of parameterized abstract data types. A sample parameterized abstract data type, bounded stacks, is located within the hierarchy.

We examine four specification methods with increasing expressiveness. Parameterized recursion theory allows to characterize the power of parameterization in the methods, using a computational model based on Moschovakis' search computability. The four specification methods can be characterized by four different notions of semicomputable parameterized abstract data type, which differ in the availability of the parameter algebra and of nondeterminism. These characterizations further lead to different algebraic properties of specifiable PADTs. Together with example PADTs, they enable us to prove a hierarchy theorem. Given a sample PADT, the algebraic properties help to find out the lowest position (= most restricted method) in the hierarchy usable to specify it. This is important because the available tools may become weaker, if we choose a too general method.