{"id":"W4230932158","doi":"10.1109/fmcad.2007.4401976","title":"Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC","year":2007,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"University of Toronto","funders":"","keywords":"Mathematical proof; Model checking; Computer science; Bounded function; Resolution (logic); Property (philosophy); Variable (mathematics); Theoretical computer science; Algorithm; Programming language; Mathematics","routes":{"ca_aff":true,"ca_fund":false,"ca_venue":false,"about_ca":false,"invisible_to_affiliation_only":false},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.002659669,0.00008978788,0.00008529431,0.0001456704,0.0001861851,0.00008368772,0.0003775523,0.00006542879,0.00000393552],"category_scores_gemma":[0.0006561084,0.00008752354,0.00004804626,0.000469775,0.0000120566,0.0006304426,0.0001037563,0.00007146346,0.00004134538],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0001553119,"about_ca_system_score_gemma":0.00002482853,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00002680429,"about_ca_topic_score_gemma":0.00008126749,"domain_scores_codex":[0.9988238,0.0000528374,0.00026992,0.0003343546,0.0002042314,0.000314835],"domain_scores_gemma":[0.9991253,0.0001320147,0.00008953381,0.0004006942,0.000160682,0.00009178313],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"bench_or_experimental","study_design_scores_codex":[0.0001106086,0.00004680874,0.0002678986,0.00004976696,0.00000548295,4.011912e-7,0.0009989649,0.0003788045,0.1212803,0.1461584,0.0002539625,0.7304486],"study_design_scores_gemma":[0.0002589206,0.0001977232,0.008754951,0.00001208574,0.000003235256,0.000007511473,0.0001170656,0.3364532,0.6464041,0.004378015,0.003228185,0.0001850353],"study_design_candidate":"bench_or_experimental","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.04418452,0.000005246384,0.9514448,0.00006954473,0.0009355184,0.0005910014,4.309943e-7,0.0003316416,0.002437308],"genre_scores_gemma":[0.3024414,2.482631e-7,0.6968763,0.0001091964,0.0001235669,0.00002248111,6.689713e-7,0.000005977168,0.0004201372],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.7302635,"threshold_uncertainty_score":0.3569106,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09702471681253161,"score_gpt":0.3561568717694678,"score_spread":0.2591321549569362,"validation_status":"score_only:v0-immature-baseline","note":"Baseline scores from an immature model (maturity gate not passed). Scores rank; they never assert a category."}}