Decidability of Formulas in Graph Theory

Article type: Research Article

Authors: Moser, Louise E.^{; *}

Affiliations: Department of Mathematics and Computer Science, California State University, Hayward, Hayward, CA 94542

Note: [*] Current address: Department of Computer Science, University of California, Santa Barbara, CA 93106. Supported by the National Science Foundation under grant DCR-8408544 and by the National Security Agency, Office of Cryptographic Research, under grant MDA904-84-H-0009.

Abstract: 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.

DOI: 10.3233/FI-1989-12204

Journal: Fundamenta Informaticae, vol. 12, no. 2, pp. 163-180, 1989