{"id":"W2578608903","doi":"10.29007/z9mz","title":"Metis-based Paramodulation Tactic for HOL Light","year":2018,"lang":"en","type":"article","venue":"EPiC series in computing","topic":"Logic, programming, and type systems","field":"Computer Science","cited_by":3,"is_retracted":false,"has_abstract":true,"ca_institutions":"","funders":"Austrian Science Fund","keywords":"HOL; Metis; Mathematical proof; Automated theorem proving; Computer science; Programming language; Proof assistant; Gas meter prover; Mathematics; Database","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.003096462,0.0006212604,0.0006556351,0.001167661,0.000923492,0.002241403,0.00240367,0.001011457,0.01186364],"category_scores_gemma":[0.01069588,0.0007617485,0.001408665,0.0007611872,0.001968222,0.004099943,0.003858286,0.003566025,0.003027265],"about_ca_system_candidate":false,"about_ca_system_consensus":false,"about_ca_system_score_codex":0.001193765,"about_ca_system_score_gemma":0.00234069,"about_ca_topic_candidate":false,"about_ca_topic_consensus":false,"about_ca_topic_score_codex":0.001221848,"about_ca_topic_score_gemma":0.001807419,"domain_scores_codex":[0.9954668,0.0008942042,0.0003227257,0.0004946997,0.002399846,0.0004216016],"domain_scores_gemma":[0.9931636,0.002842583,0.0003429017,0.002483607,0.0009327314,0.0002346438],"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.002580676,0.001161484,0.00651752,0.001895254,0.0002054543,0.0009592993,0.00246598,0.03773665,0.08999711,0.4365004,0.04723177,0.3727485],"study_design_scores_gemma":[0.0005968987,0.0007928203,0.001726181,0.0002536519,0.0001645574,0.001031233,0.0004887281,0.3289301,0.3252487,0.1579832,0.1825759,0.0002080564],"study_design_candidate":"theoretical_or_conceptual","study_design_consensus":"theoretical_or_conceptual","genre_codex":"methods","genre_gemma":"empirical","genre_scores_codex":[0.04775618,0.000247265,0.8608307,0.000496055,0.000262183,0.000477162,0.001399847,0.07183769,0.01669296],"genre_scores_gemma":[0.3505546,0.0002037885,0.6209667,0.0005462184,0.00008641664,0.0005454007,0.003228281,0.01349955,0.01036905],"genre_candidate":"empirical","genre_consensus":null,"teacher_disagreement_score":0.01186364,"threshold_uncertainty_score":0.03968787,"prediction_status":"machine_predicted_unvalidated"},"machine_scores":{"provisional":true,"baseline":true,"maturity_gate_passed":false,"score_opus":0.03108864312804124,"score_gpt":0.290305685783355,"score_spread":0.2592170426553138,"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."}}