---
title: "Splitting Without Backtracking"
authors:
  - "Alexandre Riazanov"
  - "Andrei Voronkov"
doi: ""
url: "https://ijcai.org/proceedings/2001/85"
pdf: "https://ijcai.org/proceedings/2001/0085.pdf"
venue: "Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence"
year: 2001
pages: "611-616"
track: ""
keywords:
---

# Splitting Without Backtracking

Alexandre Riazanov, Andrei Voronkov

*Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence*, pages 611-616.

## Abstract

Integrating the splitting rule into a saturation-based theorem prover may be highly beneficial for solving certain classes of first-order problems. The use of splitting in the context of saturation-based theorem proving based on explicit case analysis (as implemented in SPASS) employs backtracking which is difficult to implement as it affects design of the whole system. Here we present a “cheap” and efficient technique for implementing splitting that does not use backtracking.