id: e7c1157600544e5b83763950c694d962
parent_id: 
item_type: 1
item_id: fc9e4d47857b4515a6b6531b36cf3691
item_updated_time: 1695729632567
title_diff: "[{\"diffs\":[[1,\"Overview (old)\"]],\"start1\":0,\"start2\":0,\"length1\":0,\"length2\":14}]"
body_diff: "[{\"diffs\":[[1,\"# General notes\\\n- [X] Look into Skolem (functions, constants, ...)\\\n- [ ] What are Horn clauses\\\n- [ ] What is LCF (LCF-style interface?)\\\n\\t- Logic for (of?) Computable Functions; the 'style' is that of a kernel that exports an interface that is limited to allowed operations, reducing the trusted surface to just the kernel.\\\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- [X] 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\\\n- [X] Translating Higher-Order Clauses/Problems to First-Order Clauses (J. Meng and L.C. Paulson)\\\nOn Isabelle/HOL translation to FOL\\\n\\\n- [X] Hammer for Coq: Automation for Dependent Type Theory\\\nCoq is also a type theory-based prover, in fact Lean also uses CIC. So this should be a good starting point.\\\n\\\n- [X] A Shallow Embedding of Pure Type Systems into First-Order Logic\\\nMore theoretical treatise on a part of the translation in Hammer for Coq\\\nRead mostly, but honestly started to glaze over for a lot of the later proofs. Why not just do this _in a theorem prover_ ;)\\\n\\\n- [ ] Encoding monomorphic and polymorphic types (J. Blanchette, S. Böhme, A. Popescu, N. Smallbone, 2016)\\\nGood overview of different type translation methods\\\nCoqHammer uses type guards method, but potentially using the cover idea?\\\n\\\nCover: say we translate `cons<a>(X, Xs)` using type tags, we would get `t(list(A), cons(t(A, X), t(list(A), Xs)))`.\\\nGiven that we _know_ cons takes only one type argument, we only need one of the tags to infer the other types; if we see\\\n`t(?, cons(t(A, X), t(?, Xs))` we know it must be `t(list(A), cons(t(A, X), t(list(A), Xs)))`.\\\n\\\nA cover `C \\\\subseteq {1, ..., |@s|}` is a set of term argument indices s.t. any inferable type argument can be inferred from a term argument in C. So, for `cons: \\\\forall a. a -> list(a) -> list(a)`, either `C = {1}` or `C = {2}` is a minimal cover. `C = {1, 2}` is a maximal cover.\\\n\\\n\\\n\\\n\\\n\\\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\\\n\\\n## On soundness/completeness\\\n\\\nThe use of \\\"sound\\\" and \\\"complete\\\" seems to differ between papers, or small nuances make them mean the opposite in certain scenarios.\\\n\\\nClassically, the terms refer to a correspondence between proof systems and semantic truth, namely\\\n\\\nSoundness: `M |- phi` implies `M |= phi`\\\nCompleteness: `M |= phi` implies `M |- phi`\\\n\\\nColloquially: if a proof system is sound, it is impossible to prove something that is not true. If it is complete, it is possible to prove all true things.\\\n\\\nIn the Encoding Monomorphic and Polymorphic Types paper, we get the following definitions of \\\"sound\\\" and \\\"complete\\\" translations:\\\n\\\n\\tA translation that translates problems Phi over signature Sigma to Phi' over Sigma' is _sound_ if the satisfiability of Phi implies the satisfiability of Phi'.\\\n\\t\\\n\\\n\\\n# Outline\\\n\\\n\"]],\"start1\":0,\"start2\":0,\"length1\":0,\"length2\":3357}]"
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":"","user_data":""},"deleted":[]}
encryption_cipher_text: 
encryption_applied: 0
updated_time: 2023-09-26T12:10:20.910Z
created_time: 2023-09-26T12:10:20.910Z
type_: 13