A Semantic Framework for Proof Evidence

Name: Work Video:
Duration: 3 min 30 s
Zakaria Chihani; Dale Miller; Fabien Renaud
{'id': 'https://openalex.org/W2463991046', 'doi': 'https://doi.org/10.1007/s10817-016-9380-6', 'title': 'A Semantic Framework for Proof Evidence', 'display_name': 'A Semantic Framework for Proof Evidence', 'publication_year': 2016, 'publication_date': '2016-07-05', 'ids': {'openalex': 'https://openalex.org/W2463991046', 'doi': 'https://doi.org/10.1007/s10817-016-9380-6', 'mag': '2463991046'}, 'language': 'en', 'primary_location': {'is_oa': False, 'landing_page_url': 'https://doi.org/10.1007/s10817-016-9380-6', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S99781599', 'display_name': 'Journal of Automated Reasoning', 'issn_l': '0168-7433', 'issn': ['0168-7433', '1573-0670'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310319900', 'host_organization_name': 'Springer Science+Business Media', 'host_organization_lineage': ['https://openalex.org/P4310319965', 'https://openalex.org/P4310319900'], 'host_organization_lineage_names': ['Springer Nature', 'Springer Science+Business Media'], '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': True, 'oa_status': 'green', 'oa_url': 'https://inria.hal.science/hal-01390912/document', 'any_repository_has_fulltext': True}, 'authorships': [{'author_position': 'first', 'author': {'id': 'https://openalex.org/A5043153766', 'display_name': 'Zakaria Chihani', 'orcid': 'https://orcid.org/0009-0004-8915-4774'}, 'institutions': [], 'countries': ['FR'], 'is_corresponding': False, 'raw_author_name': 'Zakaria Chihani', 'raw_affiliation_strings': ['PARSIFAL - Proof search and reasoning with logic specifications (France)'], 'affiliations': [{'raw_affiliation_string': 'PARSIFAL - Proof search and reasoning with logic specifications (France)', 'institution_ids': []}]}, {'author_position': 'middle', 'author': {'id': 'https://openalex.org/A5018394339', 'display_name': 'Dale Miller', 'orcid': 'https://orcid.org/0000-0003-0274-4954'}, 'institutions': [{'id': 'https://openalex.org/I4210139461', 'display_name': "Laboratoire d'Informatique de l'École Polytechnique", 'ror': 'https://ror.org/04afed728', 'country_code': 'FR', 'type': 'facility', 'lineage': ['https://openalex.org/I1294671590', 'https://openalex.org/I1326498283', 'https://openalex.org/I142476485', 'https://openalex.org/I4210139461', 'https://openalex.org/I4210145102', 'https://openalex.org/I4210159245']}, {'id': 'https://openalex.org/I142476485', 'display_name': 'École Polytechnique', 'ror': 'https://ror.org/05hy3tk52', 'country_code': 'FR', 'type': 'education', 'lineage': ['https://openalex.org/I142476485', 'https://openalex.org/I4210145102']}], 'countries': ['FR'], 'is_corresponding': False, 'raw_author_name': 'Dale Miller', 'raw_affiliation_strings': ["LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau] (1 Rue Honoré d’Estienne d’Orves, Bâtiment Alain Turing, 91120 Palaiseau - France)", 'PARSIFAL - Proof search and reasoning with logic specifications (France)'], 'affiliations': [{'raw_affiliation_string': 'PARSIFAL - Proof search and reasoning with logic specifications (France)', 'institution_ids': []}, {'raw_affiliation_string': "LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau] (1 Rue Honoré d’Estienne d’Orves, Bâtiment Alain Turing, 91120 Palaiseau - France)", 'institution_ids': ['https://openalex.org/I4210139461', 'https://openalex.org/I142476485']}]}, {'author_position': 'last', 'author': {'id': 'https://openalex.org/A5045724692', 'display_name': 'Fabien Renaud', 'orcid': None}, 'institutions': [], 'countries': ['FR'], 'is_corresponding': False, 'raw_author_name': 'Fabien Renaud', 'raw_affiliation_strings': ['PARSIFAL - Proof search and reasoning with logic specifications (France)'], 'affiliations': [{'raw_affiliation_string': 'PARSIFAL - Proof search and reasoning with logic specifications (France)', 'institution_ids': []}]}], 'institution_assertions': [], 'countries_distinct_count': 1, 'institutions_distinct_count': 2, 'corresponding_author_ids': [], 'corresponding_institution_ids': [], 'apc_list': {'value': 2290, 'currency': 'EUR', 'value_usd': 2890, 'provenance': 'doaj'}, 'apc_paid': None, 'fwci': 2.887, 'has_fulltext': True, 'fulltext_origin': 'pdf', 'cited_by_count': 23, 'citation_normalized_percentile': {'value': 0.999967, 'is_in_top_1_percent': True, 'is_in_top_10_percent': True}, 'cited_by_percentile_year': {'min': 92, 'max': 93}, 'biblio': {'volume': '59', 'issue': '3', 'first_page': '287', 'last_page': '330'}, 'is_retracted': False, 'is_paratext': False, 'primary_topic': {'id': 'https://openalex.org/T10126', 'display_name': 'Logic, programming, and type systems', 'score': 0.9995, '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'}}, 'topics': [{'id': 'https://openalex.org/T10126', 'display_name': 'Logic, programming, and type systems', 'score': 0.9995, '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'}}, {'id': 'https://openalex.org/T11010', 'display_name': 'Logic, Reasoning, and Knowledge', 'score': 0.995, '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'}}, {'id': 'https://openalex.org/T11424', 'display_name': 'Security and Verification in Computing', 'score': 0.988, '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/structural-proof-theory', 'display_name': 'Structural proof theory', 'score': 0.80916774}, {'id': 'https://openalex.org/keywords/proof-complexity', 'display_name': 'Proof complexity', 'score': 0.8037249}, {'id': 'https://openalex.org/keywords/computer-assisted-proof', 'display_name': 'Computer-assisted proof', 'score': 0.6765239}, {'id': 'https://openalex.org/keywords/proof-assistant', 'display_name': 'Proof assistant', 'score': 0.6512827}, {'id': 'https://openalex.org/keywords/analytic-proof', 'display_name': 'Analytic proof', 'score': 0.5014546}, {'id': 'https://openalex.org/keywords/formal-proof', 'display_name': 'Formal proof', 'score': 0.42023894}], 'concepts': [{'id': 'https://openalex.org/C108710211', 'wikidata': 'https://www.wikidata.org/wiki/Q11538', 'display_name': 'Mathematical proof', 'level': 2, 'score': 0.8297284}, {'id': 'https://openalex.org/C195653647', 'wikidata': 'https://www.wikidata.org/wiki/Q7625047', 'display_name': 'Structural proof theory', 'level': 4, 'score': 0.80916774}, {'id': 'https://openalex.org/C105605280', 'wikidata': 'https://www.wikidata.org/wiki/Q7249999', 'display_name': 'Proof complexity', 'level': 3, 'score': 0.8037249}, {'id': 'https://openalex.org/C173613240', 'wikidata': 'https://www.wikidata.org/wiki/Q1150675', 'display_name': 'Computer-assisted proof', 'level': 3, 'score': 0.6765239}, {'id': 'https://openalex.org/C2318724', 'wikidata': 'https://www.wikidata.org/wiki/Q852732', 'display_name': 'Proof theory', 'level': 3, 'score': 0.6750935}, {'id': 'https://openalex.org/C203265346', 'wikidata': 'https://www.wikidata.org/wiki/Q11387554', 'display_name': 'Proof assistant', 'level': 3, 'score': 0.6512827}, {'id': 'https://openalex.org/C206880738', 'wikidata': 'https://www.wikidata.org/wiki/Q431667', 'display_name': 'Automated theorem proving', 'level': 2, 'score': 0.62087506}, {'id': 'https://openalex.org/C41008148', 'wikidata': 'https://www.wikidata.org/wiki/Q21198', 'display_name': 'Computer science', 'level': 0, 'score': 0.6019505}, {'id': 'https://openalex.org/C138268822', 'wikidata': 'https://www.wikidata.org/wiki/Q1051925', 'display_name': 'Resolution (logic)', 'level': 2, 'score': 0.55766416}, {'id': 'https://openalex.org/C135754263', 'wikidata': 'https://www.wikidata.org/wiki/Q4751136', 'display_name': 'Analytic proof', 'level': 3, 'score': 0.5014546}, {'id': 'https://openalex.org/C184337299', 'wikidata': 'https://www.wikidata.org/wiki/Q1437428', 'display_name': 'Semantics (computer science)', 'level': 2, 'score': 0.4815481}, {'id': 'https://openalex.org/C62073222', 'wikidata': 'https://www.wikidata.org/wiki/Q1572108', 'display_name': 'Natural deduction', 'level': 2, 'score': 0.4585012}, {'id': 'https://openalex.org/C94461902', 'wikidata': 'https://www.wikidata.org/wiki/Q2762418', 'display_name': 'Formal proof', 'level': 3, 'score': 0.42023894}, {'id': 'https://openalex.org/C199360897', 'wikidata': 'https://www.wikidata.org/wiki/Q9143', 'display_name': 'Programming language', 'level': 1, 'score': 0.40985316}, {'id': 'https://openalex.org/C80444323', 'wikidata': 'https://www.wikidata.org/wiki/Q2878974', 'display_name': 'Theoretical computer science', 'level': 1, 'score': 0.3685118}, {'id': 'https://openalex.org/C33923547', 'wikidata': 'https://www.wikidata.org/wiki/Q395', 'display_name': 'Mathematics', 'level': 0, 'score': 0.31158948}, {'id': 'https://openalex.org/C2524010', 'wikidata': 'https://www.wikidata.org/wiki/Q8087', 'display_name': 'Geometry', 'level': 1, 'score': 0.0}], 'mesh': [], 'locations_count': 4, 'locations': [{'is_oa': False, 'landing_page_url': 'https://doi.org/10.1007/s10817-016-9380-6', 'pdf_url': None, 'source': {'id': 'https://openalex.org/S99781599', 'display_name': 'Journal of Automated Reasoning', 'issn_l': '0168-7433', 'issn': ['0168-7433', '1573-0670'], 'is_oa': False, 'is_in_doaj': False, 'is_core': True, 'host_organization': 'https://openalex.org/P4310319900', 'host_organization_name': 'Springer Science+Business Media', 'host_organization_lineage': ['https://openalex.org/P4310319965', 'https://openalex.org/P4310319900'], 'host_organization_lineage_names': ['Springer Nature', 'Springer Science+Business Media'], 'type': 'journal'}, 'license': None, 'license_id': None, 'version': None, 'is_accepted': False, 'is_published': False}, {'is_oa': True, 'landing_page_url': 'https://hal.inria.fr/hal-01390912', 'pdf_url': 'https://inria.hal.science/hal-01390912/document', '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': 'other-oa', 'license_id': 'https://openalex.org/licenses/other-oa', 'version': 'submittedVersion', 'is_accepted': False, 'is_published': False}, {'is_oa': True, 'landing_page_url': 'https://hal.inria.fr/hal-01390912/file/fpc-jar.pdf', 'pdf_url': 'https://hal.inria.fr/hal-01390912/file/fpc-jar.pdf', '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': 'submittedVersion', 'is_accepted': False, 'is_published': False}, {'is_oa': True, 'landing_page_url': 'https://hal.inria.fr/hal-01390912/document', 'pdf_url': 'https://hal.inria.fr/hal-01390912/document', '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': 'submittedVersion', 'is_accepted': False, 'is_published': False}], 'best_oa_location': {'is_oa': True, 'landing_page_url': 'https://hal.inria.fr/hal-01390912', 'pdf_url': 'https://inria.hal.science/hal-01390912/document', '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': 'other-oa', 'license_id': 'https://openalex.org/licenses/other-oa', 'version': 'submittedVersion', 'is_accepted': False, 'is_published': False}, 'sustainable_development_goals': [{'display_name': 'Peace, justice, and strong institutions', 'id': 'https://metadata.un.org/sdg/16', 'score': 0.51}], 'grants': [{'funder': 'https://openalex.org/F4320334678', 'funder_display_name': 'European Research Council', 'award_id': 'ProofCert'}], 'datasets': [], 'versions': [], 'referenced_works_count': 96, 'referenced_works': ['https://openalex.org/W107224311', 'https://openalex.org/W134339645', 'https://openalex.org/W1471398886', 'https://openalex.org/W1482532876', 'https://openalex.org/W1484778177', 'https://openalex.org/W1493752083', 'https://openalex.org/W1498523273', 'https://openalex.org/W1505627668', 'https://openalex.org/W1508641834', 'https://openalex.org/W1513458930', 'https://openalex.org/W1514486135', 'https://openalex.org/W1537907223', 'https://openalex.org/W1546727036', 'https://openalex.org/W1553511155', 'https://openalex.org/W1559383704', 'https://openalex.org/W1579694940', 'https://openalex.org/W1592287058', 'https://openalex.org/W159715351', 'https://openalex.org/W1598006012', 'https://openalex.org/W1727609483', 'https://openalex.org/W1795577507', 'https://openalex.org/W1807903125', 'https://openalex.org/W1829244603', 'https://openalex.org/W1852594029', 'https://openalex.org/W1866043924', 'https://openalex.org/W1967880086', 'https://openalex.org/W1973180461', 'https://openalex.org/W1974190112', 'https://openalex.org/W1985185257', 'https://openalex.org/W1988083342', 'https://openalex.org/W1989085426', 'https://openalex.org/W1995430920', 'https://openalex.org/W1995955735', 'https://openalex.org/W1996404651', 'https://openalex.org/W2007809070', 'https://openalex.org/W2022000024', 'https://openalex.org/W2023145007', 'https://openalex.org/W2026542744', 'https://openalex.org/W203185353', 'https://openalex.org/W2048991961', 'https://openalex.org/W2054859958', 'https://openalex.org/W2063266853', 'https://openalex.org/W2070324762', 'https://openalex.org/W2076819871', 'https://openalex.org/W2084443499', 'https://openalex.org/W2085335923', 'https://openalex.org/W2088881461', 'https://openalex.org/W2093111544', 'https://openalex.org/W2095378146', 'https://openalex.org/W2095436832', 'https://openalex.org/W2101814946', 'https://openalex.org/W2106192381', 'https://openalex.org/W2106631406', 'https://openalex.org/W2106988030', 'https://openalex.org/W2109507516', 'https://openalex.org/W2113084713', 'https://openalex.org/W2114925693', 'https://openalex.org/W2118229393', 'https://openalex.org/W2124479173', 'https://openalex.org/W2138536973', 'https://openalex.org/W2141978322', 'https://openalex.org/W2148708285', 'https://openalex.org/W2152096446', 'https://openalex.org/W2166673364', 'https://openalex.org/W2181620542', 'https://openalex.org/W2186150166', 'https://openalex.org/W2246135666', 'https://openalex.org/W2263677784', 'https://openalex.org/W2277055931', 'https://openalex.org/W2294656706', 'https://openalex.org/W2300316091', 'https://openalex.org/W2400995082', 'https://openalex.org/W2402296188', 'https://openalex.org/W2404743010', 'https://openalex.org/W2463700520', 'https://openalex.org/W2545317622', 'https://openalex.org/W2568721247', 'https://openalex.org/W2735026631', 'https://openalex.org/W2911865844', 'https://openalex.org/W2914260883', 'https://openalex.org/W2968832504', 'https://openalex.org/W3135320517', 'https://openalex.org/W3142646652', 'https://openalex.org/W3151527711', 'https://openalex.org/W389428040', 'https://openalex.org/W4206717895', 'https://openalex.org/W4241126266', 'https://openalex.org/W4249736722', 'https://openalex.org/W4249903311', 'https://openalex.org/W4256124958', 'https://openalex.org/W4297574204', 'https://openalex.org/W4300885336', 'https://openalex.org/W46734479', 'https://openalex.org/W60439658', 'https://openalex.org/W657829122', 'https://openalex.org/W81349459'], 'related_works': ['https://openalex.org/W4234403895', 'https://openalex.org/W3163122332', 'https://openalex.org/W2491370528', 'https://openalex.org/W2162495973', 'https://openalex.org/W2119682046', 'https://openalex.org/W2040769847', 'https://openalex.org/W187835144', 'https://openalex.org/W1610564136', 'https://openalex.org/W1541513585', 'https://openalex.org/W1496026483'], 'abstract_inverted_index': None, 'cited_by_api_url': 'https://api.openalex.org/works?filter=cites:W2463991046', 'counts_by_year': [{'year': 2024, 'cited_by_count': 2}, {'year': 2023, 'cited_by_count': 1}, {'year': 2022, 'cited_by_count': 1}, {'year': 2021, 'cited_by_count': 3}, {'year': 2020, 'cited_by_count': 1}, {'year': 2019, 'cited_by_count': 6}, {'year': 2018, 'cited_by_count': 3}, {'year': 2017, 'cited_by_count': 2}, {'year': 2016, 'cited_by_count': 2}, {'year': 2015, 'cited_by_count': 1}], 'updated_date': '2024-12-09T17:17:32.701038', 'created_date': '2016-07-22'}
Publication Information

Basic Information

Access and Citation

AI Researcher Chatbot

Primary Location

Authors

Topics

Keywords

Related Works
