{"id":"W2653049029","doi":"","title":"Encoding Proofs in Dedukti: the case of Coq proofs","year":2016,"lang":"en","type":"preprint","venue":"HAL (Le Centre pour la Communication Scientifique Directe)","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"Google (Canada)","funders":"","keywords":"Mathematical proof; Rewriting; Proof assistant; Computer science; HOL; Programming language; Predicative expression; Proof theory; Hierarchy; Encoding (memory); Calculus (dental); Mathematics; Artificial intelligence; Philosophy; Linguistics","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.004140508,0.000517165,0.0008062118,0.001594447,0.001780255,0.006677604,0.001968868,0.001649201,0.009411225],"category_scores_gemma":[0.01732363,0.0008199067,0.001061204,0.003008461,0.004228336,0.01225828,0.005029144,0.003116915,0.001692826],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.003141114,"about_ca_system_score_gemma":0.001762682,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.002219447,"about_ca_topic_score_gemma":0.001424289,"domain_scores_codex":[0.9964756,0.001196802,0.000384875,0.0006111255,0.0008641555,0.0004673449],"domain_scores_gemma":[0.9847795,0.008410702,0.0007176274,0.004018602,0.001582415,0.0004912197],"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.00008830676,0.00001732236,0.0002850968,0.000153279,0.00001245063,0.0001643946,0.0005372453,0.001959715,0.0009447942,0.9815246,0.001742275,0.0125705],"study_design_scores_gemma":[0.0000338734,0.00001761287,0.0001472234,0.0000665498,0.00002705616,0.0002884551,0.0001957764,0.01203914,0.002761718,0.9680892,0.01630681,0.00002664005],"study_design_candidate":"simulation_or_modeling","study_design_consensus":null,"genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.1427366,0.004411588,0.7690477,0.00712856,0.0009624116,0.0001889011,0.001639821,0.003086447,0.07079801],"genre_scores_gemma":[0.8571028,0.001277618,0.127401,0.0008550252,0.0003109678,0.0001341345,0.0007966429,0.0008382453,0.01128362],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.009411225,"threshold_uncertainty_score":0.03148365,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.02351859582546718,"score_gpt":0.2472381832038405,"score_spread":0.2237195873783733,"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."}}