Skip to main content

Questions tagged [higher-order-logic]

Use this tag for questions related to higher order logic. Do not use this tag with the HOL theorem prover instead use hol. Do not use this tag for Isabelle/HOL instead use isabelle-hol. Do not use this tag with HOL light theorem prover instead use hol-light.

Filter by
Sorted by
Tagged with
32 votes
3 answers

What are the bases for different Proof Assistants?

From the Wikipedia article on Proof Assistant it shows some Proof Assistants are based on Higher Order Logic, (HOL Light) and some are based on Dependent Types, (Coq). Are there any other means upon ...
4 votes
1 answer

New types in higher order logic

From my understanding, most descriptions of higher order logic have a clear "phase distinction": We first describe the types, which are usually syntactically simple trees. For concreteness, ...
10 votes
1 answer

How "generic" are "generic proof assistants"?

I've read that Isabelle and Metamath (and maybe Andromeda) are "generic" proof assistants in some sense that allows them to be used to implement different theories such as HOL, ZF and ...
5 votes
1 answer

Is ACL2 first-order-logic and is this a limitation for proving math?

I am considering whether I should learn the ACL2 proof assistant. However, before diving into that, I wanted to know if there are significant limitations in terms of proving math. The first thing I ...
3 votes
2 answers

Reference request for an introduction to higher-order logic

I'm looking for an introductory text or other materials on higher order logic, with a minimum of assumed background knowledge beyond first order logic.
10 votes
1 answer

Performance of de Bruijn indices?

Can any of you refer me to documented results of experiments on the performance of provers using de Bruijn indices to represent references to bound variables versus mentions of names or other simple ...
15 votes
2 answers

Are Logics Based on Dependent Types Stronger Than Ones Without?

There have been several times during I came across statements like Isabelle/HOL's logic is not rich enough to formalize X on various places online and in during personal discussions. Or similar ...