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)

;;