{"id":"W1973614029","doi":"10.1109/fmcad.2007.20","title":"Exploiting Resolution Proofs to Speed Up LTL Vacuity Detection for BMC","year":2007,"lang":"en","type":"article","venue":"Formal Methods in Computer-Aided Design","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":20,"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); Algorithm; Theoretical computer science; 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":["metaepi_narrow"],"consensus_categories":[],"category_scores_codex":[0.02762016,0.0004256089,0.0005289229,0.0009336836,0.0004322851,0.0002703312,0.001454522,0.0003032268,0.000003169555],"category_scores_gemma":[0.001950922,0.0004524801,0.0001994581,0.001848751,0.00005591275,0.002303167,0.0005576862,0.0004472481,0.00002479114],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0005929131,"about_ca_system_score_gemma":0.0001310885,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00003145973,"about_ca_topic_score_gemma":0.00001731112,"domain_scores_codex":[0.9940227,0.001711616,0.001353152,0.001056316,0.0005195519,0.001336638],"domain_scores_gemma":[0.9950934,0.002670168,0.0004735663,0.001098668,0.0003636886,0.0003004898],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"design_other","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0003854152,0.00009011936,0.00007138011,0.00009152872,0.00001296462,0.000003582779,0.001226127,0.01800889,0.02026952,0.01587081,0.00005878014,0.9439109],"study_design_scores_gemma":[0.0007836507,0.0008085966,0.002842244,0.00007416838,0.000008887981,0.00003349115,0.00004312659,0.7186905,0.2628374,0.01283809,0.0006065312,0.0004333615],"study_design_candidate":"design_other","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.00519985,0.00003596038,0.9876089,0.00004112345,0.003927526,0.002455923,0.000002120225,0.0005602305,0.000168358],"genre_scores_gemma":[0.01948417,0.000002438093,0.9794347,0.0002606835,0.0005413094,0.000184051,0.000003158156,0.0000446798,0.00004485236],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.9434775,"threshold_uncertainty_score":0.9997927,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.1730657762546369,"score_gpt":0.4196368254503517,"score_spread":0.2465710491957148,"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."}}