Decidability of Formulas in Graph Theory
Louise E. Moser · Fundamenta Informaticae · 1989
A decision procedure is given for determining the validity of unquantified formulas in graph theory. The procedure, which decides equality and containment relations for vertex, edge, and graph terms, reduces to a decision procedure for propositional calculus. The correctness of the procedure is proved using model theory based on the axioms for graph theory provided. The complexity of the algorithm and its limitations are discussed.