This talk serves as an introduction to finite model theory -- an area of
mathematical logic. Currently, finite model theory is used in theoretical
computer science to study the logical foundations of computational complexity.
This is done in the hope of understanding resource bounded computation from a
machine independent point of view.

The ordinary way to solve a problem in computer science is to demonstrate an
algorithm which will run on an appropriate machine model of computation. In
fact, computer science is often succinctly defined as the study of algorithms.

We shall explain descriptive complexity -- the notion of solving a problem by
simply expressing its solution as a formula in some logic. This turns out to be
a more natural approach from the mathematical point of view, as it does not
involve converting the natural domain of discourse (say graphs) into bits of a
binary string to be processed by the instruction set of a particular machine.

The main interest and excitement is in the close connection between this
approach of expressing a solution (with a formula in some logic) to the more
classical approach of providing an algorithm (with a program to run on some
machine). In particular, relating cyclic first-order formulas in logic to
polynomial time bounds on machines, we are left with a tantalizing question: Is
there an effective enumeration of all the polynomial time computable properties
of graphs? We illustrate how the answer to this and other related questions has
a direct bearing on P vs. NP --  the most famous unresolved problem in
theoretical computer science.