top | item 12896182 Tensorflow Deepmath: Experiments towards neural network theorem proving 142 points| runesoerensen | 9 years ago |github.com 12 comments order hn newest [+] [-] runesoerensen|9 years ago|reply Relevant HN discussion about the paper: https://news.ycombinator.com/item?id=12031253 [+] [-] cmrx64|9 years ago|reply Neat! I look forward to seeing what they come up with :) For similar sorts of things, check out NeSy: http://daselab.cs.wright.edu/nesy/NeSy16/ [+] [-] bitL|9 years ago|reply What logic does it use? Any chance using relevance or linear logic to avoid vacuous truth proofs (like in set theory)? [+] [-] cmrx64|9 years ago|reply It's currently integrating higher-order logic (HOL) with a reimplementation of HOL Light. load replies (1) [+] [-] Mao_Zedang|9 years ago|reply Hook it up to a network that makes theorems. [+] [-] SticksAndBreaks|9 years ago|reply Every problem i can break into a sub problem is solveable. Thus proofen by induction that i can break recursively down every problem, i deduce- that i crashed with a NN-Stackoverflow. [+] [-] thomasahle|9 years ago|reply > Every problem i can break into a sub problem is solveable.Given the sub problems are either solvable or can in turn be broken down, I suppose?
[+] [-] runesoerensen|9 years ago|reply Relevant HN discussion about the paper: https://news.ycombinator.com/item?id=12031253
[+] [-] cmrx64|9 years ago|reply Neat! I look forward to seeing what they come up with :) For similar sorts of things, check out NeSy: http://daselab.cs.wright.edu/nesy/NeSy16/
[+] [-] bitL|9 years ago|reply What logic does it use? Any chance using relevance or linear logic to avoid vacuous truth proofs (like in set theory)? [+] [-] cmrx64|9 years ago|reply It's currently integrating higher-order logic (HOL) with a reimplementation of HOL Light. load replies (1)
[+] [-] cmrx64|9 years ago|reply It's currently integrating higher-order logic (HOL) with a reimplementation of HOL Light. load replies (1)
[+] [-] SticksAndBreaks|9 years ago|reply Every problem i can break into a sub problem is solveable. Thus proofen by induction that i can break recursively down every problem, i deduce- that i crashed with a NN-Stackoverflow. [+] [-] thomasahle|9 years ago|reply > Every problem i can break into a sub problem is solveable.Given the sub problems are either solvable or can in turn be broken down, I suppose?
[+] [-] thomasahle|9 years ago|reply > Every problem i can break into a sub problem is solveable.Given the sub problems are either solvable or can in turn be broken down, I suppose?
[+] [-] runesoerensen|9 years ago|reply
[+] [-] cmrx64|9 years ago|reply
[+] [-] bitL|9 years ago|reply
[+] [-] cmrx64|9 years ago|reply
[+] [-] Mao_Zedang|9 years ago|reply
[+] [-] SticksAndBreaks|9 years ago|reply
[+] [-] thomasahle|9 years ago|reply
Given the sub problems are either solvable or can in turn be broken down, I suppose?