2 ms·

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 no

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.

carnitine 3y ago
That’s not true either. Coq’s logic is significantly different to HoL.
- riku_iki 3y ago
  hol meaning higher order logic (https://en.wikipedia.org/wiki/Higher-order_logic https://en.wikipedia.org/wiki/Higher-order_logic) not the lang of hol prover.