limiting the effort expended on relieving hypotheses



Moreover, the user may set a global backchain-limit that limits the total backchaining depth. See set-backchain-limit. Below we lay out the precise sense in which this global backchain-limit interacts with the backchain-limits of individual rules in order to limit backchaining. But first we note that when further backchaining is disallowed, ACL2 can still prove a hypothesis in a given context by using that contextual information. This process is sometimes called ``type-set reasoning,'' an appropriate term since rules of class :type-prescription may be used. So, for example, the relieving of hypotheses may be limited to the use of contextual information (without backchaining, i.e., without recursively rewriting hypotheses) by executing :set-backchain-limit 0.


We illustrate with the following examples.


(defstub p0 (x) t) (defstub p1 (x) t) (defstub p2 (x) t) (defstub p3 (x) t)


(defaxiom p2-implies-p1-limitless (implies (p2 x) (p1 x)))


(defaxiom p1-implies-p0-limit-0 (implies (p1 x) (p0 x)) :rule-classes ((:rewrite :backchain-limit-lst 0)))

; We have (p2 x) ==> (p1 x) ==> (p0 x). We wish to establish that ; (p2 x) ==> (p0 x). Normally, this would be no problem, but here ; we fail because ACL2 cannot establish (p0 x) by type-set reasoning ; alone.

(thm (implies (p2 x) (p0 x)))

; We set the default-backchain-limit to 1.

:set-default-backchain-limit 1

; The following is more powerful than p1-implies-p0-limit-0 ; because it can use rewrite rules to establish (p1 x).

(defaxiom p1-implies-p0-limit-1 (implies (p1 x) (p0 x)))

; This theorem will succeed:



:set-default-backchain-limit nil

; Here is our last axiom.

(defaxiom p3-implies-p2-limitless (implies (p3 x) (p2 x)))

; We now have (p3 x) ==> (p2 x) ==> (p1 x) ==> (p0 x). However the ; rule p1-implies-p0-limit-1 has a backchain-limit of 1; hence we ; are not allowed to backchain far enough back to use ; p3-implies-p2-limitless. We therefore lose.

(defthm will-fail (implies (p3 x) (p0 x)))