Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language
Identifieur interne : 000742 ( Istex/Corpus ); précédent : 000741; suivant : 000743Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language
Auteurs : Zhaohui Luo ; Paul CallaghanSource :
- 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 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><affiliation><mods:affiliation>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Zhaohui.Luo@durham.ac.uk</mods:affiliation></affiliation></author><author><name sortKey="Callaghan, Paul" sort="Callaghan, Paul" uniqKey="Callaghan P" first="Paul" last="Callaghan">Paul Callaghan</name><affiliation><mods:affiliation>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: P.C.Callaghan@durham.ac.uk</mods:affiliation></affiliation></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></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><mods:affiliation>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: Zhaohui.Luo@durham.ac.uk</mods:affiliation></affiliation></author><author><name sortKey="Callaghan, Paul" sort="Callaghan, Paul" uniqKey="Callaghan P" first="Paul" last="Callaghan">Paul Callaghan</name><affiliation><mods:affiliation>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK</mods:affiliation></affiliation><affiliation><mods:affiliation>E-mail: P.C.Callaghan@durham.ac.uk</mods:affiliation></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><istex><corpusName>springer-ebooks</corpusName><author><json:item><name>Zhaohui Luo</name><affiliations><json:string>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK</json:string><json:string>E-mail: Zhaohui.Luo@durham.ac.uk</json:string></affiliations></json:item><json:item><name>Paul Callaghan</name><affiliations><json:string>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK</json:string><json:string>E-mail: P.C.Callaghan@durham.ac.uk</json:string></affiliations></json:item></author><arkIstex>ark:/67375/HCB-LM97HF74-0</arkIstex><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><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.</abstract><qualityIndicators><score>8.62</score><pdfWordCount>7955</pdfWordCount><pdfCharCount>46556</pdfCharCount><pdfVersion>1.3</pdfVersion><pdfPageCount>20</pdfPageCount><pdfPageSize>464 x 671 pts</pdfPageSize><refBibsNative>false</refBibsNative><abstractWordCount>135</abstractWordCount><abstractCharCount>931</abstractCharCount><keywordCount>0</keywordCount></qualityIndicators><title>Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language</title><chapterId><json:string>12</json:string><json:string>Chap12</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><title>Lecture Notes in Computer Science</title><language><json:string>unknown</json:string></language><copyrightDate>1999</copyrightDate><issn><json:string>0302-9743</json:string></issn><editor><json:item><name>G. Goos</name></json:item><json:item><name>J. Hartmanis</name></json:item><json:item><name>J. van Leeuwen</name></json:item></editor></serie><host><title>Logical Aspects of Computational Linguistics</title><language><json:string>unknown</json:string></language><copyrightDate>1999</copyrightDate><doi><json:string>10.1007/3-540-48975-4</json:string></doi><issn><json:string>0302-9743</json:string></issn><eisbn><json:string>978-3-540-48975-7</json:string></eisbn><bookId><json:string>3-540-48975-4</json:string></bookId><isbn><json:string>978-3-540-65751-4</json:string></isbn><volume>1582</volume><pages><first>231</first><last>250</last></pages><genre><json:string>book-series</json:string></genre><editor><json:item><name>Alain Lecomte</name><affiliations><json:string>Université Pierre Mendès France (Grenoble 2), 1251 avenue Centrale, BP 47, F-38040, Grenoble Cedex, France</json:string><json:string>E-mail: Alain.Lecomte@upmf-grenoble.fr</json:string></affiliations></json:item><json:item><name>François Lamarche</name><affiliations><json:string>LORIA (Nancy), 615 rue de Jardin Botanique, BP 101, F-54602, Villers lès Nancy Cedex, France</json:string><json:string>E-mail: Lamarche@loria.fr</json:string></affiliations></json:item><json:item><name>Guy Perrier</name><affiliations><json:string>LORIA (Nancy), 615 rue de Jardin Botanique, BP 101, F-54602, Villers lès Nancy Cedex, France</json:string><json:string>E-mail: Perrier@loria.fr</json:string></affiliations></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Logics and Meanings of Programs</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Mathematical Logic and Formal Languages</value></json:item></subject></host><ark><json:string>ark:/67375/HCB-LM97HF74-0</json:string></ark><publicationDate>1999</publicationDate><copyrightDate>1999</copyrightDate><doi><json:string>10.1007/3-540-48975-4_12</json:string></doi><id>20F3C0276115EB9B2B3164C4D24C71E107B0AD29</id><score>1</score><fulltext><json:item><extension>pdf</extension><original>true</original><mimetype>application/pdf</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-LM97HF74-0/fulltext.pdf</uri></json:item><json:item><extension>zip</extension><original>false</original><mimetype>application/zip</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-LM97HF74-0/bundle.zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/ark:/67375/HCB-LM97HF74-0/fulltext.tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language</title></titleStmt><publicationStmt><authority>ISTEX</authority><availability><licence>Springer-Verlag Berlin Heidelberg</licence></availability><date when="1999">1999</date></publicationStmt><notesStmt><note type="conference" source="proceedings" scheme="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</note><note type="publication-type" subtype="book-series" scheme="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</note></notesStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language</title><author><persName><forename type="first">Zhaohui</forename><surname>Luo</surname></persName><email>Zhaohui.Luo@durham.ac.uk</email><affiliation><orgName type="department">Department of Computer Science</orgName><orgName type="institution">University of Durham</orgName><address><street>South Road</street><settlement>Durham</settlement><postCode>DH1 3LE</postCode><country key="GB">UNITED KINGDOM</country></address></affiliation></author><author><persName><forename type="first">Paul</forename><surname>Callaghan</surname></persName><email>P.C.Callaghan@durham.ac.uk</email><affiliation><orgName type="department">Department of Computer Science</orgName><orgName type="institution">University of Durham</orgName><address><street>South Road</street><settlement>Durham</settlement><postCode>DH1 3LE</postCode><country key="GB">UNITED KINGDOM</country></address></affiliation></author><idno type="istex">20F3C0276115EB9B2B3164C4D24C71E107B0AD29</idno><idno type="ark">ark:/67375/HCB-LM97HF74-0</idno><idno type="DOI">10.1007/3-540-48975-4_12</idno></analytic><monogr><title level="m" type="main">Logical Aspects of Computational Linguistics</title><title level="m" type="sub">Second International Conference, LACL'97 Nancy, France, September 22-24, 1997 Selected Papers</title><title level="m" type="part">Selected papers</title><idno type="DOI">10.1007/3-540-48975-4</idno><idno type="book-id">3-540-48975-4</idno><idno type="ISBN">978-3-540-65751-4</idno><idno type="eISBN">978-3-540-48975-7</idno><idno type="chapter-id">Chap12</idno><idno type="part-id">Part2</idno><editor><persName><forename type="first">Alain</forename><surname>Lecomte</surname></persName><email>Alain.Lecomte@upmf-grenoble.fr</email><affiliation><orgName type="institution">Université Pierre Mendès France (Grenoble 2)</orgName><address><street>1251 avenue Centrale</street><postBox>BP 47</postBox><postCode>F-38040</postCode><settlement>Grenoble Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></editor><editor><persName><forename type="first">François</forename><surname>Lamarche</surname></persName><email>Lamarche@loria.fr</email><affiliation><orgName type="institution">LORIA (Nancy)</orgName><address><street>615 rue de Jardin Botanique</street><postBox>BP 101</postBox><postCode>F-54602</postCode><settlement>Villers lès Nancy Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></editor><editor><persName><forename type="first">Guy</forename><surname>Perrier</surname></persName><email>Perrier@loria.fr</email><affiliation><orgName type="institution">LORIA (Nancy)</orgName><address><street>615 rue de Jardin Botanique</street><postBox>BP 101</postBox><postCode>F-54602</postCode><settlement>Villers lès Nancy Cedex</settlement><country key="FR">FRANCE</country></address></affiliation></editor><imprint><biblScope unit="vol">1582</biblScope><biblScope unit="page" from="231">231</biblScope><biblScope unit="page" to="250">250</biblScope><biblScope unit="chapter-count">12</biblScope><biblScope unit="part-chapter-count">10</biblScope></imprint></monogr><series><title level="s" type="main" xml:lang="en">Lecture Notes in Computer Science</title><editor><persName><forename type="first">G.</forename><surname>Goos</surname></persName></editor><editor><persName><forename type="first">J.</forename><surname>Hartmanis</surname></persName></editor><editor><persName><forename type="first">J.</forename><nameLink>van</nameLink><surname>Leeuwen</surname></persName></editor><idno type="pISSN">0302-9743</idno><idno type="seriesID">558</idno></series></biblStruct></sourceDesc></fileDesc><profileDesc><abstract xml:lang="en"><head>Abstract</head><p>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.</p><p>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.</p></abstract><textClass ana="subject"><keywords scheme="book-subject-collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass ana="subject"><keywords scheme="book-subject"><list><label>I</label><item><term type="Primary">Computer Science</term></item><label>I1603X</label><item><term type="Secondary" subtype="priority-1">Logics and Meanings of Programs</term></item><label>I21017</label><item><term type="Secondary" subtype="priority-2">Artificial Intelligence (incl. Robotics)</term></item><label>I16048</label><item><term type="Secondary" subtype="priority-3">Mathematical Logic and Formal Languages</term></item></list></keywords></textClass><langUsage><language ident="EN"></language></langUsage></profileDesc></teiHeader></istex:fulltextTEI><json:item><extension>txt</extension><original>false</original><mimetype>text/plain</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-LM97HF74-0/fulltext.txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="corpus springer-ebooks not found" wicri:toSee="no header"><istex:xmlDeclaration>version="1.0" encoding="UTF-8"</istex:xmlDeclaration><istex:docType PUBLIC="-//Springer-Verlag//DTD A++ V2.4//EN" URI="http://devel.springer.de/A++/V2.4/DTD/A++V2.4.dtd" name="istex:docType"></istex:docType><istex:document><Publisher><PublisherInfo><PublisherName>Springer Berlin Heidelberg</PublisherName><PublisherLocation>Berlin, Heidelberg</PublisherLocation></PublisherInfo><Series><SeriesInfo SeriesType="Series" TocLevels="0"><SeriesID>558</SeriesID><SeriesPrintISSN>0302-9743</SeriesPrintISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>G.</GivenName><FamilyName>Goos</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><FamilyName>Hartmanis</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>J.</GivenName><Particle>van</Particle><FamilyName>Leeuwen</FamilyName></EditorName></Editor></EditorGroup></SeriesHeader><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" TocLevels="0"><BookID>3-540-48975-4</BookID><BookTitle>Logical Aspects of Computational Linguistics</BookTitle><BookSubTitle>Second International Conference, LACL'97 Nancy, France, September 22-24, 1997 Selected Papers</BookSubTitle><BookVolumeNumber>1582</BookVolumeNumber><BookSequenceNumber>1582</BookSequenceNumber><BookDOI>10.1007/3-540-48975-4</BookDOI><BookTitleID>59606</BookTitleID><BookPrintISBN>978-3-540-65751-4</BookPrintISBN><BookElectronicISBN>978-3-540-48975-7</BookElectronicISBN><BookChapterCount>12</BookChapterCount><BookHistory><OnlineDate><Year>2001</Year><Month>5</Month><Day>22</Day></OnlineDate></BookHistory><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>1999</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I1603X" Priority="1" Type="Secondary">Logics and Meanings of Programs</BookSubject><BookSubject Code="I21017" Priority="2" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><BookSubject Code="I16048" Priority="3" Type="Secondary">Mathematical Logic and Formal Languages</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup><BookContext><SeriesID>558</SeriesID></BookContext></BookInfo><BookHeader><EditorGroup><Editor AffiliationIDS="Aff1"><EditorName DisplayOrder="Western"><GivenName>Alain</GivenName><FamilyName>Lecomte</FamilyName></EditorName><Contact><Email>Alain.Lecomte@upmf-grenoble.fr</Email></Contact></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>François</GivenName><FamilyName>Lamarche</FamilyName></EditorName><Contact><Email>Lamarche@loria.fr</Email></Contact></Editor><Editor AffiliationIDS="Aff2"><EditorName DisplayOrder="Western"><GivenName>Guy</GivenName><FamilyName>Perrier</FamilyName></EditorName><Contact><Email>Perrier@loria.fr</Email></Contact></Editor><Affiliation ID="Aff1"><OrgName>Université Pierre Mendès France (Grenoble 2)</OrgName><OrgAddress><Street>1251 avenue Centrale</Street><Postbox>BP 47</Postbox><Postcode>F-38040</Postcode><City>Grenoble Cedex</City><Country>France</Country></OrgAddress></Affiliation><Affiliation ID="Aff2"><OrgName>LORIA (Nancy)</OrgName><OrgAddress><Street>615 rue de Jardin Botanique</Street><Postbox>BP 101</Postbox><Postcode>F-54602</Postcode><City>Villers lès Nancy Cedex</City><Country>France</Country></OrgAddress></Affiliation></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Selected papers</PartTitle><PartChapterCount>10</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookID>3-540-48975-4</BookID><BookTitle>Logical Aspects of Computational Linguistics</BookTitle></PartContext></PartInfo><Chapter ID="Chap12" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" Language="En" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>12</ChapterID><ChapterDOI>10.1007/3-540-48975-4_12</ChapterDOI><ChapterSequenceNumber>12</ChapterSequenceNumber><ChapterTitle Language="En">Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language</ChapterTitle><ChapterFirstPage>231</ChapterFirstPage><ChapterLastPage>250</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>1999</CopyrightYear></ChapterCopyright><ChapterHistory><RegistrationDate><Year>2001</Year><Month>5</Month><Day>21</Day></RegistrationDate><OnlineDate><Year>2001</Year><Month>5</Month><Day>22</Day></OnlineDate></ChapterHistory><ChapterGrants Type="Regular"><MetadataGrant Grant="OpenAccess"></MetadataGrant><AbstractGrant Grant="OpenAccess"></AbstractGrant><BodyPDFGrant Grant="Restricted"></BodyPDFGrant><BodyHTMLGrant Grant="Restricted"></BodyHTMLGrant><BibliographyGrant Grant="Restricted"></BibliographyGrant><ESMGrant Grant="Restricted"></ESMGrant></ChapterGrants><ChapterContext><SeriesID>558</SeriesID><PartID>2</PartID><BookID>3-540-48975-4</BookID><BookTitle>Logical Aspects of Computational Linguistics</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>Zhaohui</GivenName><FamilyName>Luo</FamilyName></AuthorName><Contact><Email>Zhaohui.Luo@durham.ac.uk</Email></Contact></Author><Author AffiliationIDS="Aff5"><AuthorName DisplayOrder="Western"><GivenName>Paul</GivenName><FamilyName>Callaghan</FamilyName></AuthorName><Contact><Email>P.C.Callaghan@durham.ac.uk</Email></Contact></Author><Affiliation ID="Aff5"><OrgDivision>Department of Computer Science</OrgDivision><OrgName>University of Durham</OrgName><OrgAddress><Street>South Road</Street><City>Durham</City><Postcode>DH1 3LE</Postcode><Country>UK</Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>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.</Para><Para>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.</Para></Abstract><ArticleNote Type="Misc"><Heading>*</Heading><SimplePara>This work is supported partly by the Durham Mathematical Vernacular project funded by the Leverhulme Trust (see <ExternalRef><RefSource>http://www.dur.ac.uk/~dcs7ttg/mv.html</RefSource><RefTarget Address="http://www.dur.ac.uk/~dcs7ttg/mv.html" TargetType="URL"></RefTarget></ExternalRef>) and partly by the project on Subtyping, Inheritance, and Reuse funded by UK EPSRC (GR/K79130, see <ExternalRef><RefSource>http://www.dur.ac.uk/~dcs7ttg/sir.html</RefSource><RefTarget Address="http://www.dur.ac.uk/~dcs7ttg/sir.html" TargetType="URL"></RefTarget></ExternalRef>).</SimplePara></ArticleNote></ChapterHeader><NoBody></NoBody></Chapter></Part></Book><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle><SubSeriesSubTitle Language="En">Subseries of Lecture Notes in Computer Science</SubSeriesSubTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor AffiliationIDS="Aff3"><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor AffiliationIDS="Aff4"><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor><Affiliation ID="Aff3"><OrgName>University of Saarland</OrgName><OrgAddress><City>Saarbrücken</City><Country>Germany</Country></OrgAddress></Affiliation><Affiliation ID="Aff4"><OrgName>Carnegie Mellon University</OrgName><OrgAddress><City>Pittsburgh</City><State>PA</State><Postcode>USA</Postcode></OrgAddress></Affiliation></EditorGroup></SubSeriesHeader></SubSeries></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language</title></titleInfo><titleInfo type="alternative" contentType="CDATA"><title>Mathematical Vernacular and Conceptual Well-Formedness in Mathematical Language</title></titleInfo><name type="personal"><namePart type="given">Zhaohui</namePart><namePart type="family">Luo</namePart><affiliation>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK</affiliation><affiliation>E-mail: Zhaohui.Luo@durham.ac.uk</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Paul</namePart><namePart type="family">Callaghan</namePart><affiliation>Department of Computer Science, University of Durham, South Road, DH1 3LE, Durham, UK</affiliation><affiliation>E-mail: P.C.Callaghan@durham.ac.uk</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre displayLabel="OriginalPaper" authority="ISTEX" authorityURI="https://content-type.data.istex.fr" type="conference" valueURI="https://content-type.data.istex.fr/ark:/67375/XTP-BFHXPBJJ-3">conference</genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">1999</dateIssued><copyrightDate encoding="w3cdtf">1999</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><abstract 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.</abstract><relatedItem type="host"><titleInfo><title>Logical Aspects of Computational Linguistics</title><subTitle>Second International Conference, LACL'97 Nancy, France, September 22-24, 1997 Selected Papers</subTitle></titleInfo><name type="personal"><namePart type="given">Alain</namePart><namePart type="family">Lecomte</namePart><affiliation>Université Pierre Mendès France (Grenoble 2), 1251 avenue Centrale, BP 47, F-38040, Grenoble Cedex, France</affiliation><affiliation>E-mail: Alain.Lecomte@upmf-grenoble.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">François</namePart><namePart type="family">Lamarche</namePart><affiliation>LORIA (Nancy), 615 rue de Jardin Botanique, BP 101, F-54602, Villers lès Nancy Cedex, France</affiliation><affiliation>E-mail: Lamarche@loria.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Guy</namePart><namePart type="family">Perrier</namePart><affiliation>LORIA (Nancy), 615 rue de Jardin Botanique, BP 101, F-54602, Villers lès Nancy Cedex, France</affiliation><affiliation>E-mail: Perrier@loria.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" authority="ISTEX" authorityURI="https://publication-type.data.istex.fr" valueURI="https://publication-type.data.istex.fr/ark:/67375/JMC-0G6R5W5T-Z">book-series</genre><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">1999</copyrightDate><issuance>monographic</issuance></originInfo><subject><genre>Book-Subject-Collection</genre><topic authority="SpringerSubjectCodes" authorityURI="SUCO11645">Computer Science</topic></subject><subject><genre>Book-Subject-Group</genre><topic authority="SpringerSubjectCodes" authorityURI="I">Computer Science</topic><topic authority="SpringerSubjectCodes" authorityURI="I1603X">Logics and Meanings of Programs</topic><topic authority="SpringerSubjectCodes" authorityURI="I21017">Artificial Intelligence (incl. Robotics)</topic><topic authority="SpringerSubjectCodes" authorityURI="I16048">Mathematical Logic and Formal Languages</topic></subject><identifier type="DOI">10.1007/3-540-48975-4</identifier><identifier type="ISBN">978-3-540-65751-4</identifier><identifier type="eISBN">978-3-540-48975-7</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="BookTitleID">59606</identifier><identifier type="BookID">3-540-48975-4</identifier><identifier type="BookChapterCount">12</identifier><identifier type="BookVolumeNumber">1582</identifier><identifier type="BookSequenceNumber">1582</identifier><identifier type="PartChapterCount">10</identifier><part><date>1999</date><detail type="part"><title>Selected papers</title></detail><detail type="volume"><number>1582</number><caption>vol.</caption></detail><extent unit="pages"><start>231</start><end>250</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 1999</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><originInfo><publisher>Springer</publisher><copyrightDate encoding="w3cdtf">1999</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title><subTitle>Subseries of Lecture Notes in Computer Science</subTitle></titleInfo><name type="personal"><namePart type="given">G.</namePart><namePart type="family">Goos</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">Hartmanis</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="family">van Leeuwen</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Alain</namePart><namePart type="family">Lecomte</namePart><affiliation>Université Pierre Mendès France (Grenoble 2), 1251 avenue Centrale, BP 47, F-38040, Grenoble Cedex, France</affiliation><affiliation>E-mail: Alain.Lecomte@upmf-grenoble.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">François</namePart><namePart type="family">Lamarche</namePart><affiliation>LORIA (Nancy), 615 rue de Jardin Botanique, BP 101, F-54602, Villers lès Nancy Cedex, France</affiliation><affiliation>E-mail: Lamarche@loria.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Guy</namePart><namePart type="family">Perrier</namePart><affiliation>LORIA (Nancy), 615 rue de Jardin Botanique, BP 101, F-54602, Villers lès Nancy Cedex, France</affiliation><affiliation>E-mail: Perrier@loria.fr</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><affiliation>University of Saarland, Saarbrücken, Germany</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><affiliation>Carnegie Mellon University, USA, Pittsburgh, PA</affiliation><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 1999</recordOrigin></recordInfo></relatedItem><relatedItem type="otherVersion"></relatedItem><identifier type="istex">20F3C0276115EB9B2B3164C4D24C71E107B0AD29</identifier><identifier type="ark">ark:/67375/HCB-LM97HF74-0</identifier><identifier type="DOI">10.1007/3-540-48975-4_12</identifier><identifier type="ChapterID">12</identifier><identifier type="ChapterID">Chap12</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 1999</accessCondition><recordInfo><recordContentSource authority="ISTEX" authorityURI="https://loaded-corpus.data.istex.fr" valueURI="https://loaded-corpus.data.istex.fr/ark:/67375/XBH-RLRX46XW-4">springer</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 1999</recordOrigin></recordInfo></mods><json:item><extension>json</extension><original>false</original><mimetype>application/json</mimetype><uri>https://api.istex.fr/ark:/67375/HCB-LM97HF74-0/record.json</uri></json:item></metadata></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000742 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000742 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Istex
|étape= Corpus
|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. |  |