{"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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.005902034,0.001050593,0.000953564,0.002143678,0.001016466,0.002076973,0.002602655,0.001355083,0.005000666],"category_scores_gemma":[0.04050737,0.001207775,0.001546292,0.001222217,0.002746304,0.004828149,0.004018692,0.002951956,0.001160343],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001020623,"about_ca_system_score_gemma":0.001964631,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001385411,"about_ca_topic_score_gemma":0.002212481,"domain_scores_codex":[0.9933961,0.00324687,0.0004540776,0.0006779138,0.001862132,0.0003629037],"domain_scores_gemma":[0.9529549,0.03484268,0.002373307,0.007363832,0.002124582,0.0003405844],"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.0008572221,0.0003252587,0.005064365,0.001398198,0.0002670127,0.001176596,0.001907008,0.1285247,0.09834143,0.2266533,0.006342957,0.529142],"study_design_scores_gemma":[0.000239368,0.0001724091,0.0004910121,0.0001591249,0.000126312,0.0008393792,0.0001193856,0.7598026,0.1278264,0.09936861,0.01074838,0.0001069752],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.008347572,0.0001419211,0.9845323,0.0001601266,0.00001797284,0.00006661029,0.00003595131,0.00600002,0.0006974959],"genre_scores_gemma":[0.1552617,0.000147406,0.8424531,0.0001423592,0.00003183642,0.0001210874,0.0001231057,0.001038215,0.0006810953],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.005902034,"threshold_uncertainty_score":0.03121334,"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."}}