Splitting without Backtracking
Alexandre Riazanov
The case analysis principle is the core of tableau-based theorem
proving.
Is can also be integrated into saturation-based theorem proving in the
form of the splitting rule
S \bigcup {C \/ D} -> S \bigcup{C} \union S\bigcup {D} if C and D have no common variables
(in order to refute S\bigcup {C \/ D}, refute separately S\bigcup {C}
and S\bigcup {D}).
Splitting can be implemented by using backtracking but this is
difficult and affects the design of the system.
We introduce a much simpler form of splitting that does not use
backtracking:
S\bigcup {C \/D} -> S\bigcup {C \/p, \neg P \/ D}
where p is a new predicate.
This form of splitting is implemented in our resolution-and
superposition-based theorem prover Vampire.
Some optimisations to this technique are presented and experimentally
compared.
For more information see A. Riazanov, A. Voronkov, Splitting without
Backtracking, University of Manchester, CSPP-10.