A user interface for a mathematical system that allows ambiguous formulae

DOI10.1016/J.ENTCS.2008.12.098MaRDI QIDQ5166498zbMATH OpenOpenAlexFDO

Authors Claudio Sacerdoti Coen

Publication date 27 June 2014

Published in Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.entcs.2008.12.098

zbMATH Keywords

ambiguityMatitaoverloadingtheorem proveruser interface

Mathematics Subject Classification ID

Recommendations

• Mathematical Knowledge Management
• Rating Disambiguation Errors
• Math indexer and searcher web interface. Towards fulfillment of mathematicians' information needs
• From Notation to Semantics: There and Back Again
• scientific article; zbMATH DE number 125121

Cites work

• A comparison of Mizar and Isar
• Coercive subtyping
• scientific article; zbMATH DE number 1629953 (Why is no real title available?)
• Mathematical Knowledge Management
• Mathematical knowledge management in HELM
• Spurious Disambiguation Error Detection
• Spurious disambiguation errors and how to get rid of them
• Types for Proofs and Programs
• User interaction with the Matita proof assistant

Cited in

(8)

• Towards semantic mathematical editing
• A preliminary report on the MathBrush pen-math system
• scientific article; zbMATH DE number 125121 (Why is no real title available?)
• A user-friendly interface for a lightweight verification system
• Mathematical Knowledge Management
• Spurious Disambiguation Error Detection
• From Notation to Semantics: There and Back Again
• Spurious disambiguation errors and how to get rid of them

Describes a project that uses

Uses Software

• Isar
• Mizar
• Proof General
• Matita
• CtCoq
• Whelp

This page was built for publication: A user interface for a mathematical system that allows ambiguous formulae

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