id: 06fad9c02a134ddeaeb7fca090f23b79
parent_id: 100751fbe4f64209ac12da5e3ed0a2df
item_type: 1
item_id: c66c0433c6a14de9b9a40e5a7316e382
item_updated_time: 1697028679656
title_diff: "[]"
body_diff: "[{\"diffs\":[[0,\" closure\"],[1,\"\\\n - [ ] coinductive types\"],[0,\"\\\n\\\n# Pape\"]],\"start1\":390,\"start2\":390,\"length1\":16,\"length2\":41},{\"diffs\":[[0,\" w(f)^τ₁\"],[1,\")\"],[0,\"`\\\n\\\nwhere\"]],\"start1\":22922,\"start2\":22922,\"length1\":16,\"length2\":17},{\"diffs\":[[0,\"advantage.\\\n\\\n\"],[1,\"**Sparse Naive Bayes**\\\nEstimate the relevance of a fact `a` for a goal `g` by the probability\\\n\\\nP(a is used in the proof of g)\\\n\\\nSince g is characterized by its features, we can further estimate the probability by\\\n\\\nP(a is used in a proof of s | s has features F(g))\\\n\\\nWe define the extended features of a `F'(a) = F(a) union F(b) for all b s.t. a is a dependency of b`\\\n\\\nWe can then estimate the above probability by the statements s which have the features F(g) but do not have the features F'(a) - F(g):\\\n\\\nP(a is used in a proof of s | F(a) subsetof F(g) and F(a) misses F'(a) - F(g))\\\n\\\nwhich is then transformed by Bayes' rule to\\\n\\\n[see paper]\\\n\\\n### Translation\\\nTranslation of Coq goals through CIC0 to untyped first-order logic. Translation is neither sound nor complete. In particular, it assumes proof irrelevance (**would be valid in Lean**), omits universe constraints on Type (not valid in Lean), and \\\"some information is lost in the export to CIC0\\\". It is however good enough to be practically useful.\\\n\\\nThe translation has three phases:\\\n1. Export Coq goals to CIC0\\\n2. Translate CIC0 to first-order logic with equality\\\n3. Perform optimizations on the FOL\\\n\\\n#### Export of Coq to CIC0\\\nTaken straight from the paper:\\\n\\\n- Definitions are exported as CIC0 definitions\\\n- Axioms are exported as CIC0 typing declarations\\\n- Free variables are exported as CIC0 constants with appropriate typing declarations\\\n- Inductive types are exported as CIC0 inductive declarations; induction principles and recursor definitions are exported as separate CIC0 definitions\\\n- Coinductive types are treated in the same way as inductive types, except that no induction principles or recursor definitions are exported for them\\\n(I have no idea what a coinductive type is...)\\\n- \"]],\"start1\":23063,\"start2\":23063,\"length1\":12,\"length2\":1760}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-10-11T12:54:54.726Z
created_time: 2023-10-11T12:54:54.726Z
type_: 13