Path Dissolution: A Strongly Complete Rule of Inference

Book One

Volume

Proceedings of the AAAI Conference on Artificial Intelligence, 6

Automated Reasoning

We introduce path dissolution, a rule of 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.