Publication Information

{'id': 'https://openalex.org/W2044632231', 'doi': 'https://doi.org/10.2307/2275541', 'title': 'Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic', 'display_name': 'Interpolation theorems, lower bounds for proof systems, and independence results for bounded arithmetic', 'publication_year': 1997, 'publication_date': '1997-06-01', 'ids': {'openalex': 'https://openalex.org/W2044632231', 'doi': 'https://doi.org/10.2307/2275541', 'mag': '2044632231'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'https://doi.org/10.2307/2275541', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S177675236', 'display_name': 'Journal of Symbolic Logic', 'issn_l': '0022-4812', 'issn': ['0022-4812', '1943-5886'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310311721', 'host_organization_name': 'Cambridge University Press', 'host_organization_lineage': ['https://openalex.org/P4310311721', 'https://openalex.org/P4310311702'], 'host_organization_lineage_names': ['Cambridge University Press', 'University of Cambridge'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, 'type': 'article', 'type_crossref': 'journal-article', 'indexed_in': ['crossref'], 'open_access': {'is_oa': False, 'oa_status': 'closed', 'oa_url': None, 'any_repository_has_fulltext': False}, 'authorships': [{'author_position': 'first', 'author': {'id': 'https://openalex.org/A5069803587', 'display_name': 'Jan Krajı́ček', 'orcid': 'https://orcid.org/0000-0003-0670-3957'}, 'institutions': [{'id': 'https://openalex.org/I4210120266', 'display_name': 'Czech Academy of Sciences, Institute of Mathematics', 'ror': 'https://ror.org/02tv1yf50', 'country_code': 'CZ', 'type': 'facility', 'lineage': ['https://openalex.org/I202391551', 'https://openalex.org/I4210120266']}], 'countries': ['CZ'], 'is_corresponding': True, 'raw_author_name': 'Jan Krajíček', 'raw_affiliation_strings': ['Mathematical Institute of the Academy of Sciences, Žitná 25, Praha 1, 115 67, Czech Republic, E-mail:'], 'affiliations': [{'raw_affiliation_string': 'Mathematical Institute of the Academy of Sciences, Žitná 25, Praha 1, 115 67, Czech Republic, E-mail:', 'institution_ids': ['https://openalex.org/I4210120266']}]}], 'institution_assertions': [], 'countries_distinct_count': 1, 'institutions_distinct_count': 1, 'corresponding_author_ids': ['https://openalex.org/A5069803587'], 'corresponding_institution_ids': ['https://openalex.org/I4210120266'], 'apc_list': None, 'apc_paid': None, 'fwci': 9.798, 'has_fulltext': True, 'fulltext_origin': 'ngrams', 'cited_by_count': 303, 'citation_normalized_percentile': {'value': 0.999764, 'is_in_top_1_percent': True, 'is_in_top_10_percent': True}, 'cited_by_percentile_year': {'min': 98, 'max': 99}, 'biblio': {'volume': '62', 'issue': '2', 'first_page': '457', 'last_page': '486'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10720', 'display_name': 'Complexity and Algorithms in Graphs', 'score': 0.9997, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, 'topics': [{'id': 'https://openalex.org/T10720', 'display_name': 'Complexity and Algorithms in Graphs', 'score': 0.9997, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10142', 'display_name': 'Formal Methods in Verification', 'score': 0.9989, 'subfield': {'id': 'https://openalex.org/subfields/1703', 'display_name': 'Computational Theory and Mathematics'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}, {'id': 'https://openalex.org/T10237', 'display_name': 'Cryptography and Data Security', 'score': 0.9984, 'subfield': {'id': 'https://openalex.org/subfields/1702', 'display_name': 'Artificial Intelligence'}, 'field': {'id': 'https://openalex.org/fields/17', 'display_name': 'Computer Science'}, 'domain': {'id': 'https://openalex.org/domains/3', 'display_name': 'Physical Sciences'}}], 'keywords': [{'id': 'https://openalex.org/keywords/proof-complexity', 'display_name': 'Proof complexity', 'score': 0.775558}, {'id': 'https://openalex.org/keywords/pigeonhole-principle', 'display_name': 'Pigeonhole principle', 'score': 0.7060012}, {'id': 'https://openalex.org/keywords/interpolation', 'display_name': 'Interpolation', 'score': 0.6392387}, {'id': 'https://openalex.org/keywords/unary-operation', 'display_name': 'Unary operation', 'score': 0.55500966}, {'id': 'https://openalex.org/keywords/analytic-proof', 'display_name': 'Analytic proof', 'score': 0.52595663}], 'concepts': [{'id': 'https://openalex.org/C105605280', 'wikidata': 'https://www.wikidata.org/wiki/Q7249999', 'display_name': 'Proof complexity', 'level': 3, 'score': 0.775558}, {'id': 'https://openalex.org/C33923547', 'wikidata': 'https://www.wikidata.org/wiki/Q395', 'display_name': 'Mathematics', 'level': 0, 'score': 0.77112913}, {'id': 'https://openalex.org/C171988527', 'wikidata': 'https://www.wikidata.org/wiki/Q188276', 'display_name': 'Pigeonhole principle', 'level': 2, 'score': 0.7060012}, {'id': 'https://openalex.org/C108710211', 'wikidata': 'https://www.wikidata.org/wiki/Q11538', 'display_name': 'Mathematical proof', 'level': 2, 'score': 0.6537817}, {'id': 'https://openalex.org/C137800194', 'wikidata': 'https://www.wikidata.org/wiki/Q11713455', 'display_name': 'Interpolation (computer graphics)', 'level': 3, 'score': 0.6392387}, {'id': 'https://openalex.org/C34388435', 'wikidata': 'https://www.wikidata.org/wiki/Q2267362', 'display_name': 'Bounded function', 'level': 2, 'score': 0.6388887}, {'id': 'https://openalex.org/C118615104', 'wikidata': 'https://www.wikidata.org/wiki/Q121416', 'display_name': 'Discrete mathematics', 'level': 1, 'score': 0.57217985}, {'id': 'https://openalex.org/C78023250', 'wikidata': 'https://www.wikidata.org/wiki/Q657596', 'display_name': 'Unary operation', 'level': 2, 'score': 0.55500966}, {'id': 'https://openalex.org/C2834757', 'wikidata': 'https://www.wikidata.org/wiki/Q4925424', 'display_name': 'Monotone polygon', 'level': 2, 'score': 0.5357036}, {'id': 'https://openalex.org/C135754263', 'wikidata': 'https://www.wikidata.org/wiki/Q4751136', 'display_name': 'Analytic proof', 'level': 3, 'score': 0.52595663}, {'id': 'https://openalex.org/C2318724', 'wikidata': 'https://www.wikidata.org/wiki/Q852732', 'display_name': 'Proof theory', 'level': 3, 'score': 0.4250754}, {'id': 'https://openalex.org/C134306372', 'wikidata': 'https://www.wikidata.org/wiki/Q7754', 'display_name': 'Mathematical analysis', 'level': 1, 'score': 0.13465342}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.106003284}, {'id': 'https://openalex.org/C115961682', 'wikidata': 'https://www.wikidata.org/wiki/Q860623', 'display_name': 'Image (mathematics)', 'level': 2, 'score': 0.07146934}, {'id': 'https://openalex.org/C2524010', 'wikidata': 'https://www.wikidata.org/wiki/Q8087', 'display_name': 'Geometry', 'level': 1, 'score': 0.0}, {'id': 'https://openalex.org/C154945302', 'wikidata': 'https://www.wikidata.org/wiki/Q11660', 'display_name': 'Artificial intelligence', 'level': 1, 'score': 0.0}], 'mesh': [], 'locations_count': 1, 'locations': [{'is_oa': False, 'landing_page_url': 'https://doi.org/10.2307/2275541', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S177675236', 'display_name': 'Journal of Symbolic Logic', 'issn_l': '0022-4812', 'issn': ['0022-4812', '1943-5886'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310311721', 'host_organization_name': 'Cambridge University Press', 'host_organization_lineage': ['https://openalex.org/P4310311721', 'https://openalex.org/P4310311702'], 'host_organization_lineage_names': ['Cambridge University Press', 'University of Cambridge'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}], 'best_oa_location': None, 'sustainable_development_goals': [], 'grants': [], 'datasets': [], 'versions': [], 'referenced_works_count': 43, 'referenced_works': ['https://openalex.org/W1563012911', 'https://openalex.org/W1572440476', 'https://openalex.org/W1983097969', 'https://openalex.org/W1988083342', 'https://openalex.org/W1993453078', 'https://openalex.org/W1995120485', 'https://openalex.org/W1997908783', 'https://openalex.org/W2011612028', 'https://openalex.org/W2012476164', 'https://openalex.org/W2014588328', 'https://openalex.org/W2025279645', 'https://openalex.org/W2026916148', 'https://openalex.org/W2034768280', 'https://openalex.org/W2038193643', 'https://openalex.org/W2040404640', 'https://openalex.org/W2045664183', 'https://openalex.org/W2054013713', 'https://openalex.org/W2056827464', 'https://openalex.org/W2062912795', 'https://openalex.org/W2068363706', 'https://openalex.org/W2069767473', 'https://openalex.org/W2098244894', 'https://openalex.org/W2114633883', 'https://openalex.org/W2114817374', 'https://openalex.org/W2161149481', 'https://openalex.org/W2170605748', 'https://openalex.org/W2171353564', 'https://openalex.org/W2294221698', 'https://openalex.org/W2385171024', 'https://openalex.org/W256005661', 'https://openalex.org/W2595959570', 'https://openalex.org/W3039529476', 'https://openalex.org/W39775292', 'https://openalex.org/W4213009134', 'https://openalex.org/W4230067008', 'https://openalex.org/W4248733413', 'https://openalex.org/W4250368611', 'https://openalex.org/W4255046774', 'https://openalex.org/W43155751', 'https://openalex.org/W4388289506', 'https://openalex.org/W4388289526', 'https://openalex.org/W49401050', 'https://openalex.org/W56285243'], 'related_works': ['https://openalex.org/W4234403895', 'https://openalex.org/W2922318846', 'https://openalex.org/W2722497084', 'https://openalex.org/W2626436722', 'https://openalex.org/W2490626787', 'https://openalex.org/W2461509449', 'https://openalex.org/W2119682046', 'https://openalex.org/W2044632231', 'https://openalex.org/W171706349', 'https://openalex.org/W153148314'], 'abstract_inverted_index': {'Abstract': [0], 'A': [1], 'proof': [2, 20, 24, 53, 88, 133, 144], 'of': [3, 27, 54, 73, 95, 116, 145, 149, 154, 177, 203, 214], 'the': [4, 55, 86, 99, 117, 130, 146, 152, 159, 167, 199, 215], '(propositional)': [5], 'Craig': [6], 'interpolation': [7, 56, 83, 184, 196], 'theorem': [8, 57, 185, 197], 'for': [9, 69, 85, 125, 129, 198, 211], 'cut-free': [10, 19], 'sequent': [11, 16], 'calculus': [12, 109], 'yields': [13], 'that': [14, 172, 192], 'a': [15, 18, 23, 51, 60, 66, 70, 93, 173, 193], 'with': [17, 22, 25, 32, 36, 135], '(or': [21], 'cut-formulas': [26], 'restricted': [28], 'form;': [29], 'in': [30, 138, 158], 'particular,': [31], 'only': [33], 'analytic': [34], 'cuts)': [35], 'k': [37, 47], 'inferences': [38], 'has': [39], 'an': [40], 'interpolant': [41], 'whose': [42], 'circuit-size': [43, 155], 'is': [44], 'at': [45], 'most': [46], '.': [48], 'We': [49, 75], 'give': [50], 'new': [52, 122, 207], 'based': [58], 'on': [59], 'communication': [61], 'complexity': [62], 'approach': [63], 'which': [64], 'allows': [65], 'similar': [67], 'estimate': [68], 'larger': [71], 'class': [72], 'proofs.': [74], 'derive': [76], 'from': [77], 'it': [78], 'several': [79], 'corollaries:': [80], '(1)': [81], 'Feasible': [82], 'theorems': [84], 'following': [87], 'systems:': [89], '(a)': [90, 124], 'resolution': [91, 126, 212], '(b)': [92, 128], 'subsystem': [94, 176, 202], 'LK': [96, 178, 204], 'corresponding': [97], 'to': [98], 'bounded': [100, 160], 'arithmetic': [101, 161], 'theory': [102, 162], '(': [103, 163], 'α': [104, 164], ')': [105], '(c)': [106], 'linear': [107], 'equational': [108], '(d)': [110], 'cutting': [111, 131], 'planes.': [112], '(2)': [113], 'New': [114], 'proofs': [115, 213], 'exponential': [118, 208], 'lower': [119, 156, 209], 'bounds': [120, 157, 210], '(for': [121], 'formulas)': [123], '([15])': [127], 'planes': [132], 'system': [134], 'coefficients': [136], 'written': [137], 'unary': [139], '([4]).': [140], '(3)': [141], 'An': [142], 'alternative': [143], 'independence': [147], 'result': [148], '[43]': [150], 'concerning': [151], 'provability': [153], ').': [165], 'In': [166], 'other': [168], 'direction': [169], 'we': [170], 'show': [171], 'depth': [174, 200], '2': [175], 'does': [179], 'not': [180], 'admit': [181], 'feasible': [182, 194], 'monotone': [183, 195], '(the': [186], 'so': [187], 'called': [188], 'Lyndon': [189], 'theorem),': [190], 'and': [191], '1': [201], 'would': [205], 'yield': [206], 'weak': [216], 'pigeonhole': [217], 'principle.': [218]}, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W2044632231', 'counts_by_year': [{'year': 2024, 'cited_by_count': 7}, {'year': 2023, 'cited_by_count': 4}, {'year': 2022, 'cited_by_count': 5}, {'year': 2021, 'cited_by_count': 8}, {'year': 2020, 'cited_by_count': 33}, {'year': 2019, 'cited_by_count': 42}, {'year': 2018, 'cited_by_count': 13}, {'year': 2017, 'cited_by_count': 11}, {'year': 2016, 'cited_by_count': 12}, {'year': 2015, 'cited_by_count': 12}, {'year': 2014, 'cited_by_count': 11}, {'year': 2013, 'cited_by_count': 11}, {'year': 2012, 'cited_by_count': 12}], 'updated_date': '2024-12-14T22:14:14.736748', 'created_date': '2016-06-24'}