Narrative Structure of Mathematical Texts
Identifieur interne : 000434 ( Istex/Corpus ); précédent : 000433; suivant : 000435Narrative Structure of Mathematical Texts
Auteurs : Fairouz Kamareddine ; Manuel Maarek ; Krzysztof Retel ; B. WellsSource :
- Lecture Notes in Computer Science [ 0302-9743 ] ; 2007.
Abstract
Abstract: There are many styles for the narrative structure of a mathematical document. Each mathematician has its own conventions and traditions about labeling portions of texts (e.g., chapter, section, theorem or proof ) and identifying statements according to their logical importance (e.g., theorem is more important than lemma). Such narrative/structuring labels guide the reader’s navigation of the text and form the key components in the reasoning structure of the theory reflected in the text. We present in this paper a method to computerise the narrative structure of a text which includes the relationships between labeled text entities. These labels and relations are input by the user on top of their natural language text. This narrative structure is then automatically analysed to check its consistency. This automatic analysis consists of two phases: (1) checking the correct usage of labels and relations (i.e., that a ”proof” justifies a ”theorem” but cannot justify an ”axiom”) and (2) checking that the logical precedences in the document are self-consistent. The development of this method was driven by the experience of computerising a number of mathematical documents (covering different authoring styles). We illustrate how such computerised narrative structure could be used for further manipulations, i.e. to build a skeleton of a formal document in a formal system like Mizar, Coq or Isabelle.
Url:
DOI: 10.1007/978-3-540-73086-6_24
Links to Exploration step
ISTEX:5928DA25C0C059A841D18103BC1854AF9743DC6BLe document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct:series"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Narrative Structure of Mathematical Texts</title><author><name sortKey="Kamareddine, Fairouz" sort="Kamareddine, Fairouz" uniqKey="Kamareddine F" first="Fairouz" last="Kamareddine">Fairouz Kamareddine</name><affiliation><mods:affiliation>ULTRA group, Heriot-Watt University</mods:affiliation></affiliation></author><author><name sortKey="Maarek, Manuel" sort="Maarek, Manuel" uniqKey="Maarek M" first="Manuel" last="Maarek">Manuel Maarek</name><affiliation><mods:affiliation>ULTRA group, Heriot-Watt University</mods:affiliation></affiliation></author><author><name sortKey="Retel, Krzysztof" sort="Retel, Krzysztof" uniqKey="Retel K" first="Krzysztof" last="Retel">Krzysztof Retel</name><affiliation><mods:affiliation>ULTRA group, Heriot-Watt University</mods:affiliation></affiliation></author><author><name sortKey="Wells, B" sort="Wells, B" uniqKey="Wells B" first="B." last="Wells">B. Wells</name><affiliation><mods:affiliation>ULTRA group, Heriot-Watt University</mods:affiliation></affiliation></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:5928DA25C0C059A841D18103BC1854AF9743DC6B</idno><date when="2007" year="2007">2007</date><idno type="doi">10.1007/978-3-540-73086-6_24</idno><idno type="url">https://api.istex.fr/document/5928DA25C0C059A841D18103BC1854AF9743DC6B/fulltext/pdf</idno><idno type="wicri:Area/Istex/Corpus">000434</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Narrative Structure of Mathematical Texts</title><author><name sortKey="Kamareddine, Fairouz" sort="Kamareddine, Fairouz" uniqKey="Kamareddine F" first="Fairouz" last="Kamareddine">Fairouz Kamareddine</name><affiliation><mods:affiliation>ULTRA group, Heriot-Watt University</mods:affiliation></affiliation></author><author><name sortKey="Maarek, Manuel" sort="Maarek, Manuel" uniqKey="Maarek M" first="Manuel" last="Maarek">Manuel Maarek</name><affiliation><mods:affiliation>ULTRA group, Heriot-Watt University</mods:affiliation></affiliation></author><author><name sortKey="Retel, Krzysztof" sort="Retel, Krzysztof" uniqKey="Retel K" first="Krzysztof" last="Retel">Krzysztof Retel</name><affiliation><mods:affiliation>ULTRA group, Heriot-Watt University</mods:affiliation></affiliation></author><author><name sortKey="Wells, B" sort="Wells, B" uniqKey="Wells B" first="B." last="Wells">B. Wells</name><affiliation><mods:affiliation>ULTRA group, Heriot-Watt University</mods:affiliation></affiliation></author></analytic><monogr></monogr><series><title level="s">Lecture Notes in Computer Science</title><imprint><date>2007</date></imprint><idno type="ISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="ISSN">0302-9743</idno></series><idno type="istex">5928DA25C0C059A841D18103BC1854AF9743DC6B</idno><idno type="DOI">10.1007/978-3-540-73086-6_24</idno><idno type="ChapterID">24</idno><idno type="ChapterID">Chap24</idno></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0302-9743</idno></seriesStmt></fileDesc><profileDesc><textClass></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract: There are many styles for the narrative structure of a mathematical document. Each mathematician has its own conventions and traditions about labeling portions of texts (e.g., chapter, section, theorem or proof ) and identifying statements according to their logical importance (e.g., theorem is more important than lemma). Such narrative/structuring labels guide the reader’s navigation of the text and form the key components in the reasoning structure of the theory reflected in the text. We present in this paper a method to computerise the narrative structure of a text which includes the relationships between labeled text entities. These labels and relations are input by the user on top of their natural language text. This narrative structure is then automatically analysed to check its consistency. This automatic analysis consists of two phases: (1) checking the correct usage of labels and relations (i.e., that a ”proof” justifies a ”theorem” but cannot justify an ”axiom”) and (2) checking that the logical precedences in the document are self-consistent. The development of this method was driven by the experience of computerising a number of mathematical documents (covering different authoring styles). We illustrate how such computerised narrative structure could be used for further manipulations, i.e. to build a skeleton of a formal document in a formal system like Mizar, Coq or Isabelle.</div></front></TEI><istex><corpusName>springer</corpusName><author><json:item><name>Fairouz Kamareddine</name><affiliations><json:string>ULTRA group, Heriot-Watt University,</json:string></affiliations></json:item><json:item><name>Manuel Maarek</name><affiliations><json:string>ULTRA group, Heriot-Watt University,</json:string></affiliations></json:item><json:item><name>Krzysztof Retel</name><affiliations><json:string>ULTRA group, Heriot-Watt University,</json:string></affiliations></json:item><json:item><name>J. B. Wells</name><affiliations><json:string>ULTRA group, Heriot-Watt University,</json:string></affiliations></json:item></author><language><json:string>eng</json:string></language><originalGenre><json:string>OriginalPaper</json:string></originalGenre><abstract>Abstract: There are many styles for the narrative structure of a mathematical document. Each mathematician has its own conventions and traditions about labeling portions of texts (e.g., chapter, section, theorem or proof ) and identifying statements according to their logical importance (e.g., theorem is more important than lemma). Such narrative/structuring labels guide the reader’s navigation of the text and form the key components in the reasoning structure of the theory reflected in the text. We present in this paper a method to computerise the narrative structure of a text which includes the relationships between labeled text entities. These labels and relations are input by the user on top of their natural language text. This narrative structure is then automatically analysed to check its consistency. This automatic analysis consists of two phases: (1) checking the correct usage of labels and relations (i.e., that a ”proof” justifies a ”theorem” but cannot justify an ”axiom”) and (2) checking that the logical precedences in the document are self-consistent. The development of this method was driven by the experience of computerising a number of mathematical documents (covering different authoring styles). We illustrate how such computerised narrative structure could be used for further manipulations, i.e. to build a skeleton of a formal document in a formal system like Mizar, Coq or Isabelle.</abstract><qualityIndicators><score>7.592</score><pdfVersion>1.3</pdfVersion><pdfPageSize>430 x 660 pts</pdfPageSize><refBibsNative>false</refBibsNative><keywordCount>0</keywordCount><abstractCharCount>1421</abstractCharCount><pdfWordCount>7200</pdfWordCount><pdfCharCount>40581</pdfCharCount><pdfPageCount>17</pdfPageCount><abstractWordCount>216</abstractWordCount></qualityIndicators><title>Narrative Structure of Mathematical Texts</title><chapterId><json:string>24</json:string><json:string>Chap24</json:string></chapterId><genre><json:string>conference</json:string></genre><serie><issn><json:string>0302-9743</json:string></issn><language><json:string>unknown</json:string></language><eissn><json:string>1611-3349</json:string></eissn><title>Lecture Notes in Computer Science</title><copyrightDate>2007</copyrightDate></serie><host><editor><json:item><name>Manuel Kauers</name></json:item><json:item><name>Manfred Kerber</name></json:item><json:item><name>Robert Miner</name></json:item><json:item><name>Wolfgang Windsteiger</name></json:item></editor><subject><json:item><value>Computer Science</value></json:item><json:item><value>Computer Science</value></json:item><json:item><value>Artificial Intelligence (incl. Robotics)</value></json:item><json:item><value>Data Mining and Knowledge Discovery</value></json:item><json:item><value>Information Systems Applications (incl.Internet)</value></json:item><json:item><value>Database Management</value></json:item><json:item><value>Computer Communication Networks</value></json:item><json:item><value>Mathematics, general</value></json:item></subject><isbn><json:string>978-3-540-73083-5</json:string></isbn><language><json:string>unknown</json:string></language><eissn><json:string>1611-3349</json:string></eissn><title>Towards Mechanized Mathematical Assistants</title><bookId><json:string>978-3-540-73086-6</json:string></bookId><volume>4573</volume><pages><last>312</last><first>296</first></pages><issn><json:string>0302-9743</json:string></issn><genre><json:string>book-series</json:string></genre><eisbn><json:string>978-3-540-73086-6</json:string></eisbn><copyrightDate>2007</copyrightDate><doi><json:string>10.1007/978-3-540-73086-6</json:string></doi></host><publicationDate>2007</publicationDate><copyrightDate>2007</copyrightDate><doi><json:string>10.1007/978-3-540-73086-6_24</json:string></doi><id>5928DA25C0C059A841D18103BC1854AF9743DC6B</id><score>0.13085245</score><fulltext><json:item><original>true</original><mimetype>application/pdf</mimetype><extension>pdf</extension><uri>https://api.istex.fr/document/5928DA25C0C059A841D18103BC1854AF9743DC6B/fulltext/pdf</uri></json:item><json:item><original>false</original><mimetype>application/zip</mimetype><extension>zip</extension><uri>https://api.istex.fr/document/5928DA25C0C059A841D18103BC1854AF9743DC6B/fulltext/zip</uri></json:item><istex:fulltextTEI uri="https://api.istex.fr/document/5928DA25C0C059A841D18103BC1854AF9743DC6B/fulltext/tei"><teiHeader><fileDesc><titleStmt><title level="a" type="main" xml:lang="en">Narrative Structure of Mathematical Texts</title><respStmt xml:id="ISTEX-API" resp="Références bibliographiques récupérées via GROBID" name="ISTEX-API (INIST-CNRS)"></respStmt><respStmt><resp>Références bibliographiques récupérées via GROBID</resp><name resp="ISTEX-API">ISTEX-API (INIST-CNRS)</name></respStmt></titleStmt><publicationStmt><authority>ISTEX</authority><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><availability><p>SPRINGER</p></availability><date>2007</date></publicationStmt><sourceDesc><biblStruct type="inbook"><analytic><title level="a" type="main" xml:lang="en">Narrative Structure of Mathematical Texts</title><author><persName><forename type="first">Fairouz</forename><surname>Kamareddine</surname></persName><affiliation>ULTRA group, Heriot-Watt University,</affiliation></author><author><persName><forename type="first">Manuel</forename><surname>Maarek</surname></persName><affiliation>ULTRA group, Heriot-Watt University,</affiliation></author><author><persName><forename type="first">Krzysztof</forename><surname>Retel</surname></persName><affiliation>ULTRA group, Heriot-Watt University,</affiliation></author><author><persName><forename type="first">J.</forename><surname>Wells</surname></persName><affiliation>ULTRA group, Heriot-Watt University,</affiliation></author></analytic><monogr><title level="m">Towards Mechanized Mathematical Assistants</title><title level="m" type="sub">14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007. Proceedings</title><idno type="pISBN">978-3-540-73083-5</idno><idno type="eISBN">978-3-540-73086-6</idno><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="DOI">10.1007/978-3-540-73086-6</idno><idno type="BookID">978-3-540-73086-6</idno><idno type="BookTitleID">150455</idno><idno type="BookSequenceNumber">4573</idno><idno type="BookVolumeNumber">4573</idno><idno type="BookChapterCount">31</idno><editor><persName><forename type="first">Manuel</forename><surname>Kauers</surname></persName></editor><editor><persName><forename type="first">Manfred</forename><surname>Kerber</surname></persName></editor><editor><persName><forename type="first">Robert</forename><surname>Miner</surname></persName></editor><editor><persName><forename type="first">Wolfgang</forename><surname>Windsteiger</surname></persName></editor><imprint><publisher>Springer Berlin Heidelberg</publisher><pubPlace>Berlin, Heidelberg</pubPlace><date type="published" when="2007"></date><biblScope unit="volume">4573</biblScope><biblScope unit="page" from="296">296</biblScope><biblScope unit="page" to="312">312</biblScope></imprint></monogr><series><title level="s">Lecture Notes in Computer Science</title><biblScope><date>2007</date></biblScope><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><idno type="seriesId">558</idno></series><series><title level="s">Lecture Notes in Artificial Intelligence</title><editor><persName><forename type="first">Jaime</forename><forename type="first">G.</forename><surname>Carbonell</surname></persName></editor><editor><persName><forename type="first">Jörg</forename><surname>Siekmann</surname></persName></editor><editor><persName><forename type="first">Manuel</forename><surname>Kauers</surname></persName></editor><editor><persName><forename type="first">Manfred</forename><surname>Kerber</surname></persName></editor><editor><persName><forename type="first">Robert</forename><surname>Miner</surname></persName></editor><editor><persName><forename type="first">Wolfgang</forename><surname>Windsteiger</surname></persName></editor><idno type="pISSN">0302-9743</idno><idno type="eISSN">1611-3349</idno><biblScope type="seriesId">1244</biblScope></series><idno type="istex">5928DA25C0C059A841D18103BC1854AF9743DC6B</idno><idno type="DOI">10.1007/978-3-540-73086-6_24</idno><idno type="ChapterID">24</idno><idno type="ChapterID">Chap24</idno></biblStruct></sourceDesc></fileDesc><profileDesc><creation><date>2007</date></creation><langUsage><language ident="en">en</language></langUsage><abstract xml:lang="en"><p>Abstract: There are many styles for the narrative structure of a mathematical document. Each mathematician has its own conventions and traditions about labeling portions of texts (e.g., chapter, section, theorem or proof ) and identifying statements according to their logical importance (e.g., theorem is more important than lemma). Such narrative/structuring labels guide the reader’s navigation of the text and form the key components in the reasoning structure of the theory reflected in the text. We present in this paper a method to computerise the narrative structure of a text which includes the relationships between labeled text entities. These labels and relations are input by the user on top of their natural language text. This narrative structure is then automatically analysed to check its consistency. This automatic analysis consists of two phases: (1) checking the correct usage of labels and relations (i.e., that a ”proof” justifies a ”theorem” but cannot justify an ”axiom”) and (2) checking that the logical precedences in the document are self-consistent. The development of this method was driven by the experience of computerising a number of mathematical documents (covering different authoring styles). We illustrate how such computerised narrative structure could be used for further manipulations, i.e. to build a skeleton of a formal document in a formal system like Mizar, Coq or Isabelle.</p></abstract><textClass><keywords scheme="Book Subject Collection"><list><label>SUCO11645</label><item><term>Computer Science</term></item></list></keywords></textClass><textClass><keywords scheme="Book Subject Group"><list><label>I</label><label>I21017</label><label>I18030</label><label>I18040</label><label>I18024</label><label>I13022</label><label>M00009</label><item><term>Computer Science</term></item><item><term>Artificial Intelligence (incl. Robotics)</term></item><item><term>Data Mining and Knowledge Discovery</term></item><item><term>Information Systems Applications (incl.Internet)</term></item><item><term>Database Management</term></item><item><term>Computer Communication Networks</term></item><item><term>Mathematics, general</term></item></list></keywords></textClass></profileDesc><revisionDesc><change when="2007">Published</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2016-3-20">References added</change><change xml:id="refBibs-istex" who="#ISTEX-API" when="2016-07-26">References added</change></revisionDesc></teiHeader></istex:fulltextTEI><json:item><original>false</original><mimetype>text/plain</mimetype><extension>txt</extension><uri>https://api.istex.fr/document/5928DA25C0C059A841D18103BC1854AF9743DC6B/fulltext/txt</uri></json:item></fulltext><metadata><istex:metadataXml wicri:clean="Springer, Publisher 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><SeriesElectronicISSN>1611-3349</SeriesElectronicISSN><SeriesTitle Language="En">Lecture Notes in Computer Science</SeriesTitle></SeriesInfo><SubSeries><SubSeriesInfo><SubSeriesID>1244</SubSeriesID><SubSeriesPrintISSN>0302-9743</SubSeriesPrintISSN><SubSeriesElectronicISSN>1611-3349</SubSeriesElectronicISSN><SubSeriesTitle Language="En">Lecture Notes in Artificial Intelligence</SubSeriesTitle></SubSeriesInfo><SubSeriesHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Jaime</GivenName><GivenName>G.</GivenName><FamilyName>Carbonell</FamilyName></EditorName></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Jörg</GivenName><FamilyName>Siekmann</FamilyName></EditorName></Editor></EditorGroup></SubSeriesHeader></SubSeries><Book Language="En"><BookInfo BookProductType="Proceedings" ContainsESM="No" Language="En" MediaType="eBook" NumberingStyle="Unnumbered" OutputMedium="All" TocLevels="0"><BookID>978-3-540-73086-6</BookID><BookTitle>Towards Mechanized Mathematical Assistants</BookTitle><BookSubTitle>14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007. Proceedings</BookSubTitle><BookVolumeNumber>4573</BookVolumeNumber><BookSequenceNumber>4573</BookSequenceNumber><BookDOI>10.1007/978-3-540-73086-6</BookDOI><BookTitleID>150455</BookTitleID><BookPrintISBN>978-3-540-73083-5</BookPrintISBN><BookElectronicISBN>978-3-540-73086-6</BookElectronicISBN><BookChapterCount>31</BookChapterCount><BookCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2007</CopyrightYear></BookCopyright><BookSubjectGroup><BookSubject Code="I" Type="Primary">Computer Science</BookSubject><BookSubject Code="I21017" Priority="1" Type="Secondary">Artificial Intelligence (incl. Robotics)</BookSubject><BookSubject Code="I18030" Priority="2" Type="Secondary">Data Mining and Knowledge Discovery</BookSubject><BookSubject Code="I18040" Priority="3" Type="Secondary">Information Systems Applications (incl.Internet)</BookSubject><BookSubject Code="I18024" Priority="4" Type="Secondary">Database Management</BookSubject><BookSubject Code="I13022" Priority="5" Type="Secondary">Computer Communication Networks</BookSubject><BookSubject Code="M00009" Priority="6" Type="Secondary">Mathematics, general</BookSubject><SubjectCollection Code="SUCO11645">Computer Science</SubjectCollection></BookSubjectGroup></BookInfo><BookHeader><EditorGroup><Editor><EditorName DisplayOrder="Western"><GivenName>Manuel</GivenName><FamilyName>Kauers</FamilyName></EditorName><Contact><Email>manuel.kauers@risc.uni-linz.ac.at</Email></Contact></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Manfred</GivenName><FamilyName>Kerber</FamilyName></EditorName><Contact><Email>M.Kerber@cs.bham.ac.uk</Email></Contact></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Robert</GivenName><FamilyName>Miner</FamilyName></EditorName><Contact><Email>robertm@dessci.com</Email></Contact></Editor><Editor><EditorName DisplayOrder="Western"><GivenName>Wolfgang</GivenName><FamilyName>Windsteiger</FamilyName></EditorName><Contact><Email>Wolfgang.Windsteiger@risc.Uni-Linz.ac.at</Email></Contact></Editor></EditorGroup></BookHeader><Part ID="Part2"><PartInfo TocLevels="0"><PartID>2</PartID><PartSequenceNumber>2</PartSequenceNumber><PartTitle>Contributions to MKM 2007</PartTitle><PartChapterCount>21</PartChapterCount><PartContext><SeriesID>558</SeriesID><BookTitle>Towards Mechanized Mathematical Assistants</BookTitle></PartContext></PartInfo><Chapter ID="Chap24" Language="En"><ChapterInfo ChapterType="OriginalPaper" ContainsESM="No" NumberingStyle="Unnumbered" TocLevels="0"><ChapterID>24</ChapterID><ChapterDOI>10.1007/978-3-540-73086-6_24</ChapterDOI><ChapterSequenceNumber>24</ChapterSequenceNumber><ChapterTitle Language="En">Narrative Structure of Mathematical Texts</ChapterTitle><ChapterFirstPage>296</ChapterFirstPage><ChapterLastPage>312</ChapterLastPage><ChapterCopyright><CopyrightHolderName>Springer-Verlag Berlin Heidelberg</CopyrightHolderName><CopyrightYear>2007</CopyrightYear></ChapterCopyright><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>978-3-540-73086-6</BookID><BookTitle>Towards Mechanized Mathematical Assistants</BookTitle></ChapterContext></ChapterInfo><ChapterHeader><AuthorGroup><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Fairouz</GivenName><FamilyName>Kamareddine</FamilyName></AuthorName><Contact><URL>http://www.macs.hw.ac.uk/ultra/</URL></Contact></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Manuel</GivenName><FamilyName>Maarek</FamilyName></AuthorName><Contact><URL>http://www.macs.hw.ac.uk/ultra/</URL></Contact></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>Krzysztof</GivenName><FamilyName>Retel</FamilyName></AuthorName><Contact><URL>http://www.macs.hw.ac.uk/ultra/</URL></Contact></Author><Author AffiliationIDS="Aff1"><AuthorName DisplayOrder="Western"><GivenName>J.</GivenName><GivenName>B.</GivenName><FamilyName>Wells</FamilyName></AuthorName><Contact><URL>http://www.macs.hw.ac.uk/ultra/</URL></Contact></Author><Affiliation ID="Aff1"><OrgName>ULTRA group, Heriot-Watt University</OrgName><OrgAddress><Country> </Country></OrgAddress></Affiliation></AuthorGroup><Abstract ID="Abs1" Language="En"><Heading>Abstract</Heading><Para>There are many styles for the narrative structure of a mathematical document. Each mathematician has its own conventions and traditions about labeling portions of texts <Emphasis Type="Italic">(e.g., chapter, section, theorem or proof )</Emphasis> and identifying statements according to their logical importance (e.g., <Emphasis Type="Italic">theorem </Emphasis>is more important than <Emphasis Type="Italic">lemma</Emphasis>). Such narrative/structuring labels guide the reader’s navigation of the text and form the key components in the reasoning structure of the theory reflected in the text.</Para><Para>We present in this paper a method to computerise the narrative structure of a text which includes the relationships between labeled text entities. These labels and relations are input by the user on top of their natural language text. This narrative structure is then automatically analysed to check its consistency. This automatic analysis consists of two phases: (1) checking the correct usage of labels and relations (i.e., that a ”proof” justifies a ”theorem” but cannot justify an ”axiom”) and (2) checking that the logical precedences in the document are self-consistent.</Para><Para>The development of this method was driven by the experience of computerising a number of mathematical documents (covering different authoring styles). We illustrate how such computerised narrative structure could be used for further manipulations, i.e. to build a skeleton of a formal document in a formal system like Mizar, Coq or Isabelle.</Para></Abstract></ChapterHeader><NoBody></NoBody></Chapter></Part></Book></Series></Publisher></istex:document></istex:metadataXml><mods version="3.6"><titleInfo lang="en"><title>Narrative Structure of Mathematical Texts</title></titleInfo><titleInfo type="alternative" contentType="CDATA" lang="en"><title>Narrative Structure of Mathematical Texts</title></titleInfo><name type="personal"><namePart type="given">Fairouz</namePart><namePart type="family">Kamareddine</namePart><affiliation>ULTRA group, Heriot-Watt University</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Manuel</namePart><namePart type="family">Maarek</namePart><affiliation>ULTRA group, Heriot-Watt University</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">Krzysztof</namePart><namePart type="family">Retel</namePart><affiliation>ULTRA group, Heriot-Watt University</affiliation><role><roleTerm type="text">author</roleTerm></role></name><name type="personal"><namePart type="given">J.</namePart><namePart type="given">B.</namePart><namePart type="family">Wells</namePart><affiliation>ULTRA group, Heriot-Watt University</affiliation><role><roleTerm type="text">author</roleTerm></role></name><typeOfResource>text</typeOfResource><genre type="conference" displayLabel="OriginalPaper"></genre><originInfo><publisher>Springer Berlin Heidelberg</publisher><place><placeTerm type="text">Berlin, Heidelberg</placeTerm></place><dateIssued encoding="w3cdtf">2007</dateIssued><copyrightDate encoding="w3cdtf">2007</copyrightDate></originInfo><language><languageTerm type="code" authority="rfc3066">en</languageTerm><languageTerm type="code" authority="iso639-2b">eng</languageTerm></language><physicalDescription><internetMediaType>text/html</internetMediaType></physicalDescription><abstract lang="en">Abstract: There are many styles for the narrative structure of a mathematical document. Each mathematician has its own conventions and traditions about labeling portions of texts (e.g., chapter, section, theorem or proof ) and identifying statements according to their logical importance (e.g., theorem is more important than lemma). Such narrative/structuring labels guide the reader’s navigation of the text and form the key components in the reasoning structure of the theory reflected in the text. We present in this paper a method to computerise the narrative structure of a text which includes the relationships between labeled text entities. These labels and relations are input by the user on top of their natural language text. This narrative structure is then automatically analysed to check its consistency. This automatic analysis consists of two phases: (1) checking the correct usage of labels and relations (i.e., that a ”proof” justifies a ”theorem” but cannot justify an ”axiom”) and (2) checking that the logical precedences in the document are self-consistent. The development of this method was driven by the experience of computerising a number of mathematical documents (covering different authoring styles). We illustrate how such computerised narrative structure could be used for further manipulations, i.e. to build a skeleton of a formal document in a formal system like Mizar, Coq or Isabelle.</abstract><relatedItem type="host"><titleInfo><title>Towards Mechanized Mathematical Assistants</title><subTitle>14th Symposium, Calculemus 2007, 6th International Conference, MKM 2007, Hagenberg, Austria, June 27-30, 2007. Proceedings</subTitle></titleInfo><name type="personal"><namePart type="given">Manuel</namePart><namePart type="family">Kauers</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Manfred</namePart><namePart type="family">Kerber</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Robert</namePart><namePart type="family">Miner</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Wolfgang</namePart><namePart type="family">Windsteiger</namePart><role><roleTerm type="text">editor</roleTerm></role></name><genre type="book-series" displayLabel="Proceedings"></genre><originInfo><copyrightDate encoding="w3cdtf">2007</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="I21017">Artificial Intelligence (incl. Robotics)</topic><topic authority="SpringerSubjectCodes" authorityURI="I18030">Data Mining and Knowledge Discovery</topic><topic authority="SpringerSubjectCodes" authorityURI="I18040">Information Systems Applications (incl.Internet)</topic><topic authority="SpringerSubjectCodes" authorityURI="I18024">Database Management</topic><topic authority="SpringerSubjectCodes" authorityURI="I13022">Computer Communication Networks</topic><topic authority="SpringerSubjectCodes" authorityURI="M00009">Mathematics, general</topic></subject><identifier type="DOI">10.1007/978-3-540-73086-6</identifier><identifier type="ISBN">978-3-540-73083-5</identifier><identifier type="eISBN">978-3-540-73086-6</identifier><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="BookTitleID">150455</identifier><identifier type="BookID">978-3-540-73086-6</identifier><identifier type="BookChapterCount">31</identifier><identifier type="BookVolumeNumber">4573</identifier><identifier type="BookSequenceNumber">4573</identifier><identifier type="PartChapterCount">21</identifier><part><date>2007</date><detail type="part"><title>Contributions to MKM 2007</title></detail><detail type="volume"><number>4573</number><caption>vol.</caption></detail><extent unit="pages"><start>296</start><end>312</end></extent></part><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2007</recordOrigin></recordInfo></relatedItem><relatedItem type="series"><titleInfo><title>Lecture Notes in Computer Science</title></titleInfo><originInfo><copyrightDate encoding="w3cdtf">2007</copyrightDate><issuance>serial</issuance></originInfo><relatedItem type="constituent"><titleInfo><title>Lecture Notes in Artificial Intelligence</title></titleInfo><name type="personal"><namePart type="given">Jaime</namePart><namePart type="given">G.</namePart><namePart type="family">Carbonell</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Jörg</namePart><namePart type="family">Siekmann</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Manuel</namePart><namePart type="family">Kauers</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Manfred</namePart><namePart type="family">Kerber</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Robert</namePart><namePart type="family">Miner</namePart><role><roleTerm type="text">editor</roleTerm></role></name><name type="personal"><namePart type="given">Wolfgang</namePart><namePart type="family">Windsteiger</namePart><role><roleTerm type="text">editor</roleTerm></role></name><genre type="sub-series"></genre><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SubSeriesID">1244</identifier></relatedItem><identifier type="ISSN">0302-9743</identifier><identifier type="eISSN">1611-3349</identifier><identifier type="SeriesID">558</identifier><recordInfo><recordOrigin>Springer-Verlag Berlin Heidelberg, 2007</recordOrigin></recordInfo></relatedItem><identifier type="istex">5928DA25C0C059A841D18103BC1854AF9743DC6B</identifier><identifier type="DOI">10.1007/978-3-540-73086-6_24</identifier><identifier type="ChapterID">24</identifier><identifier type="ChapterID">Chap24</identifier><accessCondition type="use and reproduction" contentType="copyright">Springer-Verlag Berlin Heidelberg, 2007</accessCondition><recordInfo><recordContentSource>SPRINGER</recordContentSource><recordOrigin>Springer-Verlag Berlin Heidelberg, 2007</recordOrigin></recordInfo></mods></metadata><enrichments><istex:refBibTEI uri="https://api.istex.fr/document/5928DA25C0C059A841D18103BC1854AF9743DC6B/enrichments/refBib"><teiHeader></teiHeader><text><front></front><body></body><back><listBibl><biblStruct xml:id="b0"><analytic><title level="a" type="main">The mathematical vernacular, a language for mathematics with typed sets</title><author><persName><forename type="first">N</forename><forename type="middle">G</forename><surname>De Bruijn</surname></persName></author></analytic><monogr><title level="m">Workshop on Programming Logic</title><meeting><address><addrLine>Sweden</addrLine></address></meeting><imprint><date type="published" when="1987"></date></imprint></monogr></biblStruct><biblStruct xml:id="b1"><analytic><title></title><author><persName><forename type="first">P</forename><forename type="middle">V</forename><surname>Biron</surname></persName></author><author><persName><forename type="first">A</forename><surname>Malhotra</surname></persName></author></analytic><monogr><title level="j">XML Schema Part Datatypes. W3C Recommendation</title><imprint><biblScope unit="volume">2</biblScope><date type="published" when="2001"></date></imprint></monogr></biblStruct><biblStruct xml:id="b2"><monogr><title level="m" type="main">MathLang: A new language for mathematics, logic, and proof checking. A research proposal to UK funding body</title><author><persName><forename type="first">F</forename><surname>Kamareddine</surname></persName></author><author><persName><forename type="first">J</forename><surname>Wells</surname></persName></author><imprint><date type="published" when="2001"></date></imprint></monogr></biblStruct><biblStruct xml:id="b3"><monogr><title level="m" type="main">Gradual computerisation/formalisation of mathematical texts into mizar</title><author><persName><forename type="first">F</forename><surname>Kamareddine</surname></persName></author><author><persName><forename type="first">M</forename><surname>Maarek</surname></persName></author><author><persName><forename type="first">K</forename><surname>Retel</surname></persName></author><author><persName><forename type="first">J</forename><forename type="middle">B</forename><surname>Wells</surname></persName></author><imprint><date type="published" when="2007"></date></imprint></monogr></biblStruct><biblStruct xml:id="b4"><analytic><title level="a" type="main">Restoring Natural Language as a</title><author><persName><forename type="first">F</forename><surname>Kamareddine</surname></persName></author><author><persName><forename type="first">R</forename><surname>Lamar</surname></persName></author><author><persName><forename type="first">M</forename><surname>Maarek</surname></persName></author><author><persName><forename type="first">J</forename><forename type="middle">B</forename><surname>Wells</surname></persName></author></analytic><monogr><title level="j">Computerised Mathematics Input Method</title><imprint><date type="published" when="2007"></date></imprint></monogr></biblStruct><biblStruct xml:id="b5"><analytic><title level="a" type="main">Toward an object-oriented structure for mathematical text</title><author><persName><forename type="first">F</forename><surname>Kamareddine</surname></persName></author><author><persName><forename type="first">M</forename><surname>Maarek</surname></persName></author><author><persName><forename type="first">J</forename><forename type="middle">B</forename><surname>Wells</surname></persName></author></analytic><monogr><title level="m">MKM 2005</title><editor>Kohlhase, M.</editor><meeting><address><addrLine>Heidelberg</addrLine></address></meeting><imprint><publisher>Springer</publisher><date type="published" when="2006"></date></imprint></monogr></biblStruct><biblStruct xml:id="b6"><analytic><title level="a" type="main">A refinement of de Bruijn's formal language of mathematics</title><author><persName><forename type="first">F</forename><surname>Kamareddine</surname></persName></author><author><persName><forename type="first">R</forename><surname>Nederpelt</surname></persName></author></analytic><monogr><title level="j">J. Logic Lang. Inform</title><imprint><biblScope unit="volume">13</biblScope><biblScope unit="issue">3</biblScope><biblScope unit="page" from="287" to="340"></biblScope><date type="published" when="2004"></date></imprint></monogr></biblStruct><biblStruct xml:id="b7"><analytic><title level="a" type="main">OMDoc – An Open Markup Format for Mathematical Documents [version 1.2]</title><author><persName><forename type="first">M</forename><surname>Kohlhase</surname></persName></author></analytic><monogr><title level="j">LNCS (LNAI)</title><imprint><publisher>Springer</publisher><publisher>Springer</publisher><biblScope unit="volume">4180</biblScope><date type="published" when="2006"></date></imprint></monogr></biblStruct><biblStruct xml:id="b8"><monogr><title level="m" type="main">SWiM – A Semantic Wiki for Mathematical Knowledge Management</title><author><persName><forename type="first">Ch</forename><surname>Lange</surname></persName></author><imprint><date type="published" when="2006-12"></date></imprint></monogr></biblStruct><biblStruct xml:id="b9"><analytic><title level="a" type="main">Resource Description Framework (RDF) Model and Syntax Specification</title><author><persName><forename type="first">O</forename><surname>Lassila</surname></persName></author><author><persName><forename type="first">R</forename><forename type="middle">R</forename><surname>Swick</surname></persName></author></analytic><monogr><title level="j">W3C Recommendation</title><imprint><date type="published" when="1999"></date></imprint></monogr></biblStruct><biblStruct xml:id="b10"><analytic><title level="a" type="main">OWL Web Ontology Language Overview</title><author><persName><forename type="first">D</forename><forename type="middle">L</forename><surname>Mcguinness</surname></persName></author><author><persName><forename type="first">F</forename><surname>Van Harmelen</surname></persName></author></analytic><monogr><title level="j">W3C Recommendation</title><imprint><date type="published" when="2004"></date></imprint></monogr></biblStruct><biblStruct xml:id="b11"><monogr><title level="m" type="main">General topology. Authors' notes, last visit 2007-02-25</title><author><persName><forename type="first">J</forename><forename type="middle">M</forename><surname>Moller</surname></persName></author><imprint></imprint></monogr></biblStruct><biblStruct xml:id="b12"><analytic><title level="a" type="main">Mathematical knowledge browser with automatic hyperlink detection</title><author><persName><forename type="first">K</forename><surname>Nakagawa</surname></persName></author><author><persName><forename type="first">M</forename><surname>Suzuki</surname></persName></author></analytic><monogr><title level="m">MKM 2005</title><editor>Kohlhase, M.</editor><meeting><address><addrLine>Heidelberg</addrLine></address></meeting><imprint><publisher>Springer</publisher><date type="published" when="2006"></date></imprint></monogr></biblStruct><biblStruct xml:id="b13"><analytic><title level="a" type="main">Extraction of Logical Structure from Articles in Mathematics</title><author><persName><forename type="first">K</forename><surname>Nakagawa</surname></persName></author><author><persName><forename type="first">A</forename><surname>Nomura</surname></persName></author><author><persName><forename type="first">M</forename><surname>Suzuki</surname></persName></author></analytic><monogr><title level="m">MKM 2005</title><editor>Kohlhase, M.</editor><meeting><address><addrLine>Heidelberg</addrLine></address></meeting><imprint><publisher>Springer</publisher><date type="published" when="2006"></date></imprint></monogr></biblStruct><biblStruct xml:id="b14"><analytic><title level="a" type="main">Transitivité et connexité</title><author><persName><forename type="first">B</forename><surname>Roy</surname></persName></author></analytic><monogr><title level="j">C. R. Acad. Sci. Paris</title><imprint><biblScope unit="volume">249</biblScope><biblScope unit="page" from="216" to="218"></biblScope><date type="published" when="1959"></date></imprint></monogr></biblStruct><biblStruct xml:id="b15"><analytic><title level="a" type="main">On equivalents of well-foundedness. An experiment in MIZAR</title><author><persName><forename type="first">P</forename><surname>Rudnicki</surname></persName></author><author><persName><forename type="first">A</forename><surname>Trybulec</surname></persName></author></analytic><monogr><title level="j">Journal of Automated Reasoning</title><imprint><biblScope unit="volume">2334</biblScope><biblScope unit="page" from="197" to="234"></biblScope><date type="published" when="1999"></date></imprint></monogr></biblStruct><biblStruct xml:id="b16"><monogr><title level="m" type="main">Elementary Theory of Numbers</title><author><persName><forename type="first">W</forename><surname>Sierpi´sierpi´nski</surname></persName></author><imprint><date type="published" when="1964"></date><publisher>PWN</publisher><pubPlace>Warszawa</pubPlace></imprint></monogr></biblStruct><biblStruct xml:id="b17"><analytic><title level="a" type="main">OWL Web Ontology Language Guide</title><author><persName><forename type="first">M</forename><forename type="middle">K</forename><surname>Smith</surname></persName></author><author><persName><surname>Welty</surname></persName></author><author><persName><surname>Ch</surname></persName></author><author><persName><forename type="first">D</forename><forename type="middle">L</forename><surname>Mcguinness</surname></persName></author></analytic><monogr><title level="j">W3C Recommendation</title><imprint><date type="published" when="2004"></date></imprint></monogr></biblStruct><biblStruct xml:id="b18"><analytic><title level="a" type="main">A theorem on boolean matrices</title><author><persName><forename type="first">S</forename><surname>Warshall</surname></persName></author></analytic><monogr><title level="j">J. ACM</title><imprint><biblScope unit="volume">9</biblScope><biblScope unit="issue">1</biblScope><biblScope unit="page" from="11" to="12"></biblScope><date type="published" when="1962"></date></imprint></monogr></biblStruct></listBibl></back></text></istex:refBibTEI><json:item><type>refBibs</type><uri>https://api.istex.fr/document/5928DA25C0C059A841D18103BC1854AF9743DC6B/enrichments/refBibs</uri></json:item></enrichments></istex></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Ticri/explor/TeiVM2/Data/Istex/Corpus
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 000434 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Istex/Corpus/biblio.hfd -nk 000434 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Ticri
|area= TeiVM2
|flux= Istex
|étape= Corpus
|type= RBID
|clé= ISTEX:5928DA25C0C059A841D18103BC1854AF9743DC6B
|texte= Narrative Structure of Mathematical Texts
}}
| This area was generated with Dilib version V0.6.31. |  |