On the Practical Semantics of Mathematical Diagrams View Full Text


Ontology type: schema:Chapter     


Chapter Info

DATE

2002

AUTHORS

Dave Barker-Plummer , Sidney C. Bailin

ABSTRACT

This chapter describes our research into the way in which diagrams convey mathematical meaning. Through the development of an automated reasoning system, called &/GROVER, we have tried to discover how a diagram can convey the meaning of a proof. &/GROVER is a theorem-proving system that interprets diagrams as proof strategies. The diagrams are similar to those that a mathematician would draw informally when communicating the ideas of a proof. We have applied &/GROVER to obtain automatic proofs of three theorems that are beyond the reach of existing theorem-proving systems operating without such guidance. In the process, we have discovered some patterns in the way diagrams are used to convey mathematical reasoning strategies. Those patterns, and the ways in which &/GROVER takes advantage of them to prove theorems, are the focus of this chapter. More... »

PAGES

339-355

Book

TITLE

Diagrammatic Representation and Reasoning

ISBN

978-1-85233-242-6
978-1-4471-0109-3

Identifiers

URI

http://scigraph.springernature.com/pub.10.1007/978-1-4471-0109-3_19

DOI

http://dx.doi.org/10.1007/978-1-4471-0109-3_19

DIMENSIONS

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


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/0802", 
        "inDefinedTermSet": "http://purl.org/au-research/vocabulary/anzsrc-for/2008/", 
        "name": "Computation Theory and Mathematics", 
        "type": "DefinedTerm"
      }
    ], 
    "author": [
      {
        "familyName": "Barker-Plummer", 
        "givenName": "Dave", 
        "type": "Person"
      }, 
      {
        "familyName": "Bailin", 
        "givenName": "Sidney C.", 
        "id": "sg:person.011667755735.32", 
        "sameAs": [
          "https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011667755735.32"
        ], 
        "type": "Person"
      }
    ], 
    "datePublished": "2002", 
    "datePublishedReg": "2002-01-01", 
    "description": "This chapter describes our research into the way in which diagrams convey mathematical meaning. Through the development of an automated reasoning system, called &/GROVER, we have tried to discover how a diagram can convey the meaning of a proof. &/GROVER is a theorem-proving system that interprets diagrams as proof strategies. The diagrams are similar to those that a mathematician would draw informally when communicating the ideas of a proof. We have applied &/GROVER to obtain automatic proofs of three theorems that are beyond the reach of existing theorem-proving systems operating without such guidance. In the process, we have discovered some patterns in the way diagrams are used to convey mathematical reasoning strategies. Those patterns, and the ways in which &/GROVER takes advantage of them to prove theorems, are the focus of this chapter.", 
    "editor": [
      {
        "familyName": "Anderson", 
        "givenName": "Michael", 
        "type": "Person"
      }, 
      {
        "familyName": "Meyer", 
        "givenName": "Bernd", 
        "type": "Person"
      }, 
      {
        "familyName": "Olivier", 
        "givenName": "Patrick", 
        "type": "Person"
      }
    ], 
    "genre": "chapter", 
    "id": "sg:pub.10.1007/978-1-4471-0109-3_19", 
    "inLanguage": "en", 
    "isAccessibleForFree": false, 
    "isPartOf": {
      "isbn": [
        "978-1-85233-242-6", 
        "978-1-4471-0109-3"
      ], 
      "name": "Diagrammatic Representation and Reasoning", 
      "type": "Book"
    }, 
    "keywords": [
      "theorem-proving system", 
      "reasoning system", 
      "automatic proof", 
      "proof strategies", 
      "practical semantics", 
      "reasoning strategies", 
      "way diagrams", 
      "semantics", 
      "proof", 
      "system", 
      "mathematical diagrams", 
      "such guidance", 
      "mathematical meaning", 
      "way", 
      "diagram", 
      "idea", 
      "advantages", 
      "strategies", 
      "chapter", 
      "research", 
      "meaning", 
      "process", 
      "guidance", 
      "patterns", 
      "focus", 
      "theorem", 
      "development", 
      "mathematicians", 
      "reach"
    ], 
    "name": "On the Practical Semantics of Mathematical Diagrams", 
    "pagination": "339-355", 
    "productId": [
      {
        "name": "dimensions_id", 
        "type": "PropertyValue", 
        "value": [
          "pub.1027070067"
        ]
      }, 
      {
        "name": "doi", 
        "type": "PropertyValue", 
        "value": [
          "10.1007/978-1-4471-0109-3_19"
        ]
      }
    ], 
    "publisher": {
      "name": "Springer Nature", 
      "type": "Organisation"
    }, 
    "sameAs": [
      "https://doi.org/10.1007/978-1-4471-0109-3_19", 
      "https://app.dimensions.ai/details/publication/pub.1027070067"
    ], 
    "sdDataset": "chapters", 
    "sdDatePublished": "2022-06-01T22:37", 
    "sdLicense": "https://scigraph.springernature.com/explorer/license/", 
    "sdPublisher": {
      "name": "Springer Nature - SN SciGraph project", 
      "type": "Organization"
    }, 
    "sdSource": "s3://com-springernature-scigraph/baseset/20220601/entities/gbq_results/chapter/chapter_87.jsonl", 
    "type": "Chapter", 
    "url": "https://doi.org/10.1007/978-1-4471-0109-3_19"
  }
]
 

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-1-4471-0109-3_19'

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-1-4471-0109-3_19'

Turtle is a human-readable linked data format.

curl -H 'Accept: text/turtle' 'https://scigraph.springernature.com/pub.10.1007/978-1-4471-0109-3_19'

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

curl -H 'Accept: application/rdf+xml' 'https://scigraph.springernature.com/pub.10.1007/978-1-4471-0109-3_19'


 

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

100 TRIPLES      23 PREDICATES      54 URIs      47 LITERALS      7 BLANK NODES

Subject Predicate Object
1 sg:pub.10.1007/978-1-4471-0109-3_19 schema:about anzsrc-for:08
2 anzsrc-for:0802
3 schema:author N917f0e12543340508ed7dbf535484673
4 schema:datePublished 2002
5 schema:datePublishedReg 2002-01-01
6 schema:description This chapter describes our research into the way in which diagrams convey mathematical meaning. Through the development of an automated reasoning system, called &/GROVER, we have tried to discover how a diagram can convey the meaning of a proof. &/GROVER is a theorem-proving system that interprets diagrams as proof strategies. The diagrams are similar to those that a mathematician would draw informally when communicating the ideas of a proof. We have applied &/GROVER to obtain automatic proofs of three theorems that are beyond the reach of existing theorem-proving systems operating without such guidance. In the process, we have discovered some patterns in the way diagrams are used to convey mathematical reasoning strategies. Those patterns, and the ways in which &/GROVER takes advantage of them to prove theorems, are the focus of this chapter.
7 schema:editor Nab4f055501734166bca6057ce30252dd
8 schema:genre chapter
9 schema:inLanguage en
10 schema:isAccessibleForFree false
11 schema:isPartOf Nd4c89fdd078745f593488034d58171b7
12 schema:keywords advantages
13 automatic proof
14 chapter
15 development
16 diagram
17 focus
18 guidance
19 idea
20 mathematical diagrams
21 mathematical meaning
22 mathematicians
23 meaning
24 patterns
25 practical semantics
26 process
27 proof
28 proof strategies
29 reach
30 reasoning strategies
31 reasoning system
32 research
33 semantics
34 strategies
35 such guidance
36 system
37 theorem
38 theorem-proving system
39 way
40 way diagrams
41 schema:name On the Practical Semantics of Mathematical Diagrams
42 schema:pagination 339-355
43 schema:productId N4427acb430fb4325a7eeccbede9baa57
44 Nf846d533370746048a9de07480776591
45 schema:publisher Ne1381536cb6b4c09b308985fc5f263f7
46 schema:sameAs https://app.dimensions.ai/details/publication/pub.1027070067
47 https://doi.org/10.1007/978-1-4471-0109-3_19
48 schema:sdDatePublished 2022-06-01T22:37
49 schema:sdLicense https://scigraph.springernature.com/explorer/license/
50 schema:sdPublisher N111c95fa347940fc88f4a09db4fcef9c
51 schema:url https://doi.org/10.1007/978-1-4471-0109-3_19
52 sgo:license sg:explorer/license/
53 sgo:sdDataset chapters
54 rdf:type schema:Chapter
55 N111c95fa347940fc88f4a09db4fcef9c schema:name Springer Nature - SN SciGraph project
56 rdf:type schema:Organization
57 N4427acb430fb4325a7eeccbede9baa57 schema:name doi
58 schema:value 10.1007/978-1-4471-0109-3_19
59 rdf:type schema:PropertyValue
60 N582c08e814a5498e9f6dbdcfcf5a7082 schema:familyName Barker-Plummer
61 schema:givenName Dave
62 rdf:type schema:Person
63 N69b05563b6044bae8cb0c99f6b53e987 schema:familyName Anderson
64 schema:givenName Michael
65 rdf:type schema:Person
66 N917f0e12543340508ed7dbf535484673 rdf:first N582c08e814a5498e9f6dbdcfcf5a7082
67 rdf:rest Nab6328b52b654e339ce6f3271d329f23
68 Nab4f055501734166bca6057ce30252dd rdf:first N69b05563b6044bae8cb0c99f6b53e987
69 rdf:rest Nf017813e0bc34c129de1bd8164d38dac
70 Nab6328b52b654e339ce6f3271d329f23 rdf:first sg:person.011667755735.32
71 rdf:rest rdf:nil
72 Ncc6692f272ac4ae5af5a749b80ed139f schema:familyName Olivier
73 schema:givenName Patrick
74 rdf:type schema:Person
75 Nd4c89fdd078745f593488034d58171b7 schema:isbn 978-1-4471-0109-3
76 978-1-85233-242-6
77 schema:name Diagrammatic Representation and Reasoning
78 rdf:type schema:Book
79 Ne1381536cb6b4c09b308985fc5f263f7 schema:name Springer Nature
80 rdf:type schema:Organisation
81 Nef9b4fb5548a4cc3b44c158d166910a5 rdf:first Ncc6692f272ac4ae5af5a749b80ed139f
82 rdf:rest rdf:nil
83 Nf017813e0bc34c129de1bd8164d38dac rdf:first Nf88c5ea0c15649438af2b0018bd654fc
84 rdf:rest Nef9b4fb5548a4cc3b44c158d166910a5
85 Nf846d533370746048a9de07480776591 schema:name dimensions_id
86 schema:value pub.1027070067
87 rdf:type schema:PropertyValue
88 Nf88c5ea0c15649438af2b0018bd654fc schema:familyName Meyer
89 schema:givenName Bernd
90 rdf:type schema:Person
91 anzsrc-for:08 schema:inDefinedTermSet anzsrc-for:
92 schema:name Information and Computing Sciences
93 rdf:type schema:DefinedTerm
94 anzsrc-for:0802 schema:inDefinedTermSet anzsrc-for:
95 schema:name Computation Theory and Mathematics
96 rdf:type schema:DefinedTerm
97 sg:person.011667755735.32 schema:familyName Bailin
98 schema:givenName Sidney C.
99 schema:sameAs https://app.dimensions.ai/discover/publication?and_facet_researcher=ur.011667755735.32
100 rdf:type schema:Person
 




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


...