Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language
Identifieur interne : 00A972 ( Main/Curation ); précédent : 00A971; suivant : 00A973Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language
Auteurs : Zhaohui Luo [Royaume-Uni] ; Paul Callaghan [Royaume-Uni]Source :
- Lecture Notes in Computer Science [ 0302-9743 ]
Abstract
Abstract: This paper investigates the semantics of mathematical concepts in a type theoretic framework with coercive subtyping. The type-theoretic analysis provides a formal semantic basis in the design and implementation of Mathematical Vernacular (MV), a natural language suitable for interactive development of mathematics with the support of the current theorem provingtec hnology. The idea of semantic well-formedness in mathematical language is motivated with examples. A formal system based on a notion of conceptual category is then presented, showing how type checking supports our notion of well-formedness. The power of this system is then extended by incorporating a notion of subcategory, using ideas from a more general theory of coercive subtyping, which provides the mechanisms for modelling conventional abbreviations in mathematics. Finally, we outline how this formal work can be used in an implementation of MV.
Url:
DOI: 10.1007/3-540-48975-4_12
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: Pour aller vers cette notice dans l'étape Curation :000742
- to stream Istex, to step Curation: Pour aller vers cette notice dans l'étape Curation :000737
- to stream Istex, to step Checkpoint: Pour aller vers cette notice dans l'étape Curation :002358
- to stream Main, to step Merge: Pour aller vers cette notice dans l'étape Curation :00B024
Links to Exploration step
ISTEX:20F3C0276115EB9B2B3164C4D24C71E107B0AD29Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language</title><author><name sortKey="Luo, Zhaohui" sort="Luo, Zhaohui" uniqKey="Luo Z" first="Zhaohui" last="Luo">Zhaohui Luo</name></author><author><name sortKey="Callaghan, Paul" sort="Callaghan, Paul" uniqKey="Callaghan P" first="Paul" last="Callaghan">Paul Callaghan</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:20F3C0276115EB9B2B3164C4D24C71E107B0AD29</idno><date when="1999" year="1999">1999</date><idno type="doi">10.1007/3-540-48975-4_12</idno><idno type="url">https://api.istex.fr/ark:/67375/HCB-LM97HF74-0/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">000742</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">000742</idno><idno type="wicri:Area/Istex/Curation">000737</idno><idno type="wicri:Area/Istex/Checkpoint">002358</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">002358</idno><idno type="wicri:doubleKey">0302-9743:1999:Luo Z:mathematical:vernacular:and</idno><idno type="wicri:Area/Main/Merge">00B024</idno><idno type="wicri:Area/Main/Curation">00A972</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language</title><author><name sortKey="Luo, Zhaohui" sort="Luo, Zhaohui" uniqKey="Luo Z" first="Zhaohui" last="Luo">Zhaohui Luo</name><affiliation wicri:level="1"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham</wicri:regionArea><wicri:noRegion>Durham</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author><author><name sortKey="Callaghan, Paul" sort="Callaghan, Paul" uniqKey="Callaghan P" first="Paul" last="Callaghan">Paul Callaghan</name><affiliation wicri:level="1"><country xml:lang="fr">Royaume-Uni</country><wicri:regionArea>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham</wicri:regionArea><wicri:noRegion>Durham</wicri:noRegion></affiliation><affiliation wicri:level="1"><country wicri:rule="url">Royaume-Uni</country></affiliation></author></analytic><monogr></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><idno type="ISSN">0302-9743</idno><idno type="ISSN">0302-9743</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: This paper investigates the semantics of mathematical concepts in a type theoretic framework with coercive subtyping. The type-theoretic analysis provides a formal semantic basis in the design and implementation of Mathematical Vernacular (MV), a natural language suitable for interactive development of mathematics with the support of the current theorem provingtec hnology. The idea of semantic well-formedness in mathematical language is motivated with examples. A formal system based on a notion of conceptual category is then presented, showing how type checking supports our notion of well-formedness. The power of this system is then extended by incorporating a notion of subcategory, using ideas from a more general theory of coercive subtyping, which provides the mechanisms for modelling conventional abbreviations in mathematics. Finally, we outline how this formal work can be used in an implementation of MV.</div></front></TEI></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Curation
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 00A972 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Curation/biblio.hfd -nk 00A972 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Curation
|type= RBID
|clé= ISTEX:20F3C0276115EB9B2B3164C4D24C71E107B0AD29
|texte= Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language
}}
| This area was generated with Dilib version V0.6.33. |  |