Automating Change of Representation for Proofs in Discrete Mathematics (Extended Version) Article Swipe
Daniel Raggi
,
Alan Bundy
,
Gudmund Grov
,
Alison Pease
·
YOU?
·
· 2016
· Open Access
·
· DOI: https://doi.org/10.1007/s11786-016-0275-z
YOU?
·
· 2016
· Open Access
·
· DOI: https://doi.org/10.1007/s11786-016-0275-z
Representation determines how we can reason about a specific problem. Sometimes one representation helps us to 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 tools from Isabelle’s Transfer package to automate the use of these transformations in proofs. We give an 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 a few reasoning tactics we developed in Isabelle to improve the use of transformations, including the automation of search in the space of representations. We present and analyse some results of the use of these tactics.
Related Topics
Concepts
Mathematical proof
Representation (politics)
Computer science
Focus (optics)
Knowledge representation and reasoning
Automation
Theoretical computer science
Automated reasoning
Artificial intelligence
Mathematics
Engineering
Optics
Physics
Geometry
Law
Mechanical engineering
Politics
Political science
Metadata
- Type
- article
- Language
- en
- Landing Page
- https://doi.org/10.1007/s11786-016-0275-z
- https://link.springer.com/content/pdf/10.1007%2Fs11786-016-0275-z.pdf
- OA Status
- hybrid
- Cited By
- 5
- References
- 28
- Related Works
- 10
- OpenAlex ID
- https://openalex.org/W2417291013
All OpenAlex metadata
Raw OpenAlex JSON
- OpenAlex ID
-
https://openalex.org/W2417291013Canonical identifier for this work in OpenAlex
- DOI
-
https://doi.org/10.1007/s11786-016-0275-zDigital Object Identifier
- Title
-
Automating Change of Representation for Proofs in Discrete Mathematics (Extended Version)Work title
- Type
-
articleOpenAlex work type
- Language
-
enPrimary language
- Publication year
-
2016Year of publication
- Publication date
-
2016-07-18Full publication date if available
- Authors
-
Daniel Raggi, Alan Bundy, Gudmund Grov, Alison PeaseList of authors in order
- Landing page
-
https://doi.org/10.1007/s11786-016-0275-zPublisher landing page
- PDF URL
-
https://link.springer.com/content/pdf/10.1007%2Fs11786-016-0275-z.pdfDirect link to full text PDF
- Open access
-
YesWhether a free full text is available
- OA status
-
hybridOpen access status per OpenAlex
- OA URL
-
https://link.springer.com/content/pdf/10.1007%2Fs11786-016-0275-z.pdfDirect OA link when available
- Concepts
-
Mathematical proof, Representation (politics), Computer science, Focus (optics), Knowledge representation and reasoning, Automation, Theoretical computer science, Automated reasoning, Artificial intelligence, Mathematics, Engineering, Optics, Physics, Geometry, Law, Mechanical engineering, Politics, Political scienceTop concepts (fields/topics) attached by OpenAlex
- Cited by
-
5Total citation count in OpenAlex
- Citations by year (recent)
-
2024: 1, 2021: 1, 2020: 1, 2019: 1, 2017: 1Per-year citation counts (last 5 years)
- References (count)
-
28Number of works referenced by this work
- Related works (count)
-
10Other works algorithmically related by OpenAlex
Full payload
| id | https://openalex.org/W2417291013 |
|---|---|
| doi | https://doi.org/10.1007/s11786-016-0275-z |
| ids.doi | https://doi.org/10.1007/s11786-016-0275-z |
| ids.mag | 2417291013 |
| ids.openalex | https://openalex.org/W2417291013 |
| fwci | 0.56375376 |
| type | article |
| title | Automating Change of Representation for Proofs in Discrete Mathematics (Extended Version) |
| awards[0].id | https://openalex.org/G6835337725 |
| awards[0].funder_id | https://openalex.org/F4320334627 |
| awards[0].display_name | |
| awards[0].funder_award_id | EP/N014758/1 |
| awards[0].funder_display_name | Engineering and Physical Sciences Research Council |
| biblio.issue | 4 |
| biblio.volume | 10 |
| biblio.last_page | 457 |
| biblio.first_page | 429 |
| 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.9994999766349792 |
| 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/T12002 |
| topics[1].field.id | https://openalex.org/fields/17 |
| topics[1].field.display_name | Computer Science |
| topics[1].score | 0.993399977684021 |
| topics[1].domain.id | https://openalex.org/domains/3 |
| topics[1].domain.display_name | Physical Sciences |
| topics[1].subfield.id | https://openalex.org/subfields/1703 |
| topics[1].subfield.display_name | Computational Theory and Mathematics |
| topics[1].display_name | Computability, Logic, AI Algorithms |
| topics[2].id | https://openalex.org/T11010 |
| topics[2].field.id | https://openalex.org/fields/17 |
| topics[2].field.display_name | Computer Science |
| topics[2].score | 0.993399977684021 |
| topics[2].domain.id | https://openalex.org/domains/3 |
| topics[2].domain.display_name | Physical Sciences |
| topics[2].subfield.id | https://openalex.org/subfields/1702 |
| topics[2].subfield.display_name | Artificial Intelligence |
| topics[2].display_name | Logic, Reasoning, and Knowledge |
| funders[0].id | https://openalex.org/F4320320332 |
| funders[0].ror | https://ror.org/01nrxwf90 |
| funders[0].display_name | University of Edinburgh |
| funders[1].id | https://openalex.org/F4320334627 |
| funders[1].ror | https://ror.org/0439y7842 |
| funders[1].display_name | Engineering and Physical Sciences Research Council |
| is_xpac | False |
| apc_list.value | 2390 |
| apc_list.currency | EUR |
| apc_list.value_usd | 2990 |
| apc_paid.value | 2390 |
| apc_paid.currency | EUR |
| apc_paid.value_usd | 2990 |
| concepts[0].id | https://openalex.org/C108710211 |
| concepts[0].level | 2 |
| concepts[0].score | 0.8987952470779419 |
| 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.7809207439422607 |
| 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.6373215913772583 |
| 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.5605373978614807 |
| concepts[3].wikidata | https://www.wikidata.org/wiki/Q190909 |
| concepts[3].display_name | Focus (optics) |
| concepts[4].id | https://openalex.org/C161301231 |
| concepts[4].level | 2 |
| concepts[4].score | 0.5398520827293396 |
| concepts[4].wikidata | https://www.wikidata.org/wiki/Q3478658 |
| concepts[4].display_name | Knowledge representation and reasoning |
| concepts[5].id | https://openalex.org/C115901376 |
| concepts[5].level | 2 |
| concepts[5].score | 0.5341013669967651 |
| concepts[5].wikidata | https://www.wikidata.org/wiki/Q184199 |
| concepts[5].display_name | Automation |
| concepts[6].id | https://openalex.org/C80444323 |
| concepts[6].level | 1 |
| concepts[6].score | 0.5006649494171143 |
| concepts[6].wikidata | https://www.wikidata.org/wiki/Q2878974 |
| concepts[6].display_name | Theoretical computer science |
| concepts[7].id | https://openalex.org/C195344581 |
| concepts[7].level | 2 |
| concepts[7].score | 0.429749995470047 |
| concepts[7].wikidata | https://www.wikidata.org/wiki/Q2555318 |
| concepts[7].display_name | Automated reasoning |
| concepts[8].id | https://openalex.org/C154945302 |
| concepts[8].level | 1 |
| concepts[8].score | 0.3026762306690216 |
| 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.25609493255615234 |
| concepts[9].wikidata | https://www.wikidata.org/wiki/Q395 |
| concepts[9].display_name | Mathematics |
| concepts[10].id | https://openalex.org/C127413603 |
| concepts[10].level | 0 |
| concepts[10].score | 0.0 |
| concepts[10].wikidata | https://www.wikidata.org/wiki/Q11023 |
| concepts[10].display_name | Engineering |
| concepts[11].id | https://openalex.org/C120665830 |
| concepts[11].level | 1 |
| concepts[11].score | 0.0 |
| concepts[11].wikidata | https://www.wikidata.org/wiki/Q14620 |
| concepts[11].display_name | Optics |
| concepts[12].id | https://openalex.org/C121332964 |
| concepts[12].level | 0 |
| concepts[12].score | 0.0 |
| concepts[12].wikidata | https://www.wikidata.org/wiki/Q413 |
| concepts[12].display_name | Physics |
| concepts[13].id | https://openalex.org/C2524010 |
| concepts[13].level | 1 |
| concepts[13].score | 0.0 |
| concepts[13].wikidata | https://www.wikidata.org/wiki/Q8087 |
| concepts[13].display_name | Geometry |
| concepts[14].id | https://openalex.org/C199539241 |
| concepts[14].level | 1 |
| concepts[14].score | 0.0 |
| concepts[14].wikidata | https://www.wikidata.org/wiki/Q7748 |
| concepts[14].display_name | Law |
| concepts[15].id | https://openalex.org/C78519656 |
| concepts[15].level | 1 |
| concepts[15].score | 0.0 |
| concepts[15].wikidata | https://www.wikidata.org/wiki/Q101333 |
| concepts[15].display_name | Mechanical engineering |
| concepts[16].id | https://openalex.org/C94625758 |
| concepts[16].level | 2 |
| concepts[16].score | 0.0 |
| concepts[16].wikidata | https://www.wikidata.org/wiki/Q7163 |
| concepts[16].display_name | Politics |
| concepts[17].id | https://openalex.org/C17744445 |
| concepts[17].level | 0 |
| concepts[17].score | 0.0 |
| concepts[17].wikidata | https://www.wikidata.org/wiki/Q36442 |
| concepts[17].display_name | Political science |
| keywords[0].id | https://openalex.org/keywords/mathematical-proof |
| keywords[0].score | 0.8987952470779419 |
| keywords[0].display_name | Mathematical proof |
| keywords[1].id | https://openalex.org/keywords/representation |
| keywords[1].score | 0.7809207439422607 |
| keywords[1].display_name | Representation (politics) |
| keywords[2].id | https://openalex.org/keywords/computer-science |
| keywords[2].score | 0.6373215913772583 |
| keywords[2].display_name | Computer science |
| keywords[3].id | https://openalex.org/keywords/focus |
| keywords[3].score | 0.5605373978614807 |
| keywords[3].display_name | Focus (optics) |
| keywords[4].id | https://openalex.org/keywords/knowledge-representation-and-reasoning |
| keywords[4].score | 0.5398520827293396 |
| keywords[4].display_name | Knowledge representation and reasoning |
| keywords[5].id | https://openalex.org/keywords/automation |
| keywords[5].score | 0.5341013669967651 |
| keywords[5].display_name | Automation |
| keywords[6].id | https://openalex.org/keywords/theoretical-computer-science |
| keywords[6].score | 0.5006649494171143 |
| keywords[6].display_name | Theoretical computer science |
| keywords[7].id | https://openalex.org/keywords/automated-reasoning |
| keywords[7].score | 0.429749995470047 |
| keywords[7].display_name | Automated reasoning |
| keywords[8].id | https://openalex.org/keywords/artificial-intelligence |
| keywords[8].score | 0.3026762306690216 |
| keywords[8].display_name | Artificial intelligence |
| keywords[9].id | https://openalex.org/keywords/mathematics |
| keywords[9].score | 0.25609493255615234 |
| keywords[9].display_name | Mathematics |
| language | en |
| locations[0].id | doi:10.1007/s11786-016-0275-z |
| locations[0].is_oa | True |
| locations[0].source.id | https://openalex.org/S136038430 |
| locations[0].source.issn | 1661-8270, 1661-8289 |
| locations[0].source.type | journal |
| locations[0].source.is_oa | False |
| locations[0].source.issn_l | 1661-8270 |
| locations[0].source.is_core | True |
| locations[0].source.is_in_doaj | False |
| locations[0].source.display_name | Mathematics in Computer Science |
| locations[0].source.host_organization | https://openalex.org/P4310320186 |
| locations[0].source.host_organization_name | Birkhäuser |
| locations[0].source.host_organization_lineage | https://openalex.org/P4310320186, https://openalex.org/P4310319900 |
| locations[0].source.host_organization_lineage_names | Birkhäuser, Springer Science+Business Media |
| locations[0].license | cc-by |
| locations[0].pdf_url | https://link.springer.com/content/pdf/10.1007%2Fs11786-016-0275-z.pdf |
| locations[0].version | publishedVersion |
| locations[0].raw_type | journal-article |
| locations[0].license_id | https://openalex.org/licenses/cc-by |
| locations[0].is_accepted | True |
| locations[0].is_published | True |
| locations[0].raw_source_name | Mathematics in Computer Science |
| locations[0].landing_page_url | https://doi.org/10.1007/s11786-016-0275-z |
| locations[1].id | pmh:oai:discovery.dundee.ac.uk:openaire/798aaeab-b3d8-4347-89ab-75196c199967 |
| locations[1].is_oa | True |
| locations[1].source.id | https://openalex.org/S4306400523 |
| locations[1].source.issn | |
| locations[1].source.type | repository |
| locations[1].source.is_oa | False |
| locations[1].source.issn_l | |
| locations[1].source.is_core | False |
| locations[1].source.is_in_doaj | False |
| locations[1].source.display_name | Discovery Research Portal (University of Dundee) |
| locations[1].source.host_organization | https://openalex.org/I177639307 |
| locations[1].source.host_organization_name | University of Dundee |
| locations[1].source.host_organization_lineage | https://openalex.org/I177639307 |
| locations[1].license | cc-by |
| locations[1].pdf_url | |
| locations[1].version | publishedVersion |
| locations[1].raw_type | info:eu-repo/semantics/publishedVersion |
| locations[1].license_id | https://openalex.org/licenses/cc-by |
| locations[1].is_accepted | True |
| locations[1].is_published | True |
| locations[1].raw_source_name | Raggi, D, Bundy, A, Grov, G & Pease, A 2016, 'Automating Change of Representation for Proofs in Discrete Mathematics (Extended Version)', Mathematics in Computer Science, vol. 10, no. 4, pp. 1-29. https://doi.org/10.1007/s11786-016-0275-z |
| locations[1].landing_page_url | https://discovery.dundee.ac.uk/en/publications/798aaeab-b3d8-4347-89ab-75196c199967 |
| locations[2].id | pmh:oai:pure.ed.ac.uk:publications/d1f5df58-7190-4051-b20c-e26c4682cee2 |
| locations[2].is_oa | False |
| locations[2].source.id | https://openalex.org/S4306400320 |
| locations[2].source.issn | |
| locations[2].source.type | repository |
| locations[2].source.is_oa | False |
| locations[2].source.issn_l | |
| locations[2].source.is_core | False |
| locations[2].source.is_in_doaj | False |
| locations[2].source.display_name | Edinburgh Research Explorer (University of Edinburgh) |
| locations[2].source.host_organization | https://openalex.org/I98677209 |
| locations[2].source.host_organization_name | University of Edinburgh |
| locations[2].source.host_organization_lineage | https://openalex.org/I98677209 |
| locations[2].license | |
| locations[2].pdf_url | |
| locations[2].version | submittedVersion |
| locations[2].raw_type | |
| locations[2].license_id | |
| locations[2].is_accepted | False |
| locations[2].is_published | False |
| locations[2].raw_source_name | |
| locations[2].landing_page_url | https://www.research.ed.ac.uk/portal/en/publications/automating-change-of-representation-for-proofs-in-discrete-mathematics-extended-version(d1f5df58-7190-4051-b20c-e26c4682cee2).html |
| indexed_in | crossref |
| 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, UK |
| 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, UK |
| has_content.pdf | True |
| has_content.grobid_xml | True |
| is_paratext | False |
| open_access.is_oa | True |
| open_access.oa_url | https://link.springer.com/content/pdf/10.1007%2Fs11786-016-0275-z.pdf |
| open_access.oa_status | hybrid |
| 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 (Extended Version) |
| has_fulltext | True |
| is_retracted | False |
| updated_date | 2025-11-06T03:46:38.306776 |
| 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.9994999766349792 |
| 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/W4394650907, https://openalex.org/W4307308174, https://openalex.org/W2399825514, https://openalex.org/W2004116709, https://openalex.org/W1864329966, https://openalex.org/W1088905, https://openalex.org/W1580558463, https://openalex.org/W1529147315, https://openalex.org/W2736582448, https://openalex.org/W846065076 |
| cited_by_count | 5 |
| counts_by_year[0].year | 2024 |
| counts_by_year[0].cited_by_count | 1 |
| counts_by_year[1].year | 2021 |
| counts_by_year[1].cited_by_count | 1 |
| counts_by_year[2].year | 2020 |
| counts_by_year[2].cited_by_count | 1 |
| counts_by_year[3].year | 2019 |
| counts_by_year[3].cited_by_count | 1 |
| counts_by_year[4].year | 2017 |
| counts_by_year[4].cited_by_count | 1 |
| locations_count | 3 |
| best_oa_location.id | doi:10.1007/s11786-016-0275-z |
| best_oa_location.is_oa | True |
| best_oa_location.source.id | https://openalex.org/S136038430 |
| best_oa_location.source.issn | 1661-8270, 1661-8289 |
| best_oa_location.source.type | journal |
| best_oa_location.source.is_oa | False |
| best_oa_location.source.issn_l | 1661-8270 |
| best_oa_location.source.is_core | True |
| best_oa_location.source.is_in_doaj | False |
| best_oa_location.source.display_name | Mathematics in Computer Science |
| best_oa_location.source.host_organization | https://openalex.org/P4310320186 |
| best_oa_location.source.host_organization_name | Birkhäuser |
| best_oa_location.source.host_organization_lineage | https://openalex.org/P4310320186, https://openalex.org/P4310319900 |
| best_oa_location.source.host_organization_lineage_names | Birkhäuser, Springer Science+Business Media |
| best_oa_location.license | cc-by |
| best_oa_location.pdf_url | https://link.springer.com/content/pdf/10.1007%2Fs11786-016-0275-z.pdf |
| best_oa_location.version | publishedVersion |
| best_oa_location.raw_type | journal-article |
| best_oa_location.license_id | https://openalex.org/licenses/cc-by |
| best_oa_location.is_accepted | True |
| best_oa_location.is_published | True |
| best_oa_location.raw_source_name | Mathematics in Computer Science |
| best_oa_location.landing_page_url | https://doi.org/10.1007/s11786-016-0275-z |
| primary_location.id | doi:10.1007/s11786-016-0275-z |
| primary_location.is_oa | True |
| primary_location.source.id | https://openalex.org/S136038430 |
| primary_location.source.issn | 1661-8270, 1661-8289 |
| primary_location.source.type | journal |
| primary_location.source.is_oa | False |
| primary_location.source.issn_l | 1661-8270 |
| primary_location.source.is_core | True |
| primary_location.source.is_in_doaj | False |
| primary_location.source.display_name | Mathematics in Computer Science |
| primary_location.source.host_organization | https://openalex.org/P4310320186 |
| primary_location.source.host_organization_name | Birkhäuser |
| primary_location.source.host_organization_lineage | https://openalex.org/P4310320186, https://openalex.org/P4310319900 |
| primary_location.source.host_organization_lineage_names | Birkhäuser, Springer Science+Business Media |
| primary_location.license | cc-by |
| primary_location.pdf_url | https://link.springer.com/content/pdf/10.1007%2Fs11786-016-0275-z.pdf |
| primary_location.version | publishedVersion |
| primary_location.raw_type | journal-article |
| primary_location.license_id | https://openalex.org/licenses/cc-by |
| primary_location.is_accepted | True |
| primary_location.is_published | True |
| primary_location.raw_source_name | Mathematics in Computer Science |
| primary_location.landing_page_url | https://doi.org/10.1007/s11786-016-0275-z |
| publication_date | 2016-07-18 |
| publication_year | 2016 |
| referenced_works | https://openalex.org/W1532290481, https://openalex.org/W1595209293, https://openalex.org/W1599039905, https://openalex.org/W4250463917, https://openalex.org/W1507441114, https://openalex.org/W2914153160, https://openalex.org/W2137810559, https://openalex.org/W2010883554, https://openalex.org/W1713610, https://openalex.org/W2146104088, https://openalex.org/W101424827, https://openalex.org/W2059311907, https://openalex.org/W2144280226, https://openalex.org/W2791394679, https://openalex.org/W1979623128, https://openalex.org/W1515857575, https://openalex.org/W4250846042, https://openalex.org/W2184900131, https://openalex.org/W4233121052, https://openalex.org/W2047769863, https://openalex.org/W6634049985, https://openalex.org/W121805954, https://openalex.org/W1599335667, https://openalex.org/W836255558, https://openalex.org/W2106192381, https://openalex.org/W1555979208, https://openalex.org/W1649012353, https://openalex.org/W1653213632 |
| referenced_works_count | 28 |
| abstract_inverted_index.a | 7, 17, 37, 94, 120 |
| abstract_inverted_index.In | 56 |
| abstract_inverted_index.We | 89, 118, 144 |
| abstract_inverted_index.an | 91 |
| abstract_inverted_index.at | 61 |
| abstract_inverted_index.in | 66, 87, 126, 139 |
| abstract_inverted_index.it | 112 |
| abstract_inverted_index.of | 42, 54, 63, 84, 93, 97, 132, 137, 142, 150, 153 |
| abstract_inverted_index.on | 29 |
| abstract_inverted_index.to | 15, 45, 80, 114, 128 |
| abstract_inverted_index.us | 14 |
| abstract_inverted_index.we | 3, 59, 72, 100, 109, 124 |
| abstract_inverted_index.and | 47, 50, 69, 108, 146 |
| abstract_inverted_index.can | 4 |
| abstract_inverted_index.few | 121 |
| abstract_inverted_index.for | 39, 103 |
| abstract_inverted_index.how | 2, 71, 111 |
| abstract_inverted_index.is, | 35 |
| abstract_inverted_index.one | 11, 32 |
| abstract_inverted_index.the | 40, 82, 106, 115, 130, 135, 140, 151 |
| abstract_inverted_index.use | 83, 131, 152 |
| abstract_inverted_index.Most | 23 |
| abstract_inverted_index.find | 16 |
| abstract_inverted_index.from | 76 |
| abstract_inverted_index.give | 90 |
| abstract_inverted_index.have | 73 |
| abstract_inverted_index.look | 60 |
| abstract_inverted_index.more | 19 |
| abstract_inverted_index.need | 38 |
| abstract_inverted_index.show | 70, 119 |
| abstract_inverted_index.some | 148 |
| abstract_inverted_index.than | 21 |
| abstract_inverted_index.that | 99 |
| abstract_inverted_index.this | 57 |
| abstract_inverted_index.used | 74 |
| abstract_inverted_index.There | 34 |
| abstract_inverted_index.about | 6, 105 |
| abstract_inverted_index.focus | 28 |
| abstract_inverted_index.helps | 13 |
| abstract_inverted_index.paper | 58 |
| abstract_inverted_index.proof | 18 |
| abstract_inverted_index.sound | 52 |
| abstract_inverted_index.space | 141 |
| abstract_inverted_index.these | 85, 154 |
| abstract_inverted_index.tools | 27, 44, 75 |
| abstract_inverted_index.better | 43 |
| abstract_inverted_index.easily | 20 |
| abstract_inverted_index.formal | 49 |
| abstract_inverted_index.reason | 5 |
| abstract_inverted_index.search | 138 |
| abstract_inverted_index.theory | 96 |
| abstract_inverted_index.within | 31 |
| abstract_inverted_index.analyse | 147 |
| abstract_inverted_index.changes | 53 |
| abstract_inverted_index.current | 24 |
| abstract_inverted_index.explain | 110 |
| abstract_inverted_index.general | 95 |
| abstract_inverted_index.improve | 129 |
| abstract_inverted_index.matter, | 107 |
| abstract_inverted_index.others. | 22 |
| abstract_inverted_index.package | 79 |
| abstract_inverted_index.present | 145 |
| abstract_inverted_index.proofs. | 88 |
| abstract_inverted_index.relates | 113 |
| abstract_inverted_index.results | 149 |
| abstract_inverted_index.tactics | 123 |
| abstract_inverted_index.Isabelle | 127 |
| abstract_inverted_index.Transfer | 78, 116 |
| abstract_inverted_index.automate | 48, 81 |
| abstract_inverted_index.consider | 101 |
| abstract_inverted_index.discrete | 67 |
| abstract_inverted_index.examples | 62 |
| abstract_inverted_index.overview | 92 |
| abstract_inverted_index.package. | 117 |
| abstract_inverted_index.problem. | 9 |
| abstract_inverted_index.specific | 8 |
| abstract_inverted_index.tactics. | 155 |
| abstract_inverted_index.thinking | 104 |
| abstract_inverted_index.Sometimes | 10 |
| abstract_inverted_index.automated | 25 |
| abstract_inverted_index.developed | 125 |
| abstract_inverted_index.including | 134 |
| abstract_inverted_index.logically | 51 |
| abstract_inverted_index.mechanise | 46 |
| abstract_inverted_index.reasoning | 26, 30, 122 |
| abstract_inverted_index.automation | 136 |
| abstract_inverted_index.determines | 1 |
| abstract_inverted_index.therefore, | 36 |
| abstract_inverted_index.appropriate | 102 |
| abstract_inverted_index.development | 41 |
| abstract_inverted_index.Isabelle’s | 77 |
| abstract_inverted_index.mathematics, | 68 |
| abstract_inverted_index.Representation | 0 |
| abstract_inverted_index.representation | 12 |
| abstract_inverted_index.representation. | 33, 55 |
| abstract_inverted_index.transformations | 65, 86, 98 |
| abstract_inverted_index.representational | 64 |
| abstract_inverted_index.representations. | 143 |
| abstract_inverted_index.transformations, | 133 |
| cited_by_percentile_year.max | 94 |
| cited_by_percentile_year.min | 89 |
| countries_distinct_count | 1 |
| institutions_distinct_count | 4 |
| citation_normalized_percentile.value | 0.8650682 |
| citation_normalized_percentile.is_in_top_1_percent | False |
| citation_normalized_percentile.is_in_top_10_percent | False |