|
|
|---|
|
|
|
|---|
Attempting to relieve the hypotheses of a rule
When the theorem prover attempts to apply a rule (e.g., a rewrite rule), it must relieve (prove) the hypotheses of that rule. In the ACL2 community, this process of relieving hypotheses is called backchaining.
There is no such thing as a backchaining or backward-chaining rule class (see rule-classes) in ACL2.