4 ms·

I'm taking a formal verification course about this right now using the logical foundations volume. This relies on the Coq proof assistant. From what I've begun

by bsedlm 5y ago

I'm taking a formal verification course about this right now using the logical foundations volume. This relies on the Coq proof assistant. From what I've begun to understand, they use 'higher order logic', which really means they can quantify (for all, there exists) over things with cardinalities larger than the countably infinite.

amw-zero 5y ago
More specifically, Coq is based on the calculus of inductive constructions: https://en.m.wikipedia.org/wiki/Calculus_of_constructions https://en.m.wikipedia.org/wiki/Calculus_of_constructions. The key differentiating feature being dependent types, whereas Isabelle/HOL implements higher-order logic without dependent types.