{"id":"W2007666139","doi":"10.1007/s00165-012-0223-x","title":"Automatic verification of reduction techniques in Higher Order Logic","year":2012,"lang":"en","type":"article","venue":"Formal Aspects of Computing","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"HOL; Computer science; Correctness; Soundness; Reduction (mathematics); Model checking; Programming language; Heuristics; Consistency (knowledge bases); Partial order reduction; Automated theorem proving; Algorithm; Formal verification; Reduction strategy; Theoretical computer science; 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.003860137,0.0009190115,0.0007998633,0.001473497,0.0007250082,0.001321143,0.001788163,0.0007799898,0.003794778],"category_scores_gemma":[0.008839778,0.000678395,0.002624219,0.0005562646,0.002732083,0.002023429,0.002437723,0.002361912,0.0006499475],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001223691,"about_ca_system_score_gemma":0.001668275,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002793229,"about_ca_topic_score_gemma":0.00292931,"domain_scores_codex":[0.9926646,0.002557053,0.0003351374,0.0006286925,0.003238334,0.0005760789],"domain_scores_gemma":[0.9899501,0.006687922,0.0004663222,0.002087608,0.0007152698,0.00009276971],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"simulation_or_modeling","study_design_scores_codex":[0.0007388724,0.0007823863,0.003597333,0.0009719198,0.0004607894,0.0009972629,0.00104512,0.3498415,0.1431529,0.3515607,0.002399083,0.1444521],"study_design_scores_gemma":[0.0001913567,0.0002361609,0.0006283405,0.00005973486,0.000135401,0.0001663067,0.00007154326,0.7567026,0.1008492,0.134839,0.006062213,0.00005808233],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.03804207,0.00006318543,0.9554949,0.0001077491,0.00003200476,0.0001409877,0.00006985098,0.004264372,0.001784859],"genre_scores_gemma":[0.5794194,0.000114651,0.4171499,0.0001539196,0.00003149362,0.0002668152,0.0003171441,0.0006716425,0.001874994],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.003860137,"threshold_uncertainty_score":0.02041459,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.04194995695396473,"score_gpt":0.3097887354940638,"score_spread":0.2678387785400991,"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."}}