Get quick answers to your questions about the article from our AI researcher chatbot
{'id': 'https://openalex.org/W2753162328', 'doi': 'https://doi.org/10.4204/eptcs.256.4', 'title': 'An Existence Theorem of Nash Equilibrium in Coq and Isabelle', 'display_name': 'An Existence Theorem of Nash Equilibrium in Coq and Isabelle', 'publication_year': 2017, 'publication_date': '2017-09-06', 'ids': {'openalex': 'https://openalex.org/W2753162328', 'doi': 'https://doi.org/10.4204/eptcs.256.4', 'mag': '2753162328'}, 'language': 'en', 'primary_location': {'is_oa': True, 'landing_page_url': None, 'pdf_url': 'https://arxiv.org/pdf/1709.02096', 'source': {'id': 'https://openalex.org/S4306400194', 'display_name': 'arXiv (Cornell University)', 'issn_l': None, 'issn': None, 'is_oa': True, 'is_in_doaj': False, 'is_core': False, 'host_organization': 'https://openalex.org/I205783295', 'host_organization_name': 'Cornell University', 'host_organization_lineage': ['https://openalex.org/I205783295'], 'host_organization_lineage_names': ['Cornell University'], 'type': 'repository'}, 'license': 'cc-by-nc-nd', 'license_id': 'https://openalex.org/licenses/cc-by-nc-nd', 'version': 'publishedVersion', 'is_accepted': True, 'is_published': True}, 'type': 'article', 'type_crossref': 'journal-article', 'indexed_in': ['arxiv', 'crossref', 'datacite', 'doaj'], 'open_access': {'is_oa': True, 'oa_status': 'diamond', 'oa_url': 'https://arxiv.org/pdf/1709.02096', 'any_repository_has_fulltext': True}, 'authorships': [{'author_position': 'first', 'author': {'id': 'https://openalex.org/A5103521817', 'display_name': 'Stéphane Le Roux', 'orcid': None}, 'institutions': [{'id': 'https://openalex.org/I132053463', 'display_name': 'Université Libre de Bruxelles', 'ror': 'https://ror.org/01r9htc13', 'country_code': 'BE', 'type': 'education', 'lineage': ['https://openalex.org/I132053463']}], 'countries': ['BE'], 'is_corresponding': False, 'raw_author_name': 'Stéphane Le Roux', 'raw_affiliation_strings': ['Université Libre de Bruxelles'], 'affiliations': [{'raw_affiliation_string': 'Université Libre de Bruxelles', 'institution_ids': ['https://openalex.org/I132053463']}]}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5109222954', 'display_name': 'Érik Martin-Dorel', 'orcid': None}, 'institutions': [{'id': 'https://openalex.org/I4210119061', 'display_name': 'Institut de Recherche en Informatique de Toulouse', 'ror': 'https://ror.org/01rx4qw44', 'country_code': 'FR', 'type': 'facility', 'lineage': ['https://openalex.org/I4210119061']}, {'id': 'https://openalex.org/I17866349', 'display_name': 'Université de Toulouse', 'ror': 'https://ror.org/004raaa70', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I17866349']}, {'id': 'https://openalex.org/I134560555', 'display_name': 'Université Toulouse III - Paul Sabatier', 'ror': 'https://ror.org/02v6kpv12', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I134560555']}, {'id': 'https://openalex.org/I3131550300', 'display_name': 'Université Toulouse-I-Capitole', 'ror': 'https://ror.org/0443n9e75', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I3131550300']}, {'id': 'https://openalex.org/I4210160189', 'display_name': 'Institut Polytechnique de Bordeaux', 'ror': 'https://ror.org/054qv7y42', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I4210160189']}, {'id': 'https://openalex.org/I4210152422', 'display_name': 'Université Toulouse - Jean Jaurès', 'ror': 'https://ror.org/04ezk3x31', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I4210152422']}], 'countries': ['FR'], 'is_corresponding': False, 'raw_author_name': 'Érik Martin-Dorel', 'raw_affiliation_strings': ['IRIT, Université de Toulouse'], 'affiliations': [{'raw_affiliation_string': 'IRIT, Université de Toulouse', 'institution_ids': ['https://openalex.org/I4210119061', 'https://openalex.org/I17866349', 'https://openalex.org/I134560555', 'https://openalex.org/I3131550300', 'https://openalex.org/I4210160189', 'https://openalex.org/I4210152422']}]}, {'author_position': 'last', 'author': {'id': 'https://openalex.org/A5111483282', 'display_name': 'Jan‐Georg Smaus', 'orcid': None}, 'institutions': [{'id': 'https://openalex.org/I17866349', 'display_name': 'Université de Toulouse', 'ror': 'https://ror.org/004raaa70', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I17866349']}, {'id': 'https://openalex.org/I4210160189', 'display_name': 'Institut Polytechnique de Bordeaux', 'ror': 'https://ror.org/054qv7y42', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I4210160189']}, {'id': 'https://openalex.org/I4210152422', 'display_name': 'Université Toulouse - Jean Jaurès', 'ror': 'https://ror.org/04ezk3x31', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I4210152422']}, {'id': 'https://openalex.org/I4210119061', 'display_name': 'Institut de Recherche en Informatique de Toulouse', 'ror': 'https://ror.org/01rx4qw44', 'country_code': 'FR', 'type': 'facility', 'lineage': ['https://openalex.org/I4210119061']}, {'id': 'https://openalex.org/I134560555', 'display_name': 'Université Toulouse III - Paul Sabatier', 'ror': 'https://ror.org/02v6kpv12', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I134560555']}, {'id': 'https://openalex.org/I3131550300', 'display_name': 'Université Toulouse-I-Capitole', 'ror': 'https://ror.org/0443n9e75', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I3131550300']}], 'countries': ['FR'], 'is_corresponding': False, 'raw_author_name': 'Jan-Georg Smaus', 'raw_affiliation_strings': ['IRIT, Université de Toulouse'], 'affiliations': [{'raw_affiliation_string': 'IRIT, Université de Toulouse', 'institution_ids': ['https://openalex.org/I17866349', 'https://openalex.org/I4210160189', 'https://openalex.org/I4210152422', 'https://openalex.org/I4210119061', 'https://openalex.org/I134560555', 'https://openalex.org/I3131550300']}]}], 'institution_assertions': [], 'countries_distinct_count': 2, 'institutions_distinct_count': 7, 'corresponding_author_ids': [], 'corresponding_institution_ids': [], 'apc_list': {'value': 0, 'currency': 'USD', 'value_usd': 0, 'provenance': 'doaj'}, 'apc_paid': None, 'fwci': 2.682, 'has_fulltext': True, 'fulltext_origin': 'pdf', 'cited_by_count': 6, 'citation_normalized_percentile': {'value': 0.75619, 'is_in_top_1_percent': False, 'is_in_top_10_percent': False}, 'cited_by_percentile_year': {'min': 81, 'max': 82}, 'biblio': {'volume': '256', 'issue': None, 'first_page': '46', 'last_page': '60'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T12137', 'display_name': 'Economic theories and models', 'score': 0.999, 'subfield': {'id': 'https://openalex.org/subfields/2002', 'display_name': 'Economics and Econometrics'}, 'field': {'id': 'https://openalex.org/fields/20', 'display_name': 'Economics, Econometrics and Finance'}, 'domain': {'id': 'https://openalex.org/domains/2', 'display_name': 'Social Sciences'}}, 'topics': [{'id': 'https://openalex.org/T12137', 'display_name': 'Economic theories and models', 'score': 0.999, 'subfield': {'id': 'https://openalex.org/subfields/2002', 'display_name': 'Economics and Econometrics'}, 'field': {'id': 'https://openalex.org/fields/20', 'display_name': 'Economics, Econometrics and Finance'}, 'domain': {'id': 'https://openalex.org/domains/2', 'display_name': 'Social Sciences'}}, {'id': 'https://openalex.org/T10991', 'display_name': 'Game Theory and Voting Systems', 'score': 0.9984, 'subfield': {'id': 'https://openalex.org/subfields/2002', 'display_name': 'Economics and Econometrics'}, 'field': {'id': 'https://openalex.org/fields/20', 'display_name': 'Economics, Econometrics and Finance'}, 'domain': {'id': 'https://openalex.org/domains/2', 'display_name': 'Social Sciences'}}, {'id': 'https://openalex.org/T11031', 'display_name': 'Game Theory and Applications', 'score': 0.9915, 'subfield': {'id': 'https://openalex.org/subfields/1803', 'display_name': 'Management Science and Operations Research'}, 'field': {'id': 'https://openalex.org/fields/18', 'display_name': 'Decision Sciences'}, 'domain': {'id': 'https://openalex.org/domains/2', 'display_name': 'Social Sciences'}}], 'keywords': [], 'concepts': [{'id': 'https://openalex.org/C144237770', 'wikidata': 'https://www.wikidata.org/wiki/Q747534', 'display_name': 'Mathematical economics', 'level': 1, 'score': 0.43026143}, {'id': 'https://openalex.org/C33923547', 'wikidata': 'https://www.wikidata.org/wiki/Q395', 'display_name': 'Mathematics', 'level': 0, 'score': 0.40621245}], 'mesh': [], 'locations_count': 6, 'locations': [{'is_oa': True, 'landing_page_url': None, 'pdf_url': 'https://arxiv.org/pdf/1709.02096', 'source': {'id': 'https://openalex.org/S4306400194', 'display_name': 'arXiv (Cornell University)', 'issn_l': None, 'issn': None, 'is_oa': True, 'is_in_doaj': False, 'is_core': False, 'host_organization': 'https://openalex.org/I205783295', 'host_organization_name': 'Cornell University', 'host_organization_lineage': ['https://openalex.org/I205783295'], 'host_organization_lineage_names': ['Cornell University'], 'type': 'repository'}, 'license': 'cc-by-nc-nd', 'license_id': 'https://openalex.org/licenses/cc-by-nc-nd', 'version': 'publishedVersion', 'is_accepted': True, 'is_published': True}, {'is_oa': False, 'landing_page_url': 'https://hal.science/hal-03434697', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S4306402512', 'display_name': 'HAL (Le Centre pour la Communication Scientifique Directe)', 'issn_l': None, 'issn': None, 'is_oa': True, 'is_in_doaj': False, 'is_core': False, 'host_organization': 'https://openalex.org/I1294671590', 'host_organization_name': 'Centre National de la Recherche Scientifique', 'host_organization_lineage': ['https://openalex.org/I1294671590'], 'host_organization_lineage_names': ['Centre National de la Recherche Scientifique'], 'type': 'repository'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, {'is_oa': False, 'landing_page_url': 'https://doaj.org/article/796513759fa340cea322383b2b53ff84', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S4306401280', 'display_name': 'DOAJ (DOAJ: Directory of Open Access Journals)', 'issn_l': None, 'issn': None, 'is_oa': True, 'is_in_doaj': False, 'is_core': False, 'host_organization': None, 'host_organization_name': None, 'host_organization_lineage': [], 'host_organization_lineage_names': [], 'type': 'repository'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, {'is_oa': False, 'landing_page_url': 'https://hal.archives-ouvertes.fr/hal-03434697', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S4306402512', 'display_name': 'HAL (Le Centre pour la Communication Scientifique Directe)', 'issn_l': None, 'issn': None, 'is_oa': True, 'is_in_doaj': False, 'is_core': False, 'host_organization': 'https://openalex.org/I1294671590', 'host_organization_name': 'Centre National de la Recherche Scientifique', 'host_organization_lineage': ['https://openalex.org/I1294671590'], 'host_organization_lineage_names': ['Centre National de la Recherche Scientifique'], 'type': 'repository'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, {'is_oa': True, 'landing_page_url': 'http://oatao.univ-toulouse.fr/19172/1/leroux_19172.pdf', 'pdf_url': 'http://oatao.univ-toulouse.fr/19172/1/leroux_19172.pdf', 'source': {'id': 'https://openalex.org/S4306401987', 'display_name': 'Open Archive Toulouse Archive Ouverte (University of Toulouse)', 'issn_l': None, 'issn': None, 'is_oa': True, 'is_in_doaj': False, 'is_core': False, 'host_organization': 'https://openalex.org/I17866349', 'host_organization_name': 'Université de Toulouse', 'host_organization_lineage': ['https://openalex.org/I17866349'], 'host_organization_lineage_names': ['Université de Toulouse'], 'type': 'repository'}, 'license': 'cc-by', 'license_id': 'https://openalex.org/licenses/cc-by', 'version': 'acceptedVersion', 'is_accepted': True, 'is_published': False}, {'is_oa': False, 'landing_page_url': 'https://api.datacite.org/dois/10.48550/arxiv.1709.02096', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S4393179698', 'display_name': 'DataCite API', 'issn_l': None, 'issn': None, 'is_oa': True, 'is_in_doaj': False, 'is_core': False, 'host_organization': 'https://openalex.org/I4210145204', 'host_organization_name': 'DataCite', 'host_organization_lineage': ['https://openalex.org/I4210145204'], 'host_organization_lineage_names': ['DataCite'], 'type': 'metadata'}, 'license': None, 'license_id': None, 'version': None}], 'best_oa_location': {'is_oa': True, 'landing_page_url': None, 'pdf_url': 'https://arxiv.org/pdf/1709.02096', 'source': {'id': 'https://openalex.org/S4306400194', 'display_name': 'arXiv (Cornell University)', 'issn_l': None, 'issn': None, 'is_oa': True, 'is_in_doaj': False, 'is_core': False, 'host_organization': 'https://openalex.org/I205783295', 'host_organization_name': 'Cornell University', 'host_organization_lineage': ['https://openalex.org/I205783295'], 'host_organization_lineage_names': ['Cornell University'], 'type': 'repository'}, 'license': 'cc-by-nc-nd', 'license_id': 'https://openalex.org/licenses/cc-by-nc-nd', 'version': 'publishedVersion', 'is_accepted': True, 'is_published': True}, 'sustainable_development_goals': [], 'grants': [], 'datasets': [], 'versions': ['https://openalex.org/W2753162328', 'https://openalex.org/W3148482407'], 'referenced_works_count': 15, 'referenced_works': ['https://openalex.org/W121484200', 'https://openalex.org/W149674103', 'https://openalex.org/W1530060568', 'https://openalex.org/W1701372208', 'https://openalex.org/W1969912861', 'https://openalex.org/W2014805785', 'https://openalex.org/W2043715088', 'https://openalex.org/W2062541377', 'https://openalex.org/W2062600857', 'https://openalex.org/W2100485490', 'https://openalex.org/W2167653210', 'https://openalex.org/W2170933628', 'https://openalex.org/W2963529132', 'https://openalex.org/W4211129676', 'https://openalex.org/W4248784701'], 'related_works': ['https://openalex.org/W4391375266', 'https://openalex.org/W4238204885', 'https://openalex.org/W3002753104', 'https://openalex.org/W2600246793', 'https://openalex.org/W2142036596', 'https://openalex.org/W2077600819', 'https://openalex.org/W2072657027', 'https://openalex.org/W2061531152', 'https://openalex.org/W2007980826', 'https://openalex.org/W1979597421'], 'abstract_inverted_index': {'Nash': [0, 90], 'equilibrium': [1], '(NE)': [2], 'is': [3], 'a': [4, 14, 31, 40, 70, 75, 81, 89, 130, 133], 'central': [5], 'concept': [6], 'in': [7, 22, 165], 'game': [8, 32, 41, 72, 76, 86], 'theory.': [9], 'Here': [10], 'we': [11, 111, 120, 145], 'prove': [12], 'formally': [13], 'published': [15], 'theorem': [16, 124, 154], 'on': [17], 'existence': [18, 128], 'of': [19, 45, 50, 67, 106, 129, 136, 152], 'an': [20], 'NE': [21, 137], 'two': [23, 51], 'proof': [24, 102, 151], 'assistants,': [25], 'Coq': [26], 'and': [27], 'Isabelle:': [28], 'starting': [29], 'from': [30], 'with': [33, 48], 'finitely': [34], 'many': [35], 'outcomes,': [36, 53], 'one': [37, 78], 'may': [38], 'derive': [39], 'by': [42, 114], 'rewriting': [43], 'each': [44], 'these': [46], 'outcomes': [47], 'either': [49], 'basic': [52], 'namely': [54], 'that': [55, 60, 122, 138, 148], 'Player': [56, 61], '1': [57], 'wins': [58], 'or': [59], '2': [62], 'wins.': [63], 'If': [64], 'all': [65], 'ways': [66], 'deriving': [68], 'such': [69], 'win/lose': [71], 'lead': [73], 'to': [74], 'where': [77], 'player': [79], 'has': [80, 88], 'winning': [82], 'strategy,': [83], 'the': [84, 100, 116, 123, 127, 149, 153], 'original': [85, 101], 'also': [87, 125, 146], 'equilibrium.': [91], 'This': [92], 'article': [93], 'makes': [94], 'three': [95], 'other': [96], 'contributions:': [97], 'first,': [98], 'while': [99], 'invoked': [103], 'linear': [104], 'extension': [105], 'strict': [107], 'partial': [108], 'orders,': [109], 'here': [110], 'avoid': [112], 'it': [113], 'generalizing': [115], 'relevant': [117], 'definition.': [118], 'Second,': [119], 'notice': [121, 147], 'implies': [126], 'secure': [131, 156], 'equilibrium,': [132], 'stronger': [134], 'version': [135], 'was': [139], 'introduced': [140], 'for': [141, 158], 'model': [142], 'checking.': [143], 'Third,': [144], 'constructive': [150], 'computes': [155], 'equilibria': [157], 'non-zero-sum': [159], 'priority': [160], 'games': [161], '(generalizing': [162], 'parity': [163], 'games)': [164], 'quasi-polynomial': [166], 'time.': [167]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W2753162328', 'counts_by_year': [{'year': 2018, 'cited_by_count': 4}, {'year': 2017, 'cited_by_count': 2}], 'updated_date': '2024-12-07T16:06:45.462695', 'created_date': '2017-09-15'}