Integrating searching and authoring in Mizar

DOI10.1007/S10817-007-9073-2MaRDI QIDQ2462640zbMATH OpenOpenAlexFDO

Authors Paul Cairns, Jeremy Gow

Publication date 3 December 2007

Published in Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s10817-007-9073-2

zbMATH Keywords

AlcorInformation retrievalLSIMathematicsMizar

Mathematics Subject Classification ID

Information storage and retrieval of data (68P20)

Recommendations

• Mathematical Knowledge Management
• scientific article; zbMATH DE number 1951634
• Information Retrieval and Rendering with MML Query
• MizarMode -- an integrated proof assistance tool for the Mizar way of formalizing mathematics
• Mathematical knowledge management in MIZAR

Cites work

• Abstracts of additional presentations made at the Royal Society Discussion Meeting ‘The nature of mathematical proof’
• An overview of a formal framework for managing mathematics
• scientific article; zbMATH DE number 1696613 (Why is no real title available?)
• scientific article; zbMATH DE number 2127501 (Why is no real title available?)
• scientific article; zbMATH DE number 3521895 (Why is no real title available?)
• scientific article; zbMATH DE number 1951625 (Why is no real title available?)
• scientific article; zbMATH DE number 1951634 (Why is no real title available?)
• scientific article; zbMATH DE number 1951636 (Why is no real title available?)
• scientific article; zbMATH DE number 2190569 (Why is no real title available?)
• Integrating computer algebra into proof planning
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical Knowledge Management
• Mathematical knowledge management. Second international conference, MKM 2003, Bertinoro, Italy, February 16--18, 2003. Proceedings
• Mathematical knowledge management. Third international conference, MKM 2004, Białowieża, Poland, September 19--21, 2004. Proceedings.
• MPTP-motivation, implementation, first experiments
• Types for Proofs and Programs

Cited in

(4)

• Custom automations in Mizar
• A user-friendly interface for a lightweight verification system
• Mathematical Knowledge Management
• An integrated web platform for the Mizar Mathematical Library

Describes a project that uses

Uses Software

• MML
• ANTLR
• MoMM
• Whelp
• ALCOR
• Mizar
• MPTP

This page was built for publication: Integrating searching and authoring in Mizar

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