Automating change of representation for proofs in discrete mathematics Article Swipe
Daniel Raggi
,
Alan Bundy
,
Gudmund Grov
,
Alison Pease
·
YOU?
·
· 2015
· Open Access
·
· DOI: https://doi.org/10.48550/arxiv.1505.02449
YOU?
·
· 2015
· Open Access
·
· DOI: https://doi.org/10.48550/arxiv.1505.02449
Representation determines how we can reason about a specific problem. Sometimes one representation helps us find a proof more easily than others. Most current automated reasoning tools focus on reasoning within one representation. There is, therefore, a need for the development of better tools to mechanise and automate formal and logically sound changes of representation. In this paper we look at examples of representational transformations in discrete mathematics, and show how we have used Isabelle's Transfer tool to automate the use of these transformations in proofs. We give a brief overview of a general theory of transformations that we consider appropriate for thinking about the matter, and we explain how it relates to the Transfer package. We show our progress towards developing a general tactic that incorporates the automatic search for representation within the proving process.
Related Topics
Concepts
Metadata
- Type
- preprint
- Language
- en
- Landing Page
- http://arxiv.org/abs/1505.02449
- https://arxiv.org/pdf/1505.02449
- OA Status
- green
- References
- 3
- Related Works
- 20
- OpenAlex ID
- https://openalex.org/W2950168994
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W2950168994Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.48550/arxiv.1505.02449Digital Object Identifier
- Title
-
Automating change of representation for proofs in discrete mathematicsWork title
- Type
-
preprintOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2015Year of publication
- Publication date
-
2015-05-10Full publication date if available
- Authors
-
Daniel Raggi, Alan Bundy, Gudmund Grov, Alison PeaseList of authors in order
- Landing page
-
https://arxiv.org/abs/1505.02449Publisher landing page
- PDF URL
-
https://arxiv.org/pdf/1505.02449Direct link to full text PDF
- Open access
-
YesWhether a free full text is available
- OA status
-
greenOpen access status per OpenAlex
- OA URL
-
https://arxiv.org/pdf/1505.02449Direct OA link when available
- Concepts
-
Mathematical proof, Representation (politics), Computer science, Focus (optics), Process (computing), Theoretical computer science, Knowledge representation and reasoning, Programming language, Artificial intelligence, Mathematics, Optics, Physics, Politics, Law, Geometry, Political scienceTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
0Total citation count in OpenAlex
- References (count)
-
3Number of works referenced by this work
- Related works (count)
-
20Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W2950168994 |
|---|---|
| doi | https://doi.org/10.48550/arxiv.1505.02449 |
| ids.doi | https://doi.org/10.48550/arxiv.1505.02449 |
| ids.mag | 2950168994 |
| ids.openalex | https://openalex.org/W2950168994 |
| fwci | |
| type | preprint |
| title | Automating change of representation for proofs in discrete mathematics |
| biblio.issue | |
| biblio.volume | |
| biblio.last_page | |
| biblio.first_page | |
| topics[0].id | https://openalex.org/T10126 |
| topics[0].field.id | https://openalex.org/fields/17 |
| topics[0].field.display_name | Computer Science |
| topics[0].score | 0.9997000098228455 |
| topics[0].domain.id | https://openalex.org/domains/3 |
| topics[0].domain.display_name | Physical Sciences |
| topics[0].subfield.id | https://openalex.org/subfields/1702 |
| topics[0].subfield.display_name | Artificial Intelligence |
| topics[0].display_name | Logic, programming, and type systems |
| topics[1].id | https://openalex.org/T11010 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.9936000108718872 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1702 |
| topics[1].subfield.display_name | Artificial Intelligence |
| topics[1].display_name | Logic, Reasoning, and Knowledge |
| topics[2].id | https://openalex.org/T12002 |
| topics[2].field.id | https://openalex.org/fields/17 |
| topics[2].field.display_name | Computer Science |
| topics[2].score | 0.9846000075340271 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/1703 |
| topics[2].subfield.display_name | Computational Theory and Mathematics |
| topics[2].display_name | Computability, Logic, AI Algorithms |
| is_xpac | False |
| apc_list | |
| apc_paid | |
| concepts[0].id | https://openalex.org/C108710211 |
| concepts[0].level | 2 |
| concepts[0].score | 0.9150217771530151 |
| concepts[0].wikidata | https://www.wikidata.org/wiki/Q11538 |
| concepts[0].display_name | Mathematical proof |
| concepts[1].id | https://openalex.org/C2776359362 |
| concepts[1].level | 3 |
| concepts[1].score | 0.835556149482727 |
| concepts[1].wikidata | https://www.wikidata.org/wiki/Q2145286 |
| concepts[1].display_name | Representation (politics) |
| concepts[2].id | https://openalex.org/C41008148 |
| concepts[2].level | 0 |
| concepts[2].score | 0.6532576084136963 |
| concepts[2].wikidata | https://www.wikidata.org/wiki/Q21198 |
| concepts[2].display_name | Computer science |
| concepts[3].id | https://openalex.org/C192209626 |
| concepts[3].level | 2 |
| concepts[3].score | 0.562271773815155 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q190909 |
| concepts[3].display_name | Focus (optics) |
| concepts[4].id | https://openalex.org/C98045186 |
| concepts[4].level | 2 |
| concepts[4].score | 0.549228847026825 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q205663 |
| concepts[4].display_name | Process (computing) |
| concepts[5].id | https://openalex.org/C80444323 |
| concepts[5].level | 1 |
| concepts[5].score | 0.4854784309864044 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q2878974 |
| concepts[5].display_name | Theoretical computer science |
| concepts[6].id | https://openalex.org/C161301231 |
| concepts[6].level | 2 |
| concepts[6].score | 0.4761000871658325 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q3478658 |
| concepts[6].display_name | Knowledge representation and reasoning |
| concepts[7].id | https://openalex.org/C199360897 |
| concepts[7].level | 1 |
| concepts[7].score | 0.2903929352760315 |
| concepts[7].wikidata | https://www.wikidata.org/wiki/Q9143 |
| concepts[7].display_name | Programming language |
| concepts[8].id | https://openalex.org/C154945302 |
| concepts[8].level | 1 |
| concepts[8].score | 0.28546416759490967 |
| concepts[8].wikidata | https://www.wikidata.org/wiki/Q11660 |
| concepts[8].display_name | Artificial intelligence |
| concepts[9].id | https://openalex.org/C33923547 |
| concepts[9].level | 0 |
| concepts[9].score | 0.25839486718177795 |
| concepts[9].wikidata | https://www.wikidata.org/wiki/Q395 |
| concepts[9].display_name | Mathematics |
| concepts[10].id | https://openalex.org/C120665830 |
| concepts[10].level | 1 |
| concepts[10].score | 0.0 |
| concepts[10].wikidata | https://www.wikidata.org/wiki/Q14620 |
| concepts[10].display_name | Optics |
| concepts[11].id | https://openalex.org/C121332964 |
| concepts[11].level | 0 |
| concepts[11].score | 0.0 |
| concepts[11].wikidata | https://www.wikidata.org/wiki/Q413 |
| concepts[11].display_name | Physics |
| concepts[12].id | https://openalex.org/C94625758 |
| concepts[12].level | 2 |
| concepts[12].score | 0.0 |
| concepts[12].wikidata | https://www.wikidata.org/wiki/Q7163 |
| concepts[12].display_name | Politics |
| concepts[13].id | https://openalex.org/C199539241 |
| concepts[13].level | 1 |
| concepts[13].score | 0.0 |
| concepts[13].wikidata | https://www.wikidata.org/wiki/Q7748 |
| concepts[13].display_name | Law |
| concepts[14].id | https://openalex.org/C2524010 |
| concepts[14].level | 1 |
| concepts[14].score | 0.0 |
| concepts[14].wikidata | https://www.wikidata.org/wiki/Q8087 |
| concepts[14].display_name | Geometry |
| concepts[15].id | https://openalex.org/C17744445 |
| concepts[15].level | 0 |
| concepts[15].score | 0.0 |
| concepts[15].wikidata | https://www.wikidata.org/wiki/Q36442 |
| concepts[15].display_name | Political science |
| keywords[0].id | https://openalex.org/keywords/mathematical-proof |
| keywords[0].score | 0.9150217771530151 |
| keywords[0].display_name | Mathematical proof |
| keywords[1].id | https://openalex.org/keywords/representation |
| keywords[1].score | 0.835556149482727 |
| keywords[1].display_name | Representation (politics) |
| keywords[2].id | https://openalex.org/keywords/computer-science |
| keywords[2].score | 0.6532576084136963 |
| keywords[2].display_name | Computer science |
| keywords[3].id | https://openalex.org/keywords/focus |
| keywords[3].score | 0.562271773815155 |
| keywords[3].display_name | Focus (optics) |
| keywords[4].id | https://openalex.org/keywords/process |
| keywords[4].score | 0.549228847026825 |
| keywords[4].display_name | Process (computing) |
| keywords[5].id | https://openalex.org/keywords/theoretical-computer-science |
| keywords[5].score | 0.4854784309864044 |
| keywords[5].display_name | Theoretical computer science |
| keywords[6].id | https://openalex.org/keywords/knowledge-representation-and-reasoning |
| keywords[6].score | 0.4761000871658325 |
| keywords[6].display_name | Knowledge representation and reasoning |
| keywords[7].id | https://openalex.org/keywords/programming-language |
| keywords[7].score | 0.2903929352760315 |
| keywords[7].display_name | Programming language |
| keywords[8].id | https://openalex.org/keywords/artificial-intelligence |
| keywords[8].score | 0.28546416759490967 |
| keywords[8].display_name | Artificial intelligence |
| keywords[9].id | https://openalex.org/keywords/mathematics |
| keywords[9].score | 0.25839486718177795 |
| keywords[9].display_name | Mathematics |
| language | en |
| locations[0].id | pmh:oai:arXiv.org:1505.02449 |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S4306400194 |
| locations[0].source.issn | |
| locations[0].source.type | repository |
| locations[0].source.is_oa | True |
| locations[0].source.issn_l | |
| locations[0].source.is_core | False |
| locations[0].source.is_in_doaj | False |
| locations[0].source.display_name | arXiv (Cornell University) |
| locations[0].source.host_organization | https://openalex.org/I205783295 |
| locations[0].source.host_organization_name | Cornell University |
| locations[0].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[0].license | |
| locations[0].pdf_url | https://arxiv.org/pdf/1505.02449 |
| locations[0].version | submittedVersion |
| locations[0].raw_type | text |
| locations[0].license_id | |
| locations[0].is_accepted | False |
| locations[0].is_published | False |
| locations[0].raw_source_name | |
| locations[0].landing_page_url | http://arxiv.org/abs/1505.02449 |
| locations[1].id | mag:2950168994 |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306400194 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | True |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | arXiv (Cornell University) |
| locations[1].source.host_organization | https://openalex.org/I205783295 |
| locations[1].source.host_organization_name | Cornell University |
| locations[1].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[1].license | |
| locations[1].pdf_url | |
| locations[1].version | submittedVersion |
| locations[1].raw_type | |
| locations[1].license_id | |
| locations[1].is_accepted | False |
| locations[1].is_published | False |
| locations[1].raw_source_name | arXiv (Cornell University) |
| locations[1].landing_page_url | https://arxiv.org/pdf/1505.02449.pdf |
| locations[2].id | doi:10.48550/arxiv.1505.02449 |
| locations[2].is_oa | True |
| locations[2].source.id | https://openalex.org/S4306400194 |
| locations[2].source.issn | |
| locations[2].source.type | repository |
| locations[2].source.is_oa | True |
| locations[2].source.issn_l | |
| locations[2].source.is_core | False |
| locations[2].source.is_in_doaj | False |
| locations[2].source.display_name | arXiv (Cornell University) |
| locations[2].source.host_organization | https://openalex.org/I205783295 |
| locations[2].source.host_organization_name | Cornell University |
| locations[2].source.host_organization_lineage | https://openalex.org/I205783295 |
| locations[2].license | |
| locations[2].pdf_url | |
| locations[2].version | |
| locations[2].raw_type | article |
| locations[2].license_id | |
| locations[2].is_accepted | False |
| locations[2].is_published | |
| locations[2].raw_source_name | |
| locations[2].landing_page_url | https://doi.org/10.48550/arxiv.1505.02449 |
| indexed_in | arxiv, datacite |
| authorships[0].author.id | https://openalex.org/A5074686232 |
| authorships[0].author.orcid | https://orcid.org/0000-0002-9207-6621 |
| authorships[0].author.display_name | Daniel Raggi |
| authorships[0].countries | GB |
| authorships[0].affiliations[0].institution_ids | https://openalex.org/I98677209 |
| authorships[0].affiliations[0].raw_affiliation_string | School of Informatics University of Edinburgh Edinburgh, Scotland |
| authorships[0].institutions[0].id | https://openalex.org/I98677209 |
| authorships[0].institutions[0].ror | https://ror.org/01nrxwf90 |
| authorships[0].institutions[0].type | education |
| authorships[0].institutions[0].lineage | https://openalex.org/I98677209 |
| authorships[0].institutions[0].country_code | GB |
| authorships[0].institutions[0].display_name | University of Edinburgh |
| authorships[0].author_position | first |
| authorships[0].raw_author_name | Daniel Raggi |
| authorships[0].is_corresponding | False |
| authorships[0].raw_affiliation_strings | School of Informatics University of Edinburgh Edinburgh, Scotland |
| authorships[1].author.id | https://openalex.org/A5040311876 |
| authorships[1].author.orcid | https://orcid.org/0000-0002-0578-6474 |
| authorships[1].author.display_name | Alan Bundy |
| authorships[1].countries | GB |
| authorships[1].affiliations[0].institution_ids | https://openalex.org/I98677209 |
| authorships[1].affiliations[0].raw_affiliation_string | School of Informatics University of Edinburgh Edinburgh, Scotland |
| authorships[1].institutions[0].id | https://openalex.org/I98677209 |
| authorships[1].institutions[0].ror | https://ror.org/01nrxwf90 |
| authorships[1].institutions[0].type | education |
| authorships[1].institutions[0].lineage | https://openalex.org/I98677209 |
| authorships[1].institutions[0].country_code | GB |
| authorships[1].institutions[0].display_name | University of Edinburgh |
| authorships[1].author_position | middle |
| authorships[1].raw_author_name | Alan Bundy |
| authorships[1].is_corresponding | False |
| authorships[1].raw_affiliation_strings | School of Informatics University of Edinburgh Edinburgh, Scotland |
| authorships[2].author.id | https://openalex.org/A5077910506 |
| authorships[2].author.orcid | https://orcid.org/0000-0001-8837-5496 |
| authorships[2].author.display_name | Gudmund Grov |
| authorships[2].affiliations[0].raw_affiliation_string | School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, Scotland |
| authorships[2].author_position | middle |
| authorships[2].raw_author_name | Gudmund Grov |
| authorships[2].is_corresponding | False |
| authorships[2].raw_affiliation_strings | School of Mathematical and Computer Sciences, Heriot-Watt University, Edinburgh, Scotland |
| authorships[3].author.id | https://openalex.org/A5012487481 |
| authorships[3].author.orcid | https://orcid.org/0000-0003-1856-9599 |
| authorships[3].author.display_name | Alison Pease |
| authorships[3].countries | GB |
| authorships[3].affiliations[0].institution_ids | https://openalex.org/I177639307 |
| authorships[3].affiliations[0].raw_affiliation_string | School of Computing University of Dundee, Dundee, Scotland |
| authorships[3].institutions[0].id | https://openalex.org/I177639307 |
| authorships[3].institutions[0].ror | https://ror.org/03h2bxq36 |
| authorships[3].institutions[0].type | education |
| authorships[3].institutions[0].lineage | https://openalex.org/I177639307 |
| authorships[3].institutions[0].country_code | GB |
| authorships[3].institutions[0].display_name | University of Dundee |
| authorships[3].author_position | last |
| authorships[3].raw_author_name | Alison Pease |
| authorships[3].is_corresponding | False |
| authorships[3].raw_affiliation_strings | School of Computing University of Dundee, Dundee, Scotland |
| has_content.pdf | False |
| has_content.grobid_xml | False |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://arxiv.org/pdf/1505.02449 |
| open_access.oa_status | green |
| open_access.any_repository_has_fulltext | False |
| created_date | 2025-10-10T00:00:00 |
| display_name | Automating change of representation for proofs in discrete mathematics |
| has_fulltext | False |
| is_retracted | False |
| updated_date | 2025-11-06T06:51:31.235846 |
| primary_topic.id | https://openalex.org/T10126 |
| primary_topic.field.id | https://openalex.org/fields/17 |
| primary_topic.field.display_name | Computer Science |
| primary_topic.score | 0.9997000098228455 |
| primary_topic.domain.id | https://openalex.org/domains/3 |
| primary_topic.domain.display_name | Physical Sciences |
| primary_topic.subfield.id | https://openalex.org/subfields/1702 |
| primary_topic.subfield.display_name | Artificial Intelligence |
| primary_topic.display_name | Logic, programming, and type systems |
| related_works | https://openalex.org/W2069829906, https://openalex.org/W184558934, https://openalex.org/W2343048589, https://openalex.org/W1943070153, https://openalex.org/W2955107593, https://openalex.org/W2563839384, https://openalex.org/W1519609121, https://openalex.org/W374661910, https://openalex.org/W2096042113, https://openalex.org/W2137586949, https://openalex.org/W2640541807, https://openalex.org/W204383095, https://openalex.org/W2185769173, https://openalex.org/W1575107838, https://openalex.org/W3143432647, https://openalex.org/W1971240548, https://openalex.org/W2911255915, https://openalex.org/W1518266748, https://openalex.org/W2287696855, https://openalex.org/W1524257410 |
| cited_by_count | 0 |
| locations_count | 3 |
| best_oa_location.id | pmh:oai:arXiv.org:1505.02449 |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S4306400194 |
| best_oa_location.source.issn | |
| best_oa_location.source.type | repository |
| best_oa_location.source.is_oa | True |
| best_oa_location.source.issn_l | |
| best_oa_location.source.is_core | False |
| best_oa_location.source.is_in_doaj | False |
| best_oa_location.source.display_name | arXiv (Cornell University) |
| best_oa_location.source.host_organization | https://openalex.org/I205783295 |
| best_oa_location.source.host_organization_name | Cornell University |
| best_oa_location.source.host_organization_lineage | https://openalex.org/I205783295 |
| best_oa_location.license | |
| best_oa_location.pdf_url | https://arxiv.org/pdf/1505.02449 |
| best_oa_location.version | submittedVersion |
| best_oa_location.raw_type | text |
| best_oa_location.license_id | |
| best_oa_location.is_accepted | False |
| best_oa_location.is_published | False |
| best_oa_location.raw_source_name | |
| best_oa_location.landing_page_url | http://arxiv.org/abs/1505.02449 |
| primary_location.id | pmh:oai:arXiv.org:1505.02449 |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S4306400194 |
| primary_location.source.issn | |
| primary_location.source.type | repository |
| primary_location.source.is_oa | True |
| primary_location.source.issn_l | |
| primary_location.source.is_core | False |
| primary_location.source.is_in_doaj | False |
| primary_location.source.display_name | arXiv (Cornell University) |
| primary_location.source.host_organization | https://openalex.org/I205783295 |
| primary_location.source.host_organization_name | Cornell University |
| primary_location.source.host_organization_lineage | https://openalex.org/I205783295 |
| primary_location.license | |
| primary_location.pdf_url | https://arxiv.org/pdf/1505.02449 |
| primary_location.version | submittedVersion |
| primary_location.raw_type | text |
| primary_location.license_id | |
| primary_location.is_accepted | False |
| primary_location.is_published | False |
| primary_location.raw_source_name | |
| primary_location.landing_page_url | http://arxiv.org/abs/1505.02449 |
| publication_date | 2015-05-10 |
| publication_year | 2015 |
| referenced_works | https://openalex.org/W2106192381, https://openalex.org/W836255558, https://openalex.org/W2137810559 |
| referenced_works_count | 3 |
| abstract_inverted_index.a | 7, 16, 36, 88, 92, 122 |
| abstract_inverted_index.In | 55 |
| abstract_inverted_index.We | 86, 116 |
| abstract_inverted_index.at | 60 |
| abstract_inverted_index.in | 65, 84 |
| abstract_inverted_index.it | 110 |
| abstract_inverted_index.of | 41, 53, 62, 81, 91, 95 |
| abstract_inverted_index.on | 28 |
| abstract_inverted_index.to | 44, 77, 112 |
| abstract_inverted_index.us | 14 |
| abstract_inverted_index.we | 3, 58, 71, 98, 107 |
| abstract_inverted_index.and | 46, 49, 68, 106 |
| abstract_inverted_index.can | 4 |
| abstract_inverted_index.for | 38, 101, 130 |
| abstract_inverted_index.how | 2, 70, 109 |
| abstract_inverted_index.is, | 34 |
| abstract_inverted_index.one | 11, 31 |
| abstract_inverted_index.our | 118 |
| abstract_inverted_index.the | 39, 79, 104, 113, 127, 133 |
| abstract_inverted_index.use | 80 |
| abstract_inverted_index.Most | 22 |
| abstract_inverted_index.find | 15 |
| abstract_inverted_index.give | 87 |
| abstract_inverted_index.have | 72 |
| abstract_inverted_index.look | 59 |
| abstract_inverted_index.more | 18 |
| abstract_inverted_index.need | 37 |
| abstract_inverted_index.show | 69, 117 |
| abstract_inverted_index.than | 20 |
| abstract_inverted_index.that | 97, 125 |
| abstract_inverted_index.this | 56 |
| abstract_inverted_index.tool | 76 |
| abstract_inverted_index.used | 73 |
| abstract_inverted_index.There | 33 |
| abstract_inverted_index.about | 6, 103 |
| abstract_inverted_index.brief | 89 |
| abstract_inverted_index.focus | 27 |
| abstract_inverted_index.helps | 13 |
| abstract_inverted_index.paper | 57 |
| abstract_inverted_index.proof | 17 |
| abstract_inverted_index.sound | 51 |
| abstract_inverted_index.these | 82 |
| abstract_inverted_index.tools | 26, 43 |
| abstract_inverted_index.better | 42 |
| abstract_inverted_index.easily | 19 |
| abstract_inverted_index.formal | 48 |
| abstract_inverted_index.reason | 5 |
| abstract_inverted_index.search | 129 |
| abstract_inverted_index.tactic | 124 |
| abstract_inverted_index.theory | 94 |
| abstract_inverted_index.within | 30, 132 |
| abstract_inverted_index.changes | 52 |
| abstract_inverted_index.current | 23 |
| abstract_inverted_index.explain | 108 |
| abstract_inverted_index.general | 93, 123 |
| abstract_inverted_index.matter, | 105 |
| abstract_inverted_index.others. | 21 |
| abstract_inverted_index.proofs. | 85 |
| abstract_inverted_index.proving | 134 |
| abstract_inverted_index.relates | 111 |
| abstract_inverted_index.towards | 120 |
| abstract_inverted_index.Transfer | 75, 114 |
| abstract_inverted_index.automate | 47, 78 |
| abstract_inverted_index.consider | 99 |
| abstract_inverted_index.discrete | 66 |
| abstract_inverted_index.examples | 61 |
| abstract_inverted_index.overview | 90 |
| abstract_inverted_index.package. | 115 |
| abstract_inverted_index.problem. | 9 |
| abstract_inverted_index.process. | 135 |
| abstract_inverted_index.progress | 119 |
| abstract_inverted_index.specific | 8 |
| abstract_inverted_index.thinking | 102 |
| abstract_inverted_index.Sometimes | 10 |
| abstract_inverted_index.automated | 24 |
| abstract_inverted_index.automatic | 128 |
| abstract_inverted_index.logically | 50 |
| abstract_inverted_index.mechanise | 45 |
| abstract_inverted_index.reasoning | 25, 29 |
| abstract_inverted_index.Isabelle's | 74 |
| abstract_inverted_index.determines | 1 |
| abstract_inverted_index.developing | 121 |
| abstract_inverted_index.therefore, | 35 |
| abstract_inverted_index.appropriate | 100 |
| abstract_inverted_index.development | 40 |
| abstract_inverted_index.incorporates | 126 |
| abstract_inverted_index.mathematics, | 67 |
| abstract_inverted_index.Representation | 0 |
| abstract_inverted_index.representation | 12, 131 |
| abstract_inverted_index.representation. | 32, 54 |
| abstract_inverted_index.transformations | 64, 83, 96 |
| abstract_inverted_index.representational | 63 |
| cited_by_percentile_year | |
| countries_distinct_count | 1 |
| institutions_distinct_count | 4 |
| sustainable_development_goals[0].id | https://metadata.un.org/sdg/4 |
| sustainable_development_goals[0].score | 0.4399999976158142 |
| sustainable_development_goals[0].display_name | Quality Education |
| citation_normalized_percentile |