Fixed-point Logics with Nondeterministic Choice

Authors: Dawar A.; Richerby D.

Source: Journal of Logic and Computation, Volume 13, Number 4, August 2003 , pp. 503-530(28)

Publisher: Oxford University Press

Key:

- Free Content

- New Content

- Subscribed Content

- Free Trial Content

Abstract:

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

Document Type: Research article

The full text electronic article is available for purchase. You will be able to download the full text electronic article after payment.

$40.03 plus tax Refund Policy