{"id":"W2006220703","doi":"10.1002/mma.1055","title":"Formal verification of tail distribution bounds in the HOL theorem prover","year":2008,"lang":"en","type":"article","venue":"Mathematical Methods in the Applied Sciences","topic":"Formal Methods in Verification","field":"Computer Science","cited_by":14,"is_retracted":false,"has_abstract":true,"ca_institutions":"Concordia University","funders":"","keywords":"Mathematics; Markov chain; Random variable; Applied mathematics; Automated theorem proving; Chebyshev filter; Discrete mathematics; Bernoulli distribution; Algorithm; Statistics; Mathematical analysis","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.01672234,0.001148215,0.001179194,0.001907468,0.001381929,0.004454049,0.00375541,0.001486956,0.006571477],"category_scores_gemma":[0.04351845,0.001262789,0.002279821,0.0009699696,0.00512007,0.006043777,0.004882039,0.003264104,0.00162845],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002410793,"about_ca_system_score_gemma":0.003575847,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00254804,"about_ca_topic_score_gemma":0.001579484,"domain_scores_codex":[0.9854221,0.005119176,0.001204847,0.00154716,0.005304351,0.001402303],"domain_scores_gemma":[0.9394856,0.0501268,0.001946461,0.005103176,0.002906328,0.0004316153],"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.0006054956,0.0003086679,0.00297715,0.0009076508,0.0001511068,0.001169695,0.001150356,0.08058364,0.01516039,0.7871374,0.008745795,0.1011025],"study_design_scores_gemma":[0.0003254118,0.0001646972,0.0004197493,0.0001880551,0.000130024,0.0004293932,0.0001171752,0.4531673,0.0625266,0.463797,0.01862689,0.0001077657],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.008332352,0.00007675349,0.9811,0.0002962238,0.00006515488,0.0001086313,0.00021357,0.007675478,0.002131811],"genre_scores_gemma":[0.4766749,0.0003069788,0.514226,0.000764147,0.0001905535,0.0004181406,0.0008160613,0.002368008,0.00423533],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01672234,"threshold_uncertainty_score":0.0884372,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.08441597948996474,"score_gpt":0.3775679991622145,"score_spread":0.2931520196722497,"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."}}