Next: Existing Tactics Up: Example Tactics Previous: Example Transformation Tactics

## A Larger Example

We end this section with a somewhat larger example; backchain_with is a tactic that implements backchaining, a restricted form of resolution. It tries to prove the goal by ``backing through'' hypotheses, i.e., by finding a hypothesis that is an implication whose consequent matches the conclusion of the goal, and then recursively calling itself to prove the antecedents of the implication.

The main component is back_thru_hyp, which, given i, proceeds as follows. First, it uses match_part to match the conclusion against part of hypothesis i; if the hypothesis has the form : -> -> : -> ( & & ) (where some of the variables may not be present), and if terms can be obtained that, when substituted for the in one of the , yield the conclusion, then match_part succeeds and returns those terms. The terms are used to obtain instances of the ( antecedents). If m=0 then the goal can be proved immediately; otherwise, a tactic based on the seq rule is used to obtain the subgoals that the seq rule would produce, except that all but the last of the subgoals have no extra hypotheses. The last of these subgoals is completely proved using repeated eliminations; of the rest, the ones which have conclusions of the form a in A are left for the membership tactic , and backchain_with is recursively applied to the remainder.

When invoked, backchain_with first breaks down the conclusion and then tries to back through each hypothesis in turn until it succeeds; if it does not, the tactic tactic is applied. If tactic is `\p.fail` then backchain_with behaves like a primitive Prolog interpreter, where the hypotheses are the clauses and the conclusion is the query. The fact that backchain_with takes a tactic as an argument allows one to make this basic search method more powerful, since it means that one can specify what actions to take at the ``leaves'' of the search.

```letrec backchain_with tactic =
```
```   let atomize_concl =
REPEAT
(\ p . let c = concl p in
if is_function_term c or is_and_term c
then intro p else fail
)			                 in
```
```   let back_thru_hyp i p =
let t = type_of_hyp i p and c = conclusion p  in
let inst_list = match_part c t  in
let antecedents = antecedents t inst_list  in
( if null antecedents then
repeat_and_elim i
THEN
hypothesis
else
parallel_seq antecedents
THEN
(\ p . (if conclusion p = c then
repeat_function_elim i inst_list
THEN
( hypothesis
ORELSE
( apply_to_last_hyp repeat_and_elim
THEN
hypothesis
)
)
else
if_not_membership_goal
(backchain_with tactic)
)  p
)
) p                         in
```
```   atomize_concl
THEN
if_not_membership_goal
(apply_to_a_hyp back_thru_hyp ORELSE tactic)

;;
```

Next: Existing Tactics Up: Example Tactics Previous: Example Transformation Tactics

Richard Eaton
Thu Sep 14 08:45:18 EDT 1995