Refutation graphs

摘要

A graph-theoretic characterization of truth-functional consistency is introduced, providing a clear perspective on some resolution-based for deciding formulas in propositional and first-order logic. Various resolution strategies are analyzed in terms of “walks” about specially defined graphs. A new procedure—called Graph Construction—is presented that improves on the Model Elimination and SL strategies.