A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics View Full Text


Ontology type: schema:Chapter      Open Access: True


Chapter Info

DATE

2004

AUTHORS

Lori Lorigo , Jon Kleinberg , Richard Eaton , Robert Constable

ABSTRACT

As the amount of online formal mathematical content grows, for example through active efforts such as the Mathweb [21], MOWGLI [4], Formal Digital Library, or FDL [1], and others, it becomes increasingly valuable to find automated means to manage this data and capture semantics such as relatedness and significance. We apply graph-based approaches, such as HITS, or Hyperlink Induced Topic Search, [11] used for World Wide Web document search and analysis, to formal mathematical data collections. The nodes of the graphs we analyze are theorems and definitions, and the links are logical dependencies. By exploiting this link structure, we show how one may extract organizational and relatedness information from a collection of digital formal math. We discuss the value of the information we can extract, yielding potential applications in math search tools, theorem proving, and education. More... »

PAGES

220-235

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-3-540-27818-4_16

DOI

http://dx.doi.org/10.1007/978-3-540-27818-4_16

DIMENSIONS

https://app.dimensions.ai/details/publication/pub.1033005674


Indexing Status Check whether this publication has been indexed by Scopus and Web Of Science using the SN Indexing Status Tool
Incoming Citations Browse incoming citations for this publication using opencitations.net

JSON-LD is the canonical representation for SciGraph data.

TIP: You can open this SciGraph record using an external JSON-LD service: JSON-LD Playground Google SDTT

[
  {
    "@context": "https://springernature.github.io/scigraph/jsonld/sgcontext.json", 
    "about": [
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/08", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information and Computing Sciences", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0801", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Artificial Intelligence and Image Processing", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }, 
      {
        "id": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/0806", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Information Systems", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Cornell University, Ithaca, NY, USA", 
          "id": "http://www.grid.ac/institutes/grid.5386.8", 
          "name": [
            "Department of Computer Science, Cornell University, Ithaca, NY, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Lorigo", 
        "givenName": "Lori", 
        "id": "sg:person.012263354457.22", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012263354457.22"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Cornell University, Ithaca, NY, USA", 
          "id": "http://www.grid.ac/institutes/grid.5386.8", 
          "name": [
            "Department of Computer Science, Cornell University, Ithaca, NY, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Kleinberg", 
        "givenName": "Jon", 
        "id": "sg:person.011522233557.04", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011522233557.04"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Cornell University, Ithaca, NY, USA", 
          "id": "http://www.grid.ac/institutes/grid.5386.8", 
          "name": [
            "Department of Computer Science, Cornell University, Ithaca, NY, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Eaton", 
        "givenName": "Richard", 
        "id": "sg:person.07707043675.63", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07707043675.63"
        ], 
        "type": "Person"
      }, 
      {
        "affiliation": {
          "alternateName": "Department of Computer Science, Cornell University, Ithaca, NY, USA", 
          "id": "http://www.grid.ac/institutes/grid.5386.8", 
          "name": [
            "Department of Computer Science, Cornell University, Ithaca, NY, USA"
          ], 
          "type": "Organization"
        }, 
        "familyName": "Constable", 
        "givenName": "Robert", 
        "id": "sg:person.01077226370.60", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01077226370.60"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2004", 
    "datePublishedReg": "2004-01-01", 
    "description": "As the amount of online formal mathematical content grows, for example through active efforts such as the Mathweb [21], MOWGLI [4], Formal Digital Library, or FDL [1], and others, it becomes increasingly valuable to find automated means to manage this data and capture semantics such as relatedness and significance. We apply graph-based approaches, such as HITS, or Hyperlink Induced Topic Search, [11] used for World Wide Web document search and analysis, to formal mathematical data collections. The nodes of the graphs we analyze are theorems and definitions, and the links are logical dependencies. By exploiting this link structure, we show how one may extract organizational and relatedness information from a collection of digital formal math. We discuss the value of the information we can extract, yielding potential applications in math search tools, theorem proving, and education.", 
    "editor": [
      {
        "familyName": "Asperti", 
        "givenName": "Andrea", 
        "type": "Person"
      }, 
      {
        "familyName": "Bancerek", 
        "givenName": "Grzegorz", 
        "type": "Person"
      }, 
      {
        "familyName": "Trybulec", 
        "givenName": "Andrzej", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-3-540-27818-4_16", 
    "inLanguage": "en", 
    "isAccessibleForFree": true, 
    "isPartOf": {
      "isbn": [
        "978-3-540-23029-8", 
        "978-3-540-27818-4"
      ], 
      "name": "Mathematical Knowledge Management", 
      "type": "Book"
    }, 
    "keywords": [
      "digital libraries", 
      "Formal Digital Library", 
      "graph-based approach", 
      "captures semantics", 
      "document search", 
      "link structure", 
      "theorem proving", 
      "topic search", 
      "logical dependencies", 
      "search tools", 
      "relatedness information", 
      "formal mathematics", 
      "inherent structure", 
      "graph", 
      "formal math", 
      "data collection", 
      "MOWGLI", 
      "semantics", 
      "HITS", 
      "information", 
      "search", 
      "mathematical content", 
      "proving", 
      "library", 
      "nodes", 
      "collection", 
      "FDL", 
      "tool", 
      "applications", 
      "dependency", 
      "example", 
      "link", 
      "definition", 
      "mathematics", 
      "efforts", 
      "data", 
      "potential applications", 
      "structure", 
      "means", 
      "active efforts", 
      "amount", 
      "theorem", 
      "content", 
      "analysis", 
      "education", 
      "values", 
      "math", 
      "significance", 
      "approach", 
      "online formal mathematical content", 
      "formal mathematical content", 
      "Mathweb", 
      "Hyperlink Induced Topic Search", 
      "Induced Topic Search", 
      "World Wide Web document search", 
      "Wide Web document search", 
      "Web document search", 
      "formal mathematical data collections", 
      "mathematical data collections", 
      "digital formal math", 
      "math search tools"
    ], 
    "name": "A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics", 
    "pagination": "220-235", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1033005674"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-3-540-27818-4_16"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-3-540-27818-4_16", 
      "https://app.dimensions.ai/details/publication/pub.1033005674"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-01-01T19:11", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220101/entities/gbq_results/chapter/chapter_178.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-3-540-27818-4_16"
  }
]
 

Download the RDF metadata as:  json-ld nt turtle xml License info

HOW TO GET THIS DATA PROGRAMMATICALLY:

JSON-LD is a popular format for linked data which is fully compatible with JSON.

curl -H 'Accept: application/ld+json' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-27818-4_16'

N-Triples is a line-based linked data format ideal for batch operations.

curl -H 'Accept: application/n-triples' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-27818-4_16'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-27818-4_16'

RDF/XML is a standard XML format for linked data.

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-3-540-27818-4_16'


 

This table displays all metadata directly associated to this object as RDF triples.

160 TRIPLES      23 PREDICATES      89 URIs      80 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-3-540-27818-4_16 schema:about anzsrc-for:08
2 anzsrc-for:0801
3 anzsrc-for:0802
4 anzsrc-for:0806
5 schema:author N0f078615f6de46d48206361c2bda886a
6 schema:datePublished 2004
7 schema:datePublishedReg 2004-01-01
8 schema:description As the amount of online formal mathematical content grows, for example through active efforts such as the Mathweb [21], MOWGLI [4], Formal Digital Library, or FDL [1], and others, it becomes increasingly valuable to find automated means to manage this data and capture semantics such as relatedness and significance. We apply graph-based approaches, such as HITS, or Hyperlink Induced Topic Search, [11] used for World Wide Web document search and analysis, to formal mathematical data collections. The nodes of the graphs we analyze are theorems and definitions, and the links are logical dependencies. By exploiting this link structure, we show how one may extract organizational and relatedness information from a collection of digital formal math. We discuss the value of the information we can extract, yielding potential applications in math search tools, theorem proving, and education.
9 schema:editor N8f7681e2f22344458aa35cde1cc306b1
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf N140cb24754924373b2231efc630093d0
14 schema:keywords FDL
15 Formal Digital Library
16 HITS
17 Hyperlink Induced Topic Search
18 Induced Topic Search
19 MOWGLI
20 Mathweb
21 Web document search
22 Wide Web document search
23 World Wide Web document search
24 active efforts
25 amount
26 analysis
27 applications
28 approach
29 captures semantics
30 collection
31 content
32 data
33 data collection
34 definition
35 dependency
36 digital formal math
37 digital libraries
38 document search
39 education
40 efforts
41 example
42 formal math
43 formal mathematical content
44 formal mathematical data collections
45 formal mathematics
46 graph
47 graph-based approach
48 information
49 inherent structure
50 library
51 link
52 link structure
53 logical dependencies
54 math
55 math search tools
56 mathematical content
57 mathematical data collections
58 mathematics
59 means
60 nodes
61 online formal mathematical content
62 potential applications
63 proving
64 relatedness information
65 search
66 search tools
67 semantics
68 significance
69 structure
70 theorem
71 theorem proving
72 tool
73 topic search
74 values
75 schema:name A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics
76 schema:pagination 220-235
77 schema:productId N7b84a70e996b4c0284c31be42a8af397
78 Nef8b87dfb44941c5982113dd24fa3a63
79 schema:publisher N70e00253a7c94251b5b8f1d0abdae679
80 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033005674
81 https://doi.org/10.1007/978-3-540-27818-4_16
82 schema:sdDatePublished 2022-01-01T19:11
83 schema:sdLicense https://scigraph.springernature.com/explorer/license/
84 schema:sdPublisher N5ebb8a9b1556495d8f08c1792dd525d0
85 schema:url https://doi.org/10.1007/978-3-540-27818-4_16
86 sgo:license sg:explorer/license/
87 sgo:sdDataset chapters
88 rdf:type schema:Chapter
89 N0f078615f6de46d48206361c2bda886a rdf:first sg:person.012263354457.22
90 rdf:rest Ncac52291f9d944aea30894abf51fa672
91 N140cb24754924373b2231efc630093d0 schema:isbn 978-3-540-23029-8
92 978-3-540-27818-4
93 schema:name Mathematical Knowledge Management
94 rdf:type schema:Book
95 N27cf018433384e0faeab45b141b0021c rdf:first N3ac683ffd01b456e80a2a1b29f6ef892
96 rdf:rest Nc03e31d3aa3e4cc9804b27e2e4e810db
97 N3ac683ffd01b456e80a2a1b29f6ef892 schema:familyName Bancerek
98 schema:givenName Grzegorz
99 rdf:type schema:Person
100 N3b86a5efd7f1441eb9bb3514970d6e50 schema:familyName Asperti
101 schema:givenName Andrea
102 rdf:type schema:Person
103 N4bf4020066d5473f960ab30547ecda99 rdf:first sg:person.01077226370.60
104 rdf:rest rdf:nil
105 N4f59ec4e2ede4d8e9646bc56503212ab schema:familyName Trybulec
106 schema:givenName Andrzej
107 rdf:type schema:Person
108 N5ebb8a9b1556495d8f08c1792dd525d0 schema:name Springer Nature - SN SciGraph project
109 rdf:type schema:Organization
110 N70e00253a7c94251b5b8f1d0abdae679 schema:name Springer Nature
111 rdf:type schema:Organisation
112 N7b84a70e996b4c0284c31be42a8af397 schema:name doi
113 schema:value 10.1007/978-3-540-27818-4_16
114 rdf:type schema:PropertyValue
115 N8f7681e2f22344458aa35cde1cc306b1 rdf:first N3b86a5efd7f1441eb9bb3514970d6e50
116 rdf:rest N27cf018433384e0faeab45b141b0021c
117 Nbb3aedbb52604e7fb1af0b7a7e669153 rdf:first sg:person.07707043675.63
118 rdf:rest N4bf4020066d5473f960ab30547ecda99
119 Nc03e31d3aa3e4cc9804b27e2e4e810db rdf:first N4f59ec4e2ede4d8e9646bc56503212ab
120 rdf:rest rdf:nil
121 Ncac52291f9d944aea30894abf51fa672 rdf:first sg:person.011522233557.04
122 rdf:rest Nbb3aedbb52604e7fb1af0b7a7e669153
123 Nef8b87dfb44941c5982113dd24fa3a63 schema:name dimensions_id
124 schema:value pub.1033005674
125 rdf:type schema:PropertyValue
126 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
127 schema:name Information and Computing Sciences
128 rdf:type schema:DefinedTerm
129 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
130 schema:name Artificial Intelligence and Image Processing
131 rdf:type schema:DefinedTerm
132 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
133 schema:name Computation Theory and Mathematics
134 rdf:type schema:DefinedTerm
135 anzsrc-for:0806 schema:inDefinedTermSet anzsrc-for:
136 schema:name Information Systems
137 rdf:type schema:DefinedTerm
138 sg:person.01077226370.60 schema:affiliation grid-institutes:grid.5386.8
139 schema:familyName Constable
140 schema:givenName Robert
141 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01077226370.60
142 rdf:type schema:Person
143 sg:person.011522233557.04 schema:affiliation grid-institutes:grid.5386.8
144 schema:familyName Kleinberg
145 schema:givenName Jon
146 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011522233557.04
147 rdf:type schema:Person
148 sg:person.012263354457.22 schema:affiliation grid-institutes:grid.5386.8
149 schema:familyName Lorigo
150 schema:givenName Lori
151 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012263354457.22
152 rdf:type schema:Person
153 sg:person.07707043675.63 schema:affiliation grid-institutes:grid.5386.8
154 schema:familyName Eaton
155 schema:givenName Richard
156 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07707043675.63
157 rdf:type schema:Person
158 grid-institutes:grid.5386.8 schema:alternateName Department of Computer Science, Cornell University, Ithaca, NY, USA
159 schema:name Department of Computer Science, Cornell University, Ithaca, NY, USA
160 rdf:type schema:Organization
 




Preview window. Press ESC to close (or click here)


...