Author name cluster

Till Mossakowski

Possible papers associated with this exact author name in Arrow. This page groups case-insensitive exact name matches and is not a full identity disambiguation profile.

21 papers

2 author rows

NeSy Conference 2025 Conference Paper

mULLER: A Modular Monad-Based Semantics of the Neurosymbolic ULLER Framework

Daniel Romero Schellhorn
Till Mossakowski

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

Details

NeSy Conference 2024 Conference Paper

A Fuzzy Loss for Ontology Classification

Simon Flügel
Martin Glauer
Till Mossakowski
Fabian Neuhaus

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

Details

NeSy Conference 2022 Conference Paper

Modular Design Patterns for Neural-symbolic Integration: Refinement and Combination

Till Mossakowski

We formalise some aspects of the neural-symbol design patterns of van Bekkum et al. , such that we can formally define notions of refinement of patterns, as well as modular combination of larger patterns from smaller building blocks. These formal notions have been implemented in the heterogeneous tool set (Hets), such that patterns and refinements can be checked for well-formedness, and combinations can be computed.

Details

FLAP Journal 2019 Journal Article

Towards Fuzzy Neural Conceptors.

Till Mossakowski
Razvan Diaconescu
Martin Glauer

Conceptors are an approach to neuro-symbolic integration based on recurrent neural networks. Jaeger has introduced two-valued logics for conceptors. We observe that conceptors are essentially fuzzy in nature, and hence develop a fuzzy subconceptor relation and a fuzzy logic for conceptors.

Details

TCS Journal 2018 Journal Article

Partial pushout semantics of generics in DOL

Till Mossakowski
Bernd Krieg-Brückner

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.

Details DOI

IJCAI Conference 2017 Conference Paper

Relations Between Spatial Calculi About Directions and Orientations (Extended Abstract)

Till Mossakowski
Reinhard Moratz

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

PDF Details

JAIR Journal 2015 Journal Article

Relations Between Spatial Calculi About Directions and Orientations

Till Mossakowski
Reinhard Moratz

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

PDF Details DOI

IJCAI Conference 2013 Conference Paper

Three Semantics for the Core of the Distributed Ontology Language (Extended Abstract)

Till Mossakowski
Christoph Lange
Oliver Kutz

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 uniﬁed framework for (1) ontologies formalized in heterogeneous logics, (2) modular ontologies, (3) links between ontologies, and (4) 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.

PDF Details DOI

AIJ Journal 2012 Journal Article

Qualitative reasoning about relative direction of oriented points

Till Mossakowski
Reinhard Moratz

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 very useful for solving spatial navigation tasks. It turns out that scalable granularity is useful in these navigation tasks.

Details DOI

AIJ Journal 2011 Journal Article

A condensed semantics for qualitative spatial reasoning about oriented straight line segments

Reinhard Moratz
Dominik Lücke
Till Mossakowski

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.

Details DOI

AAAI Conference 2011 Conference Paper

A Modular Consistency Proof for DOLCE

Oliver Kutz
Till Mossakowski

We propose a novel technique for proving the consistency of large, complex and heterogeneous theories for which ‘standard’ automated reasoning methods are considered insufﬁcient. In particular, we exemplify the applicability of the method by establishing the consistency of the foundational ontology DOLCE, a large, ﬁrst-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 speciﬁcation of DOLCE which reﬂects the way models of the theory can be built, (ii) an automated veriﬁcation of the amalgamability conditions, and (iii) a (partially automated) series of relative consistency proofs.

PDF Details

TCS Journal 2009 Journal Article

HasCasl: Integrated higher-order specification and program development

Lutz Schröder
Till Mossakowski

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.

Details DOI

ECAI Conference 2008 Conference Paper

Conservativity in Structured Ontologies

Oliver Kutz
Till Mossakowski

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 &Escr; -connections.

Details

TCS Journal 2006 Journal Article

A coalgebraic approach to the semantics of the ambient calculus

Daniel Hausmann
Till Mossakowski
Lutz Schröder

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.

Details DOI

MFCS Conference 2006 Conference Paper

Completeness of Global Evaluation Logic

Sergey Goncharov 0001
Lutz Schröder
Till Mossakowski

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

Details

TCS Journal 2005 Journal Article

Amalgamation in the semantics of CASL

Lutz Schröder
Till Mossakowski
Andrzej Tarlecki
Bartek Klin
Piotr Hoffman

We present a semantics for architectural specifications in the Common Algebraic Specification Language (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.

Details DOI

TIME Conference 2003 Conference Paper

A temporal-logic extension of role-based access control covering dynamic separation of duties

Till Mossakowski
Michael Drouineaud
Karsten Sohr

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

Details

MFCS Conference 2002 Conference Paper

Comorphism-Based Grothendieck Logics

Till Mossakowski

Abstract 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 rôle for obtaining the latter).

Details

TCS Journal 2002 Journal Article

Relating CASL with other specification languages: the institution level

Till Mossakowski

In this work, we investigate various specification languages and their relation to CASL, the recently developed Common Algebraic Specification Language. In particular, we consider the languages Larch, OBJ3 and functional CafeOBJ, ACT ONE, ASF, and HEP-theories, as well as various sublanguages of CASL. All these languages are translated to an appropriate sublanguage of CASL. The translation mainly concerns the level of specification in-the-small: the logics underlying the languages are formalized as institutions, and representations among the institutions are developed. However, it is also considered how these translations interact with specification in-the-large. Thus, we obtain, on the one hand, translations of any of the above-mentioned specification languages to an appropriate sublanguage of CASL. This allows us to take libraries and case studies that have been developed for other languages and re-use them in CASL. On the other hand, we set up institution representations going from the CASL institution (and some of its subinstitutions) to simpler subinstitutions. Given a theorem proving tool for such a simpler subinstitution, with the help of a representation, it can also be used for a more complex institution. Thus, first-order theorem provers and conditional term rewriting tools become usable for CASL.

Details DOI

MFCS Conference 2001 Conference Paper

Checking Amalgamability Conditions for C ASL Architectural Specifications

Bartek Klin
Piotr Hoffman
Andrzej Tarlecki
Lutz Schröder
Till Mossakowski

Abstract scC ASL, a specification formalism developed recently by the CoFI group, offers architectural specifications as a way to describe how simpler modules can be used to construct more complex ones. The semantics for C asl architectural specifications formulates static amalgamation conditions as a prerequisite for such constructions to be well-formed. These are non-trivial in the presence of subsorts due to the failure of the amalgamation property for the C ASL institution. We show that indeed the static amalgamation conditions for C ASL are undecidable in general. However, we identify a number of practically relevant special cases where the problem becomes decidable and analyze its complexity there. In cases where the result turns out to be PSPACE -hard, we discuss further restrictions under which polynomial algorithms become available. All this underlies the static analysis as implemented in the C ASL tool set.

Details

CSL Conference 1996 Conference Paper

Equivalences among Various Logical Frameworks of Partial Algebras

Till Mossakowski

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

Details