{"id":"W2116591673","doi":"10.1109/fdl.2008.4641435","title":"The performance of combining multiway decision graphs and HOL theorem prover","year":2008,"lang":"en","type":"article","venue":"","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":2,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Automated theorem proving; Computer science; Consistency (knowledge bases); Rule of inference; Inference; Theoretical computer science; Automation; Programming language; Algorithm; Artificial intelligence","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.003864258,0.001277356,0.001184002,0.001445955,0.0005148444,0.001856307,0.002550701,0.0008762476,0.004597066],"category_scores_gemma":[0.006610271,0.0007112561,0.0008113775,0.001010559,0.0008447897,0.004260176,0.002422114,0.001434092,0.001089943],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0008188631,"about_ca_system_score_gemma":0.001458038,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001517701,"about_ca_topic_score_gemma":0.001949486,"domain_scores_codex":[0.9952484,0.001697341,0.0002131053,0.0008392496,0.001712314,0.0002896259],"domain_scores_gemma":[0.993198,0.004646896,0.0002701249,0.001327692,0.000387944,0.0001693222],"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.002985342,0.001022681,0.00651375,0.001230689,0.0005924355,0.0009200571,0.0003784583,0.2413526,0.09111885,0.04970555,0.003583251,0.6005964],"study_design_scores_gemma":[0.0002158039,0.0004610349,0.0006681264,0.00005393795,0.0001518697,0.0002134765,0.00008322838,0.9030601,0.06910397,0.0211988,0.004722778,0.00006698976],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.08967129,0.0005295613,0.889651,0.0002477777,0.00008828201,0.0001784947,0.0001441965,0.01514459,0.00434484],"genre_scores_gemma":[0.4703172,0.0002601719,0.5270217,0.0001223455,0.00003207694,0.0001024991,0.0003067419,0.0005459487,0.001291249],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.004597066,"threshold_uncertainty_score":0.02043641,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02288197179140945,"score_gpt":0.2676747469142631,"score_spread":0.2447927751228536,"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."}}