Ordering Subgoals in a Backward Chaining Prover

Many automated theorem provers are based on backward chaining: reasoning starts from a goal statement which we aim to prove and each inference step reduces one of the goals to a (possibly empty) set of new subgoals. We thus maintain a set of open goals that need to be proven and the proof is complete once the open goal set becomes empty. For each goal, there can be several valid inferences, resulting in different successor goal sets and selecting the right inference constitutes the core problem of such theorem provers which has been thoroughly studied in the past half century. There is, however, another decision to make during proof search, which has been largely underappreciated in the theorem proving community: this is the order in which we select goals from the open goal set. When goals do not share variables, their ordering is irrelevant as their proofs do not influence each other. However, variables establish connections between goals and a certain proof of one goal can result in variable instantiations that make it impossible to prove another goal. In this paper, we look at the leanCoP connection tableau calculus and explore how goal ordering influences theorem proving performance. leanCoP is a first order theorem prover which translates the problem into clausal normal form and builds a proof tree whose nodes are goals, using two kinds of inference steps: extension steps add children to a leaf node while reduction steps close leaf nodes. In leanCoP both steps are applied on the leftmost open node by default.