{"id":"W7024328435","doi":"","title":"Reconstructing propositional proofs in type theory","year":2017,"lang":"en","type":"dissertation","venue":"El Repositorio Institucional de la Universidad EAFIT (Universidad EAFIT)","topic":"Soil Geostatistics and Mapping","field":"Environmental Science","cited_by":0,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"Chalmers Tekniska Högskola; Universidad EAFIT","keywords":"Metis; Mathematical proof; Propositional variable; Automated theorem proving; Well-formed formula; Gas meter prover; Propositional calculus; Algebra over a field; Circumscription; Type (biology)","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.01114042,0.001276888,0.001131531,0.002864033,0.002075552,0.00648638,0.00422193,0.00161718,0.0109315],"category_scores_gemma":[0.0393802,0.002408886,0.003840907,0.002294657,0.005662703,0.01205251,0.006937141,0.006562763,0.003442475],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.003497371,"about_ca_system_score_gemma":0.003924473,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.00269368,"about_ca_topic_score_gemma":0.002543569,"domain_scores_codex":[0.9856128,0.005586169,0.0009782471,0.001684402,0.005284185,0.0008541273],"domain_scores_gemma":[0.9729892,0.01722269,0.0008295977,0.005087306,0.003586548,0.0002846843],"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.00012568,0.0000844404,0.00082787,0.0004598532,0.0000948388,0.0003497503,0.001115882,0.01442763,0.003812675,0.8788255,0.003217508,0.09665838],"study_design_scores_gemma":[0.00007592543,0.00005643839,0.0002327954,0.0001888515,0.0001108221,0.0003203049,0.0003304896,0.08224005,0.02884137,0.8555127,0.03201903,0.00007128815],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"methods","genre_scores_codex":[0.004152408,0.0001977662,0.988906,0.0004256743,0.00009151529,0.00008997515,0.000157875,0.002624994,0.003353721],"genre_scores_gemma":[0.1448587,0.0005345365,0.8461988,0.0004299149,0.0001193381,0.0001742973,0.0007072631,0.001864879,0.005112267],"genre_candidate":"methods","genre_consensus":"methods","teacher_disagreement_score":0.01114042,"threshold_uncertainty_score":0.05891687,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.006628950550117628,"score_gpt":0.2456914524809166,"score_spread":0.2390625019307989,"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."}}