Hacker News new | ask | show | jobs
by carnitine 963 days ago
They definitely don’t all compile to the same thing. Some do, most don’t.
1 comments
riku_iki 963 days ago
I meant to say they are all the same thing on logical level, all those fancy typed theories can be reduced to hol/fol, for some it is implemented, for others not.
link
carnitine 961 days ago
That’s not true either. Coq’s logic is significantly different to HoL.
link
riku_iki 961 days ago
hol meaning higher order logic (https://en.wikipedia.org/wiki/Higher-order_logic) not the lang of hol prover.
link