A query language for formal mathematical libraries

DOI10.1007/978-3-642-31374-5_10MaRDI QIDQ2907320zbMATH OpenOpenAlexFDO

Authors Florian Rabe

Publication date 7 September 2012

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1204.4685

Mathematics Subject Classification ID

Information storage and retrieval of data (68P20) Knowledge representation (68T30) Computing methodologies for information systems (hypertext navigation, interfaces, decision support, etc.) (68U35)

Abstract: One of the most promising applications of mathematical knowledge management is search: Even if we restrict attention to the tiny fragment of mathematics that has been formalized, the amount exceeds the comprehension of an individual human. Based on the generic representation language MMT, we introduce the mathematical query language QMT: It combines simplicity, expressivity, and scalability while avoiding a commitment to a particular logical formalism. QMT can integrate various search paradigms such as unification, semantic web, or XQuery style queries, and QMT queries can span different mathematical libraries. We have implemented QMT as a part of the MMT API. This combination provides a scalable indexing and query engine that can be readily applied to any library of mathematical knowledge. While our focus here is on libraries that are available in a content markup language, QMT naturally extends to presentation and narration markup languages.

Recommendations

• Towards a heterogeneous query language for mathematical knowledge
• Information Retrieval and Rendering with MML Query
• scientific article; zbMATH DE number 1951633
• A Search Engine for Mathematical Formulae
• Relational data across mathematical libraries

Cites work

• scientific article; zbMATH DE number 1951627 (Why is no real title available?)
• scientific article; zbMATH DE number 1951634 (Why is no real title available?)
• A Search Engine for Mathematical Formulae
• A framework for defining logics
• A math query language with an expanded set of wildcards
• A scalable module system
• Extending full text search engine for mathematical content
• Indexing and Searching Mathematics in Digital Libraries
• Mathematical Knowledge Management
• Methods to access and retrieve mathematical content in ActiveMath
• Project abstract: logic atlas and integrator (LATIN)
• Querying proofs
• Technical aspects of the digital library of mathematical functions
• The MMT API: a generic MKM system
• The TPTP problem library. CNF release v1. 2. 1
• Towards MKM in the large: modular representation and scalable software architecture

Cited in

(10)

• Algebraic and calculus query languages for recursively typed complex objects
• Towards a heterogeneous query language for mathematical knowledge
• A scalable module system
• scientific article; zbMATH DE number 1951633 (Why is no real title available?)
• QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
• A survey of languages for formalizing mathematics
• Relational data across mathematical libraries
• QED reloaded: towards a pluralistic formal library of mathematical knowledge
• Supporting data-driven mathematics: database and interface generation
• The MMT API: a generic MKM system

Describes a project that uses

Uses Software

• TNTBase
• QMT
• MMT
• Mizar
• MoMM
• TPTP
• MathWebSearch

This page was built for publication: A query language for formal mathematical libraries

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2907320)