id: 5c58eb8f62f04f89aeb6a650f6868629
parent_id: 0cbec79d65b648f4bfa892ef1cd6c2d9
item_type: 1
item_id: 283efb3db6a14c828015279c670d6ad6
item_updated_time: 1682952996964
title_diff: "[]"
body_diff: "[{\"diffs\":[[-1,\"Dear Jasmin,\\\n\\\nMy apologies for the radio silence - the last few months have been busy with courses, so thesis/literature study progress has been slow.\\\nMy last course concluded last month, though, so I have started reading papers for the literature study. I thought I'd send a progress update, and I have some questions on what to do next.\\\n\\\nAs an overview, I read the _Hammering towards QED_ paper, and then started looking at different translations; starting with Translating Higher-Order Clauses/Problems to First-Order Clauses (by J. Meng and L.C. Paulson), which seemed like a good introduction.\\\n\\\nThen, as Coq is similar to Lean in its type-theoretic foundation, I thought it would be relevant to read the CoqHammer papers:\\\n- Hammer for Coq: Automation for Dependent Type Theory\\\n- A Shallow Embedding of Pure Type Systems into First-Order Logic\\\n\\\nThese papers at least make it seem like CIC0 is worth considering as a translation for Lean, as well. My knowledge of the differences between Coq and Lean's type systems is not that good, though - I should probably look at the Lean 4 system overview paper to get a better understanding of that.\\\n\\\nAt this point, I am not entirely sure what direction to look in - I think getting a more thorough understanding of type encoding may be useful (the H2QED paper talks about monotonicity of types, perhaps looking into those references would be useful), as that seems to be a key problem; how do you encode types to be sound enough to get good results but not bog down the ATP. But perhaps it is more useful to look at more recent developments? The papers I've read only focus on translating to untyped FOL; perhaps looking at translations to richer logics supported by newer ATPs is a good idea?\\\n\\\nAdditionally, I'm wondering how specific the topic for the literature study should be - as my thesis will focus on the translation aspect, I assume that should also be the focus of the literature study, but I assume there should also be a general overview of hammer developments, components, etc.\\\n\\\n\\\n\\\nCheers,\\\nSam\\\n\\\n\\\n\\\n\"]],\"start1\":0,\"start2\":0,\"length1\":2055,\"length2\":0}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-05-01T15:04:50.489Z
created_time: 2023-05-01T15:04:50.489Z
type_: 13