Describing Graphs: A First-Order Approach to Graph Canonization

Abstract

In this paper we ask the question, “What must be added to first-order logic plus least-fixed point to obtain exactly the polynomial-time properties of unordered graphs?” We consider the languages Lkconsisting of first-order logic restricted to k variables and Ckconsisting of Lkplus “counting quantifiers”. We give efficient canonization algorithms for graphs characterized by Ckor Lk. It follows from known results that all trees and almost all graphs are characterized by C2.