{"id":"W2013754071","doi":"10.1016/j.entcs.2009.07.012","title":"LCF-style Platform based on Multiway Decision Graphs","year":2009,"lang":"en","type":"article","venue":"Electronic Notes in Theoretical Computer Science","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":1,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Reachability; Automated theorem proving; HOL; Computer science; Set (abstract data type); Product (mathematics); Theoretical computer science; Inference; Rule of inference; Programming language; Artificial intelligence; 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.001393949,0.0007468018,0.0006036688,0.001205293,0.0005697648,0.001547872,0.001842869,0.0008494496,0.00962643],"category_scores_gemma":[0.003284881,0.0004775481,0.00144502,0.0005143991,0.001304561,0.002131683,0.001640256,0.001310724,0.001652192],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001120335,"about_ca_system_score_gemma":0.001700142,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.003234032,"about_ca_topic_score_gemma":0.002604737,"domain_scores_codex":[0.9987118,0.0002942251,0.00008566221,0.0002981335,0.0004088373,0.0002012426],"domain_scores_gemma":[0.998516,0.0007851756,0.0001058205,0.0003494401,0.0001784777,0.00006514895],"domain_codex":null,"domain_gemma":null,"domain_candidate":null,"domain_consensus":null,"study_design_codex":"theoretical_or_conceptual","study_design_gemma":"theoretical_or_conceptual","study_design_scores_codex":[0.0007344153,0.0006129947,0.002647516,0.000903778,0.0001912463,0.001731925,0.0006058465,0.2384245,0.04407037,0.4088938,0.01029835,0.2908852],"study_design_scores_gemma":[0.0002535761,0.0003152551,0.0004928494,0.0001057005,0.0001056302,0.0006386123,0.00006804599,0.7166898,0.0622939,0.1693995,0.04954766,0.00008947207],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.01311675,0.00008428967,0.9711477,0.0001275865,0.00004480785,0.0003156291,0.0004782189,0.01047156,0.004213381],"genre_scores_gemma":[0.2268114,0.0001681369,0.76557,0.000194785,0.0000295087,0.0004570158,0.001177469,0.0007609946,0.004830607],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.00962643,"threshold_uncertainty_score":0.03220356,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01075389753875564,"score_gpt":0.2872517377196815,"score_spread":0.2764978401809259,"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."}}