Skip to main content

Questions tagged [acl2]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
3 votes
1 answer
136 views

untyped lambda expressions may not have normal forms; are they used (or OK to use) in proof assistants?

I heard that untyped lambda expressions can have no normal forms. As an example, the expression $(\lambda x. x\space x) (\lambda x. x\space x)$ , when put to a $\beta$ conversion, gives back the same ...
tinlyx's user avatar
  • 2,034
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