Splitting Without Backtracking
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.
Alexandre Riazanov, and Andrei Voronkov. 2001. Splitting Without Backtracking. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI-01. IJCAI, 611–616. https://ijcai.org/proceedings/2001/85
Riazanov, A., & Voronkov, A. (2001). Splitting Without Backtracking. In Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI-01 (pp. 611–616). IJCAI. https://ijcai.org/proceedings/2001/85
@inproceedings{ijcai2001p85,
title = {Splitting Without Backtracking},
author = {Riazanov, Alexandre and Voronkov, Andrei},
booktitle = {Proceedings of the Seventeenth International Joint Conference on
Artificial Intelligence, {IJCAI-01}},
publisher = {International Joint Conferences on Artificial Intelligence},
pages = {611--616},
year = {2001},
url = {https://ijcai.org/proceedings/2001/85},
}
TY - CPAPER TI - Splitting Without Backtracking AU - Riazanov, Alexandre AU - Voronkov, Andrei T2 - Proceedings of the Seventeenth International Joint Conference on Artificial Intelligence, IJCAI-01 PB - International Joint Conferences on Artificial Intelligence PY - 2001 SP - 611 EP - 616 UR - https://ijcai.org/proceedings/2001/85 ER -Copied
Machine-readable versions of this paper, for tools and AI agents:
