Michael Kohlhase

LFMTP Workshop 2019 Workshop Paper

GF + MMT = GLF - From Language to Semantics through LF

• Michael Kohlhase
• Jan Frederik Schaefer

These days, vast amounts of knowledge are available online, most of it in written form. Search engines help us access this knowledge, but aggregating, relating and reasoning with it is still a predominantly human effort. One of the key challenges for automated reasoning based on natural-language texts is the need to extract meaning (semantics) from texts. Natural language understanding (NLU) systems describe the conversion from a set of natural language utterances to terms in a particular logic. Tools for the co-development of grammar and target logic are currently largely missing. We will describe the Grammatical Logical Framework (GLF), a combination of two existing frameworks, in which large parts of a symbolic, rule-based NLU system can be developed and implemented: the Grammatical Framework (GF) and MMT. GF is a tool for syntactic analysis, generation, and translation with complex natural language grammars and MMT can be used to specify logical systems and to represent knowledge in them. Combining these tools is possible, because they are based on compatible logical frameworks: Martin-L\"of type theory and LF. The flexibility of logical frameworks is needed, as NLU research has not settled on a particular target logic for meaning representation. Instead, new logics are developed all the time to handle various language phenomena. GLF allows users to develop the logic and the language parsing components in parallel, and to connect them for experimentation with the entire pipeline.

I&C Journal 2013 Journal Article

A scalable module system

• Florian Rabe
• Michael Kohlhase

Symbolic and logic computation systems ranging from computer algebra systems to theorem provers are finding their way into science, technology, mathematics and engineering. But such systems rely on explicitly or implicitly represented mathematical knowledge that needs to be managed to use such systems effectively. While mathematical knowledge management (MKM) “in the small” is well-studied, scaling up to large, highly interconnected corpora remains difficult. We hold that in order to realize MKM “in the large”, we need representation languages and software architectures that are designed systematically with large-scale processing in mind. Therefore, we have designed and implemented the Mmt language – a module system for mathematical theories. Mmt is designed as the simplest possible language that combines a module system, a foundationally uncommitted formal semantics, and web-scalable implementations. Due to a careful choice of representational primitives, Mmt allows us to integrate existing representation languages for formal mathematical knowledge in a simple, scalable formalism. In particular, Mmt abstracts from the underlying mathematical and logical foundations so that it can serve as a standardized representation format for a formal digital library. Moreover, Mmt systematically separates logic-dependent and logic-independent concerns so that it can serve as an interface layer between computation systems and MKM systems.

IJCAI Conference 1997 Conference Paper

Computing Parallelism in Discourse

• Claire Gardent
• Michael Kohlhase

Although much has been said about parallelism in discourse, a formal, computational theory of parallelism structure is still outstanding. In this paper, we present a theory which given two parallel utterances predicts which are the parallel elements. The theory consists of a sorted, higher-order abductive calculus and we show that it reconciles the insights of discourse theories of parallelism with those of Higher-Order Unification approaches to discourse semantics, thereby providing a natural framework in which to capture the effect of parallelism on discourse semantics.

ECAI Conference 1996 Conference Paper

A Resolution Calculus for Presuppositions

• Manfred Kerber
• Michael Kohlhase

LPAR Conference 1992 Conference Paper

Unification in Order-Sorted Type Theory

• Michael Kohlhase

Abstract The introduction of sorts to first-order automated deduction has brought a considerable gain in efficiency by reducing the search space. It is therefore promising to treat sorts in higher order theorem proving as well, in order to achieve a similar gain. In this paper we develop a sorted version of type theory; we extend the syntax and semantics of simple type theory by a higher order sort concept that includes term declarations. In our system the partial ordering on the base sorts induces a partial ordering on the higher types by covariance in the rangesort and the natural inclusion of base function sorts. We present a set of transformations for sorted (pre-) unification and prove the nondeterministic completeness of the algorithm induced by these transformations.