Tutorials
Distributed Ontology Language
given by Oliver Kutz
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, entityrelationship diagrams and object role modelling provide bridges from ontology modelling to applications, e.g. in software engineering and databases. Also in model-driven engineering, there is a diversity of diagrams: UML consists of 15 different diagram types, and SysML provides further types. Finally, in software and hardware specifcation, a variety of formalisms are in use, like Z, VDM, first-order logic, temporal logic etc.
Another diversity appears at the level of ontology, model and specification modularity and relations among ontologies, specifications and models. There is ontology matching and alignment, module extraction, interpolation, ontologies linked by bridges, interpretation and refinement, and combination of ontologies, models and specifications. The Distributed Ontology, Modeling and Specification Language (DOL) aims at providing a unified metalanguage for handling this diversity. In particular, DOL provides constructs for
- "as-is" use of ontologies, models and specifications (OMS) formulated (as a logical theory) in a specific ontology, modelling or specification language,
- OMS formalised in heterogeneous logics,
- modular OMS,
- mappings between OMS,
- networks of OMS, and
- queries.
The final DOL specification was submitted as a standard to the Object Management Group (OMG) in early 2015. This course will introduce syntax and semantics of the DOL language, discuss a number of modelling and interoperability problems that can be addressed with DOL, and introduce to the use of available DOL tools.
An Introduction to Coalgebraic Logic
given by Dirk Pattinson
The tutorial gives an overview of modal logic at the intersection of computer science, philosophy, logic, and artificial intelligence. The emphasis is on the broad spectrum of semantic and syntactic variation found in modal logics, and on unifying perspectives on this variety. The basic duality between algebra and coalgebra, and therfore coalgebraic logic, plays a key role. The course is targeted at graduate students, assuming basic familiarity with naive set theory and propositional logic.
We understand modal logics as extensions of propositional logic with additional operators. The course discusses a number of examples and focus on
duality as bridge between the syntactic and the semantic viewpoint. We then present the basic decision problems in modal logic and discuss backwards proof search in sequent calculi. We then elaborate on the combination of modal
logics, extensions of modal logics with nominals, the global modality, and fixpoints, and embed modal logic into the wider context of the philosophical, logical and computational landscape.
Institutions: an abstract framework for foundations of software specification and logic
given by Andrzej Tarlecki
One goal of this series of talks is to show some examples where the use of category theory, via the theory of institutions, led to beautiful, general and generic results, applicable in many different contexts, and to a better understanding of some standard classical results and ideas from the theory of specifications and from mathematical logic.
The concept of an institutions uses the language of category theory to offer a simple formalization of the notion of a logical system, where sentences and semantic structures are abstract objects linked by a satisfaction relation, classified by (abstract) signatures. The key idea is to endow the collection of signatures with a structure of a category, together with (covariant) translations of sentences and (contravariant) reducts of semantic structures induced by signature morphisms in a way that preserves satisfaction. Nearly all (if not quite all) logical systems fit such an institutional mould.
An ambitious research programme, going back to the original development of the notion of institution in the 1980s, is to mimic developments that classically concern or rely on a particular logical system within an arbitrary institution, perhaps subject to some further requirements. In this way, we arrive at general results that apply to many logical systems and capture a better understanding of the essence of many classical results and ideas.
In this series of talks I will present some bits and pieces of the theory of institutions, starting from the basics, and going on to sample ideas and results from institutional foundations of software specification and abstract model theory.
