|
|
Gire and Hoang introduce a fixed-point logic with a `symmetric' choice operator that makes a nondeterministic choice from a definable set of tuples at each stage in the inductive construction of a relation as long as the set of tuples is an automorphism class of the structure. We present the first clean definition of the syntax and semantics of this logic and investigate its expressive power. We extend the logic of Gire and Hoang with parameterized and nested fixed points and first-order combinations of fixed points. We show that the ability to supply parameters to fixed points is crucial, strictly increasing the power of the logic. Our logic can express the graph isomorphism problem and we show that, on almost all structures, it captures $\mathrm{\mathbf{P}^{GI}}\!$, the class of problems decidable in polynomial time by a deterministic Turing machine with an oracle for graph isomorphism.
|
© 2002-2003 Kurt Gödel Society, Norbert Preining. |
2003-06-04
 | |
Print this page