id: 6c293b273f554cb8a049ab37ee22e69b
parent_id: 6e0cc536cbe14c769868df50083453d4
item_type: 1
item_id: 6e98d35480c9412c8a1390f17cda32ea
item_updated_time: 1682690647437
title_diff: "[]"
body_diff: "[{\"diffs\":[[-1,\"Around 6 papers, on roughly the topic of the master project we want to do\\\n- [X] Hammering towards QED (J. C. Blanchette, C. Kaliszyk, L. C. Paulson, J. Urban)\\\n- [X] Translating Higher-Order Clauses/Problems to First-Order Clauses (J. Meng and L.C. Paulson)\\\n\\t- On Isabelle/HOL translation to FOL\\\n- [X] Hammer for Coq: Automation for Dependent Type Theory\\\n\\t- Coq is also a type theory-based prover, in fact Lean also uses CIC. So this should be a good starting point.\\\n- [X] A Shallow Embedding of Pure Type Systems into First-Order Logic\\\n\\t- More theoretical treatise on a part of the translation in Hammer for Coq\\\n\\t- Read mostly, but honestly started to glaze over for a lot of the later proofs. Why not just do this _in a theorem prover_ ;)\\\n- [ ] Automatic Proofs and Refutations for Higher-Order Logic (J.C. Blanchette)\\\n- [ ] Goal translation for a hammer for Coq (Czajka, L., Kaliszyk, C., HaTT 2016)\\\n\\t- Base for the Hammer for Coq translation\\\n- [ ] First-order proof tactics in higher-order logic theorem provers (Hurd, 2003)\\\n- [ ] History of interactive theorem proving (Harrison, J., Urban, J., Wiedijk, F., 2014)\\\n- [ ] Program extraction within the Coq proof assistant (Letouzey, P., 2004)\\\n- [ ] Three years of experience with Sledgehammer (J.C. Blanchette, L.C. Paulson)\\\n- [ ] Encoding monomorphic and polymorphic types (J. Blanchette, S. Böhme, A. Popescu, N. Smallbone, 2016)\\\n- [ ] Sort it out with monotonicity (K. Claessen, A. Lillieström, N. Smallbone, 2011)\\\n\\\nOther examples of translation into (higher-order) logic\\\n- [ ] Encoding the Calculus of Constructions in a higher-order logic (A. Felty, 1993)\\\n- [ ] Translating dependent type theory into higher-order logic (B. Jacobs, T. Melham, 1993)\\\n- [ ] Translating a dependently-typed logic into first-order logic (K. Sojakova, F. Rabe, 2008)\\\n\\\nNotes:\\\n\\\nLook into Skolem (functions, constants, ...)\\\nHorn clauses\\\nLCF (LCF-style interface?)\\\nLambda-lifting/combinators (Curry)\\\n[Lean type system overview](https://leanprover.github.io/papers/lean4.pdf)\\\nwtf is _confluence_ and _strongly normalizing_\\\n\\\nTimeline:\\\n\\\n15/04: Hammer for Coq, pagina's 1-15\\\n18/04: Hammer for Coq (finish); Jasmin e-mailen over voortgang; voorbeeld lit study lezen\\\n19/04: A Shallow Embedding..., pagina's 1-15\\\n20/04: A Shallow Embedding..., pagina's 16-39\"]],\"start1\":0,\"start2\":0,\"length1\":2282,\"length2\":0}]"
metadata_diff: {"new":{},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-04-28T14:11:07.336Z
created_time: 2023-04-28T14:11:07.336Z
type_: 13