Oxford Journals
tools journals homepage advanced search contact help
Journal of Logic and Computation: Current Issue

OUP > Journals > Computing/Engineer. & Mathematics/Stats. > Journal of Logic and Computation

Journal of Logic and Computation

Volume 13, Issue 4, June 2003: pp. 503-530

Original Article
Fixed-point 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. E-mail: Anuj.Dawar@cl.cam.ac.uk, David.Richerby@cl.cam.ac.uk

The inductive operators nio (due to Arvind and Biswas) and c-ifp (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 first-order 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 fixed-point formulae.

Keywords: Finite model theory, complexity theory, fixed-point logics, polynomial-time computation, nondeterminism.

Table of Contents   Full-Text PDF (285 KB)

Oxford University Press
Published by Oxford University Press
Copyright ©Oxford University Press 2003
Print ISSN: 0955-792X  Online ISSN: 1465-363X.
Oxford University Press Privacy Policy and Legal Statement