ML Anthology

Splitting Without Backtracking

Alexandre Riazanov, Andrei Voronkov
IJCAI 2001 pp. 611-617
/ijcai/2001/riazanov2001ijcai-splitting/

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.

Semantic Scholar

Cite

Text

Riazanov and Voronkov. "Splitting Without Backtracking." International Joint Conference on Artificial Intelligence, 2001.

Markdown

[Riazanov and Voronkov. "Splitting Without Backtracking." International Joint Conference on Artificial Intelligence, 2001.](https://mlanthology.org/ijcai/2001/riazanov2001ijcai-splitting/)

BibTeX

@inproceedings{riazanov2001ijcai-splitting,
  title     = {{Splitting Without Backtracking}},
  author    = {Riazanov, Alexandre and Voronkov, Andrei},
  booktitle = {International Joint Conference on Artificial Intelligence},
  year      = {2001},
  pages     = {611-617},
  url       = {https://mlanthology.org/ijcai/2001/riazanov2001ijcai-splitting/}
}