Theorem Prover: How to optimize a backward proof search containing a "useless rule AND"

Question

Quick review:

• Inference rule = conclusion + rule + premises
• Proof tree = conclusion + rule + sub-trees
• Backward proof search: given an input goal, try to build a proof tree by applying inference rules in bottom-up way (for example, the goal is the final conclusion, after applying a rule, it will generate a list of new sub-goals on the premises)

Problem:
Given an input goal (e.g. A AND B,C), assume that we apply the rule AND firstly on A AND B, then get two new sub-goals, the first one is A,C, the second one is B,C.
The problem is that A and B are useless, which means we can build a complete proof tree using only C. However, we have two sub-goals, then we have to prove C two times, so it is really inefficient.

Question:
For example, we have A AND B,C AND D,E AND F,G,H AND I. In this case, we only need D and G to build a complete proof tree. So how to choose the right rules to apply?

This is an example code in Ocaml:

(* conclusion -> tree *)
let rec prove goal =                                          (* the function builds a proof tree from an input goal *)
  let rule      = get_rule goal in                            (* get the first rule *)
  let sub-goals = apply_rule goal in                          (* apply a rule *)
  let sub-trees = List.map (fun g -> prove g) sub-goals in    (* prove sub-goals recursively *)
  (goal, rule, sub-trees)                                     (* return proof tree *)

Answer 1

If you want the shortest (shallowest) proof, which in this case uses disjunction introduction and avoids conjunction introduction, then you can look at techniques like iterative deepening. For instance you could change your code as follows:

let rec prove n goal =
  if n=0 then failwith "No proof found" else
  let rule      = get_rule goal in
  let sub-goals = apply_rule goal in
  let sub-trees = List.map (fun g -> prove (n-1) g) sub-goals in
  (goal, rule, sub-trees)

let idfs maxn goal =
  let rec aux n =
    if n > maxn then None else
    try 
      Some (prove n goal)
    with Failure _ -> aux (n+1) in
  aux 1

If you want to avoid re-doing the proof for a sub-goal that has already appeared, then you can use some form of memoization (a narrow form of lemma speculation/application really). See for instance the answers to this question, especially the second answer since prove is naturally recursive.

These suggestions do not touch the subject of how you pick the rules to apply, that is how exactly get_rule is coded. In practice, many options will be available and you would want to iterate through them.