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
4 votes
1 answer
163 views

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, ...
Trebor's user avatar
  • 3,867
10 votes
1 answer
232 views

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 ...
Max New's user avatar
  • 304
5 votes
1 answer
191 views

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 ...
tinlyx's user avatar
  • 2,034
3 votes
2 answers
195 views

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.
user695931's user avatar
10 votes
1 answer
239 views

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 ...
Cris P's user avatar
  • 335
15 votes
2 answers
350 views

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 ...
Wno-all's user avatar
  • 1,108
32 votes
3 answers
1k views

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 ...
Guy Coder's user avatar
  • 2,836