The interdisciplinary project DIREGA aims to analyse the joint application of linguistic, symbolic, and sub-symbolic AI techniques to German register law. This analysis is based on a dataset consisting of all past applications, related documents, and decisions of German register courts in the Free State of Bavaria. Corpus queries and sub-symbolic AI methods will be used for information extraction which then instantiate facts for the symbolic reasoning pipeline based on a manual formalization of the relevant laws. The goal is to build a prototypical implementation checking register applications and providing a detailed explanation for acceptance (or rejection) to aid legal professionals such as notaries in drafting and reviewing such documents.

To cater to the increasingly diverse student bodies, higher education has to personalize education. In times of stagnant educational budgets and staffing problems, this can only be achieved via adaptive, interactive learning support services. In this paper we show how these can be generated by modeling the domain, the learner competencies, and the rhetoric and didactic relations among learning objects, re-using existing technologies and systems of mathematical knowledge management.

Abstract The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented great theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution, and our experiences will prove valuable to others undertaking such efforts.

Among the standard stages of the engineering design process, the principle solution can be regarded as an analogue of the design specification, fixing the way the final product works. It is usually constructed as an abstract sketch where the functional parts of the product are identified, and geometric and topological constraints are formulated. Here, we outline a semantic approach where the principle solution is annotated with ontological assertions, thus making the intended requirements explicit and available for further machine processing; this includes the automated detection of design errors in the final CAD model, making additional use of a background ontology of engineering knowledge.

ldquoSemantic technologiesrdquo are touted as the next big wave in educational technology and as the solution to many problems in this arena. Interdisciplinary work between the fields of knowledge management (KM) and educational technology (ET) is booming. But the crop of actual systems and semantically enhanced learning objects is still meager, maybe because KM and EL are lacking a consensus on the underlying notions, e.g., of ldquosemantics,rdquo yielding specific problems in their interplay. In this paper, we look at semantic educational technologies and draw conclusions for their approach in KM. In particular, we (re)evaluate the notions of semantics, knowledge, and learning; their role for learning materials in ET; and how they interact with the contexts involved in the learning/teaching process. Based on this, we distill a list of conditions the underlying knowledge representation format must fulfil to support these. As these conditions are still rather abstract, we show how they can be realized in a concrete language design, taking in our open mathematical documents format OMDoc as a point of departure.

Abstract. In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-order calculi with respect to these model classes.

In this paper we revisit Pustejovsky's proposal to treat ontologically complex word meaning by so-called dotted pairs. We use a higher-order feature logic based on Ohori's record λ-calculus to model the semantics of words like book and library, in particular their behavior in the context of quantification and cardinality statements.

Abstract. The capabilities of a automated theorem prover's interface are essential for the effective use of (interactive) proof systems. L Ω UI is the multi-modal interface that combines several features: a graphical display of information in a proof graph, a selective term browser with hypertext facilities, proof and proof plan presentation in natural language, and an editor for adding and maintaining the knowledge base. L Ω UI is realized in an agent-based client-server architecture and implemented in the concurrent constraint programming language Oz.

In this paper, we show that Higher-Order Coloured Unification - a form of unification developed for automated theorem proving - provides a general theory for modeling the interface between the interpretation process and other sources of linguistic, non semantic information. In particular, it provides the general theory for the Primary Occurrence Restriction which (Dalrymple et al., 1991)'s analysis called for.