{"id":"W152230201","doi":"10.1007/978-3-540-24771-5_16","title":"Calculational Relation-Algebraic Proofs in Isabelle/Isar","year":2004,"lang":"en","type":"book-chapter","venue":"Lecture notes in computer science","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":21,"is_retracted":false,"has_abstract":false,"ca_institutions":"McMaster University","funders":"","keywords":"Mathematical proof; Relation (database); Algebraic number; Calculus (dental); Computer science; Mathematics; Geometry; Mathematical analysis; Medicine; Data mining","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.005742243,0.001274235,0.001898175,0.002135773,0.002589339,0.006769213,0.004332247,0.001537555,0.02509769],"category_scores_gemma":[0.008569816,0.002478292,0.002493504,0.002964752,0.004899406,0.01461862,0.003240719,0.007410138,0.01035317],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.002638953,"about_ca_system_score_gemma":0.002429518,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001562826,"about_ca_topic_score_gemma":0.002506454,"domain_scores_codex":[0.9955449,0.001721493,0.0003042287,0.0005244124,0.001594408,0.0003105103],"domain_scores_gemma":[0.9954939,0.002708487,0.0001896259,0.0009968352,0.0005004724,0.0001106469],"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.00001896337,0.00003544616,0.00005089708,0.0001921305,0.00001932379,0.00004878437,0.0003775737,0.0009570956,0.0004969774,0.9461907,0.01382634,0.03778568],"study_design_scores_gemma":[0.00003205046,0.00001342778,0.0001099378,0.0001228067,0.0000237102,0.0001849428,0.00005959932,0.004633895,0.001987976,0.9057927,0.08699372,0.0000452136],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.004993784,0.004277409,0.8708382,0.002797458,0.0006315698,0.0001287334,0.000407108,0.00857115,0.1073546],"genre_scores_gemma":[0.180051,0.004867645,0.7344058,0.001238161,0.001038214,0.0003154787,0.001399228,0.006522036,0.07016242],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.02509769,"threshold_uncertainty_score":0.08396018,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.01938299762709196,"score_gpt":0.2423159575408286,"score_spread":0.2229329599137366,"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."}}