{"id":"W1824826039","doi":"10.4204/eptcs.186.5","title":"Systematic Verification of the Modal Logic Cube in Isabelle/HOL","year":2015,"lang":"en","type":"article","venue":"Electronic Proceedings in Theoretical Computer Science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":13,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"Deutsche Forschungsgemeinschaft","keywords":"HOL; Cube (algebra); Higher-order logic; Computer science; Modal; Modal logic; Programming language; Embedding; Multimodal logic; Automation; Normal modal logic; Accessibility relation; Automated theorem proving; Dynamic logic (digital electronics); Algorithm; Theoretical computer science; Description logic; Mathematics; Artificial intelligence; Engineering","routes":{"ca_aff":false,"ca_fund":false,"ca_venue":false,"about_ca":true,"invisible_to_affiliation_only":true},"retraction":null,"screen":null,"direct_labels":[],"prediction":{"model_version":"codex-gemma-dda1882f352a","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.004819211,0.0001849503,0.0003519783,0.0002428123,0.0001109677,0.0002309749,0.003380995,0.0000859217,0.000001429677],"category_scores_gemma":[0.0004643737,0.000120057,0.00006286479,0.002705015,0.001077578,0.0006130105,0.0007045133,0.0003628849,0.00001412579],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.0004305721,"about_ca_system_score_gemma":0.0004415447,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00001356501,"about_ca_topic_score_gemma":0.000004137676,"domain_scores_codex":[0.996994,0.00009691939,0.0005898253,0.0006461253,0.0008808204,0.0007922738],"domain_scores_gemma":[0.9987665,0.00009580729,0.0002365053,0.0004934254,0.0002838933,0.0001238569],"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.000004973675,0.0000832249,0.0005686454,0.0002420352,0.000002363752,0.000001021905,0.001623261,0.00006645291,0.0003693413,0.9965488,0.000009852532,0.0004799984],"study_design_scores_gemma":[0.0003817568,0.0002748494,0.0004180772,0.0001714856,0.000003800779,0.00004835639,0.00008016672,0.3064934,0.004233045,0.6876973,0.00001843569,0.0001792949],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.1221164,0.0006040513,0.8649558,0.001403635,0.000965594,0.00172539,1.645036e-7,0.0001744965,0.008054422],"genre_scores_gemma":[0.9970472,0.00000427661,0.002715687,0.0001176603,0.00004359169,0.00005091347,1.043309e-7,0.000006580589,0.0000139246],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.8749309,"threshold_uncertainty_score":0.6282786,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01391705845651953,"score_gpt":0.2437346175284077,"score_spread":0.2298175590718882,"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."}}