A query language for formal mathematical libraries

DOI10.1007/978-3-642-31374-5_10zbMATH Open1359.68272arXiv1204.4685OpenAlexW1581739545MaRDI QIDQ2907320FDOQ2907320

Authors: Florian Rabe 

Publication date: 7 September 2012

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

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.

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

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

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)

Cites Work

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

Cited In (8)

• Algebraic and calculus query languages for recursively typed complex objects
• Towards a heterogeneous query language for mathematical knowledge
• A scalable module system
• Title not available (Why is that?)
• QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
• A survey of languages for formalizing mathematics
• A survey on retrieval of mathematical knowledge
• Supporting data-driven mathematics: database and interface generation

Uses Software

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

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)