OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation
Journal of Logic and Computation
Volume 13, Issue 4, June 2003: pp. 503530
Original Article Fixedpoint Logics with Nondeterministic Choice
Anuj Dawar and David Richerby
University of Cambridge Computer Laboratory, William Gates Building, J.J. Thomson Avenue, Cambridge, CB3 0FD, UK. Email: Anuj.Dawar@cl.cam.ac.uk, David.Richerby@cl.cam.ac.uk
The inductive operators nio (due to Arvind and Biswas) and cifp (due to Gire and Hoang) allow for a nondeterministic choice of tuples at each stage in the inductive construction of a relation. We consider the extensions of firstorder logic with each of these operators, presenting a formal semantics for each, in which formulae denote sets of relations. We derive normal forms for these formulae and prove that the operators have equal expressive power. Finally, we show that, by using an appropriate notion of satisfaction for nondeterministic formulae, essentially any computational complexity class defined in terms of nondeterministic Turing machines operating within polynomial time bounds can be expressed in terms of nondeterministic fixedpoint formulae.
Keywords: Finite model theory, complexity theory, fixedpoint logics, polynomialtime computation, nondeterminism.
Table of Contents
FullText PDF (285 KB)
