Path Dissolution: A Strongly Complete Rule of Inference
Abstract
We introduce path dissolution, a rule or inference that operates on formulas in negation normal form. Path dissolution is strongly complete; i.e., it has the property that, given an unsatisfiable ground formula, any sequence of dissolution steps will produce the empty graph. This is accomplished by strictly reducing (at each step) the number of c-paths in the formula. Dissolution, unlike most resolution-based inference rules, does not directly lift into first-order logic; techniques for employing dissolution at the first order level are discussed.
Cite
Text
Murray and Rosenthal. "Path Dissolution: A Strongly Complete Rule of Inference." AAAI Conference on Artificial Intelligence, 1987.Markdown
[Murray and Rosenthal. "Path Dissolution: A Strongly Complete Rule of Inference." AAAI Conference on Artificial Intelligence, 1987.](https://mlanthology.org/aaai/1987/murray1987aaai-path/)BibTeX
@inproceedings{murray1987aaai-path,
title = {{Path Dissolution: A Strongly Complete Rule of Inference}},
author = {Murray, Neil V. and Rosenthal, Erik},
booktitle = {AAAI Conference on Artificial Intelligence},
year = {1987},
pages = {161-166},
url = {https://mlanthology.org/aaai/1987/murray1987aaai-path/}
}