News for hackers. Stuff that matters.

A comment on Formalizing 100 Theorems. Parent comment

Re:Formalizing 100 Theorems by riku_iki on Friday November 03, 2023 @04:04PM (#38134265)
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.
[ Parent | on HN ]
Re:Formalizing 100 Theorems by carnitine on Sunday November 05, 2023 @10:11AM (#38151771)
That’s not true either. Coq’s logic is significantly different to HoL.
[ Parent | on HN ]
Re:Formalizing 100 Theorems by riku_iki on Sunday November 05, 2023 @10:16AM (#38151813)
hol meaning higher order logic (https://en.wikipedia.org/wiki/Higher-order_logic) not the lang of hol prover.
[ Parent | on HN ]