{"id":"W3217571258","doi":"10.17169/refubium-19127","title":"Systematic Verification of the Modal Logic Cube in Isabelle/HOL","year":2015,"lang":"en","type":"article","venue":"arXiv (Cornell University)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"","keywords":"HOL; Cube (algebra); Higher-order logic; Modal logic; Normal modal logic; Modal; Accessibility relation; Computer science; Programming language; Multimodal logic; Embedding; Automation; Automated theorem proving; Dynamic logic (digital electronics); Automated reasoning; 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":"metacan-v3-hybrid-931329e0061c","candidate_categories":[],"consensus_categories":[],"category_scores_codex":[0.01116132,0.001037486,0.0009453367,0.001215976,0.00239966,0.002709416,0.002692576,0.001293358,0.007342201],"category_scores_gemma":[0.02335436,0.001394857,0.002875997,0.0007714736,0.004571991,0.005499444,0.006508581,0.003958871,0.001692223],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002530059,"about_ca_system_score_gemma":0.009100565,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.006772595,"about_ca_topic_score_gemma":0.009210123,"domain_scores_codex":[0.9857032,0.005738719,0.0004832189,0.001483228,0.005046683,0.001544954],"domain_scores_gemma":[0.9694325,0.01931226,0.001116061,0.00661137,0.003146896,0.0003810241],"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.0009199874,0.0006634066,0.004844538,0.001928528,0.000527646,0.0015184,0.002951315,0.1099009,0.07653274,0.5682842,0.02471752,0.2072108],"study_design_scores_gemma":[0.000444554,0.00033588,0.001535993,0.0003621813,0.0003265121,0.0005726047,0.0004939589,0.447721,0.1852413,0.3129429,0.0497978,0.0002252871],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.02636208,0.0001629478,0.9568307,0.0007919633,0.0001209999,0.0002812024,0.0003881511,0.01113298,0.003928895],"genre_scores_gemma":[0.3289416,0.0003435886,0.6636312,0.0007535259,0.00007360305,0.0004555043,0.00105361,0.001911578,0.002835931],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01116132,"threshold_uncertainty_score":0.05902737,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.09283432082463612,"score_gpt":0.1906971370384501,"score_spread":0.097862816213814,"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."}}