Semantic annotations enable services that make the knowledge in documents more accessible. In the case of ALeA, an adaptive learning assistant we use as a case study, they enable, for example, guided tours and practice problems tailored to the learner's competencies. However, the cost of semantic authoring is substantial and tool support is limited. In this paper we discuss the nature of the semantic authoring task and argue that, while sharing aspects of both classical (informal) authoring and formal authoring, it is a task of its own that needs special editing support facilities. We present and evaluate a simple utility that supports the process of annotating technical terms with semantic references to a flexiformal content commons and increases annotation productivity by almost an order of magnitude.
The effort required for maintaining large libraries of formal mathematics is quite substantial. In this work, we exploit structural similarity to alleviate the burden of maintenance, investigating two main problems: First, we present a general framework for detecting duplicates in large libraries of formal mathematics, combining surface-level syntax, document markup, and the underlying formulae. For scalability, we generate potentially matching candidates with a discriminator-based approach. On Isabelle/HOL, our method maintains perfect precision up to a similarity threshold of 0.95. Secondly, we address the issue of out-of-place auxiliary lemmas that are frequently created during development of indepth formalizations. We propose a community detection approach on the underlying dependency graph of formal entities, which finds co-located lemmas that have similar link patterns. For a dataset of lemmas moved during Isabelle development, the correct location is in the top 6 neighborhoods suggested by our approach on average (median).
During formalization – e.g. of Mathematics – we have to take many decisions that informal mathematics leaves (and can leave) open. In particular, often there are multiple isomorphic ways of formalizing a set of axioms between which mathematicians can switch seamlessly. But this can impede beginners from fully understanding a domain, and it has proved difficult to mimic the same seamlessness in formalized mathematics, hindering interoperability between systems and libraries. Realms have been proposed as an explicit representation of collections of isomorphic theories and conservative extensions, but have proven difficult to implement and manage. Therefore, here we introduce a more specialized definition that, in our experience, covers a large set of practically relevant examples. The central concept is that of a base of a theory: a subtheory that uniquely determines the entire theory. This allows us to represent an entire realm as a single theory with multiple bases. We show that many foundational concepts can be elegantly represented as such basic realms. The resulting formalism offers a good abstraction level to deal with (the consequences of) differing choices in the literature and in formal libraries, thus reducing interoperability problems, while keeping the formalizations simple.
Flexible Boolean semantics is a framework for analysing natural language using Boolean algebras and flexibility principles. In this article, we use flexible Boolean semantics to analyse the language of mathematics. We find that the framework cannot be used to produce desirable results for sentences in which the subject is a coordination of definite descriptions, each denoting a set, and the predicate describes a property of sets. To resolve this issue, we extend the type system and the operators from the framework to handle such sentences.
Now pervasive in many mathematics and computer science research domains, proof assistants have recently gained importance in education, mostly during the college years. In this article, we propose a new learning environment as a layer above the Lean proof assistant, specifically targeting high-school level proofs. Drawing inspiration from coherent logic and adaptations of proof assistants for teaching, such as Lean-Verbose and Coq Waterproof, along with our own experience using proof assistants in higher education, we designed Yalep, a declarative controlled natural language, with a minimal number of syntactic constructions, which favors forward-chaining of facts. Yalep provides convenience for type theory hiding, and functions defined on type subsets. This paper presents the design choices and implementation of these features.
