id: b5bddf78f9e24bcbbbc1c7861fdc1fcb
parent_id: 
item_type: 1
item_id: fc9e4d47857b4515a6b6531b36cf3691
item_updated_time: 1682691021310
title_diff: "[{\"diffs\":[[1,\"Overview\"]],\"start1\":0,\"start2\":0,\"length1\":0,\"length2\":8}]"
body_diff: "[{\"diffs\":[[1,\"# General notes\\\n- [ ] Look into Skolem (functions, constants, ...)\\\n- [ ] What are Horn clauses\\\n- [ ] What is LCF (LCF-style interface?)\\\n- [ ] Look up more info on Lambda-lifting/combinators (Curry)?\\\n- [ ] Read the [Lean type system overview](https://leanprover.github.io/papers/lean4.pdf)\\\n- [ ] wtf is _confluence_ and _strongly normalizing_\\\n\\\n- [ ] look into different TPTP encodings\\\n- [ ] look up progress on a Lean (4) hammer\\\n\\\n- [ ] Read info in Literature Study/Master Project Canvas courses\\\n- [ ] E-mail Jasmin 😅\\\n\\\n# Literature study\\\n\\\nAround 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\\\n## Timeline\\\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\":0,\"length2\":2572}]"
metadata_diff: {"new":{"id":"fc9e4d47857b4515a6b6531b36cf3691","parent_id":"ea739ea32b9a4a8ebf7c2355b78c9cf4","latitude":"52.01157690","longitude":"4.35706770","altitude":"0.0000","author":"","source_url":"","is_todo":0,"todo_due":0,"todo_completed":0,"source":"joplin-desktop","source_application":"net.cozic.joplin-desktop","application_data":"","order":1682690624762,"markup_language":1,"is_shared":0,"share_id":"","conflict_original_id":"","master_key_id":""},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-04-28T14:11:07.401Z
created_time: 2023-04-28T14:11:07.401Z
type_: 13