Information retrieval in MML

DOI10.1007/3-540-36469-2_10MaRDI QIDQ4413887zbMATH OpenFDO

Authors Grzegorz Bancerek, Piotr Rudnicki

Publication date 21 July 2003

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

Full work available at URL http://link.springer.de/link/service/series/0558/bibs/2594/25940119.htm

Mathematics Subject Classification ID

Database theory (68P15) Information storage and retrieval of data (68P20) Knowledge representation (68T30)

Recommendations

• Information Retrieval and Rendering with MML Query
• Mathematical knowledge management in MIZAR
• On the integrity of a repository of formalized mathematics
• Mathematical Knowledge Management
• The role of the Mizar mathematical library for interactive proof development in Mizar

Cited in

(20)

• The role of the Mizar mathematical library for interactive proof development in Mizar
• MML
• Semantics of Mizar as an Isabelle object logic
• User interaction with the Matita proof assistant
• Integrating searching and authoring in Mizar
• Crystal: Integrating structured queries into a tactic language
• Mathematical knowledge management in MIZAR
• Accessing the Mizar library with a weakly strict Mizar parser
• Presenting and explaining Mizar
• A query language for formal mathematical libraries
• A Brief Overview of Mizar
• Mizar: state-of-the-art and beyond
• Documentation Generator Focusing on Symbols for the HTML-ized Mizar Library
• Tools for MML environment analysis
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Information Retrieval and Rendering with MML Query
• An integrated web platform for the Mizar Mathematical Library
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• MPTP 0.2: Design, implementation, and initial experiments

Describes a project that uses

Uses Software

• Mizar

This page was built for publication: Information retrieval in MML

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