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", 
      "Hyperlink Induced Topic Search", 
      "graph-based approach", 
      "captures semantics", 
      "document search", 
      "logical dependencies", 
      "topic search", 
      "theorem proving", 
      "link structure", 
      "mathematical content", 
      "search tool", 
      "relatedness information", 
      "formal mathematics", 
      "inherent structure", 
      "graph", 
      "data collection", 
      "semantics", 
      "HITS", 
      "information", 
      "Mowgli", 
      "library", 
      "theorem", 
      "search", 
      "proving", 
      "mathematics", 
      "nodes", 
      "collection", 
      "tool", 
      "FDL", 
      "approach", 
      "applications", 
      "dependency", 
      "potential applications", 
      "structure", 
      "example", 
      "definition", 
      "link", 
      "efforts", 
      "data", 
      "means", 
      "amount", 
      "values", 
      "active efforts", 
      "analysis", 
      "math", 
      "content", 
      "education", 
      "significance"
    ], 
    "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-05-20T07:42", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220519/entities/gbq_results/chapter/chapter_163.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.

147 TRIPLES      23 PREDICATES      76 URIs      67 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 Nd9c0365b44b348eaa8ad774fd5e8559d
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 N6cfdd3d212f649119a86eaaa1b9d4702
10 schema:genre chapter
11 schema:inLanguage en
12 schema:isAccessibleForFree true
13 schema:isPartOf Nbc5866a49bb242309e3f2e0a6fd8dd99
14 schema:keywords FDL
15 HITS
16 Hyperlink Induced Topic Search
17 Mowgli
18 active efforts
19 amount
20 analysis
21 applications
22 approach
23 captures semantics
24 collection
25 content
26 data
27 data collection
28 definition
29 dependency
30 digital libraries
31 document search
32 education
33 efforts
34 example
35 formal mathematics
36 graph
37 graph-based approach
38 information
39 inherent structure
40 library
41 link
42 link structure
43 logical dependencies
44 math
45 mathematical content
46 mathematics
47 means
48 nodes
49 potential applications
50 proving
51 relatedness information
52 search
53 search tool
54 semantics
55 significance
56 structure
57 theorem
58 theorem proving
59 tool
60 topic search
61 values
62 schema:name A Graph-Based Approach Towards Discerning Inherent Structures in a Digital Library of Formal Mathematics
63 schema:pagination 220-235
64 schema:productId N7244364a823546b7810321778da5377c
65 N7fc83578c39540dbb3f5067a4b47bfae
66 schema:publisher N8d2774aa5aa6477581327f15de2d5a83
67 schema:sameAs https://app.dimensions.ai/details/publication/pub.1033005674
68 https://doi.org/10.1007/978-3-540-27818-4_16
69 schema:sdDatePublished 2022-05-20T07:42
70 schema:sdLicense https://scigraph.springernature.com/explorer/license/
71 schema:sdPublisher Nc811e9406a054864b4f687c8b405d314
72 schema:url https://doi.org/10.1007/978-3-540-27818-4_16
73 sgo:license sg:explorer/license/
74 sgo:sdDataset chapters
75 rdf:type schema:Chapter
76 N61ea27e001b84d5ea4cd71ca1183e192 rdf:first N976462d3cfb84ceea82811b4091dd396
77 rdf:rest Nfcbda786292e44a9843641b72d3da64a
78 N6c3773ac749541d49dfb69c33b9123ba rdf:first sg:person.07707043675.63
79 rdf:rest N9488598a7f5c412abe79c09f510cba68
80 N6cfdd3d212f649119a86eaaa1b9d4702 rdf:first Ne5ae88be1b974683b029bfa2a5aa49a7
81 rdf:rest N61ea27e001b84d5ea4cd71ca1183e192
82 N6f28f28e229946d0812e03595eeca568 rdf:first sg:person.011522233557.04
83 rdf:rest N6c3773ac749541d49dfb69c33b9123ba
84 N7244364a823546b7810321778da5377c schema:name doi
85 schema:value 10.1007/978-3-540-27818-4_16
86 rdf:type schema:PropertyValue
87 N7fc83578c39540dbb3f5067a4b47bfae schema:name dimensions_id
88 schema:value pub.1033005674
89 rdf:type schema:PropertyValue
90 N87c3cd09cebc4c0d8b991759fecb6179 schema:familyName Trybulec
91 schema:givenName Andrzej
92 rdf:type schema:Person
93 N8d2774aa5aa6477581327f15de2d5a83 schema:name Springer Nature
94 rdf:type schema:Organisation
95 N9488598a7f5c412abe79c09f510cba68 rdf:first sg:person.01077226370.60
96 rdf:rest rdf:nil
97 N976462d3cfb84ceea82811b4091dd396 schema:familyName Bancerek
98 schema:givenName Grzegorz
99 rdf:type schema:Person
100 Nbc5866a49bb242309e3f2e0a6fd8dd99 schema:isbn 978-3-540-23029-8
101 978-3-540-27818-4
102 schema:name Mathematical Knowledge Management
103 rdf:type schema:Book
104 Nc811e9406a054864b4f687c8b405d314 schema:name Springer Nature - SN SciGraph project
105 rdf:type schema:Organization
106 Nd9c0365b44b348eaa8ad774fd5e8559d rdf:first sg:person.012263354457.22
107 rdf:rest N6f28f28e229946d0812e03595eeca568
108 Ne5ae88be1b974683b029bfa2a5aa49a7 schema:familyName Asperti
109 schema:givenName Andrea
110 rdf:type schema:Person
111 Nfcbda786292e44a9843641b72d3da64a rdf:first N87c3cd09cebc4c0d8b991759fecb6179
112 rdf:rest rdf:nil
113 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
114 schema:name Information and Computing Sciences
115 rdf:type schema:DefinedTerm
116 anzsrc-for:0801 schema:inDefinedTermSet anzsrc-for:
117 schema:name Artificial Intelligence and Image Processing
118 rdf:type schema:DefinedTerm
119 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
120 schema:name Computation Theory and Mathematics
121 rdf:type schema:DefinedTerm
122 anzsrc-for:0806 schema:inDefinedTermSet anzsrc-for:
123 schema:name Information Systems
124 rdf:type schema:DefinedTerm
125 sg:person.01077226370.60 schema:affiliation grid-institutes:grid.5386.8
126 schema:familyName Constable
127 schema:givenName Robert
128 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.01077226370.60
129 rdf:type schema:Person
130 sg:person.011522233557.04 schema:affiliation grid-institutes:grid.5386.8
131 schema:familyName Kleinberg
132 schema:givenName Jon
133 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011522233557.04
134 rdf:type schema:Person
135 sg:person.012263354457.22 schema:affiliation grid-institutes:grid.5386.8
136 schema:familyName Lorigo
137 schema:givenName Lori
138 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.012263354457.22
139 rdf:type schema:Person
140 sg:person.07707043675.63 schema:affiliation grid-institutes:grid.5386.8
141 schema:familyName Eaton
142 schema:givenName Richard
143 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.07707043675.63
144 rdf:type schema:Person
145 grid-institutes:grid.5386.8 schema:alternateName Department of Computer Science, Cornell University, Ithaca, NY, USA
146 schema:name Department of Computer Science, Cornell University, Ithaca, NY, USA
147 rdf:type schema:Organization
 




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


...