{"doi":"10.4230/lipics.csl.2017.27","title":"Unknown","abstract":null,"journal":null,"year":null,"id":589348,"datarank":4.454720333127042,"base_score":4.574710978503383,"endowment":4.574710978503383,"self_citation_contribution":0.6862066467755076,"citation_network_contribution":3.7685136863515347,"self_endowment_contribution":0.6862066467755076,"citer_contribution":3.7685136863515347,"corpus_percentile":null,"corpus_rank":null,"citation_count":96,"citer_count":97,"citers_with_citation_signal":73,"citers_with_endowment":73,"datacite_reuse_total":2,"is_dataset":false,"is_dataset_confidence":null,"is_data_producer":false,"deposit_databanks":null,"is_oa":false,"file_count":0,"downloads":0,"has_version_chain":false,"published_date":null,"fair_score":null,"fair_percentile":null,"algorithm_id":"datarank_citation_only_1hop_v6","ranking_scope":"data_only","authors":[],"reference_count":0,"raw_metadata":{"has_enrichment":true,"resolved":true,"title":"The Model-Theoretic Expressiveness of Propositional Proof Systems","abstract":"We establish new, and surprisingly tight, connections between propositional proof complexity and finite model theory.\r\nSpecifically, we show that the power of several propositional proof systems, such as Horn resolution, bounded width resolution, and the polynomial calculus of bounded degree, can be characterised in a precise sense by variants of fixed-point logics that are of fundamental importance in descriptive complexity theory.\r\nOur main results are that Horn resolution has the same expressive power as least fixed-point logic, that bounded width resolution captures existential least fixed-point logic, and that the (monomial restriction of the) polynomial calculus of bounded degree solves precisely the problems definable in fixed-point logic with counting.","is_dataset_classified":null,"base_score":0.0,"endowment":0.0,"datacite_reuse_total":2,"file_count":0,"downloads":0,"views":0,"has_version_chain":false,"is_dataset":false,"is_oa":false,"pmid":"26657633","pmcid":null,"openalex_id":null,"authors":[],"funders":[],"total_grants":0,"fwci":null,"citation_percentile":null,"influential_citations":0,"citation_trend":[],"oa_status":null,"license":"cc by 3.0","oa_locations":[],"fields_of_study":[],"mesh_terms":[],"keywords":["Propositional proof systems","fixed-point logics","resolution","polynomial calculus","generalized quantifiers"],"sdg_mappings":[],"linked_datasets":[{"doi":"10.4230/lipics.csl.2017","title":"LIPIcs, Volume 82, CSL'17, Complete Volume","publisher":"Schloss Dagstuhl – Leibniz-Zentrum für Informatik","resource_type":"ConferenceProceeding"},{"doi":"10.18154/rwth-2020-09507","title":"The Model-Theoretic Expressiveness of Propositional Proof Systems","publisher":"RWTH Aachen University","resource_type":"Text"}],"clinical_trials":[],"software_tools":[],"database_accessions":[],"source":"live","citation_network_status":"fetched"},"created_at":"2026-07-23T16:51:21.933914Z","pmid":null,"pmcid":null,"fwci":null,"citation_percentile":null,"influential_citations":0,"oa_status":null,"license":null,"views":0,"total_file_size_bytes":0,"version_count":0,"fair_f":null,"fair_a":null,"fair_i":null,"fair_r":null,"fair_zscore":null,"fair_rationale":null,"fair_model":null,"fair_agent_version":null,"fair_fulltext_source":null,"fair_has_llm":null,"fair_computed_at":null,"clinical_trials":[],"software_tools":[],"db_accessions":[],"linked_datasets":[],"topics":[]}