= Partial fixed-point logic
{title2=$\mathrm{PFP}$}
= PFP
{c}
{synonym}
Extend <first-order logic> by iterating definable relation operators from the empty relation. If iteration reaches a fixed point, use that relation; if it enters a nontrivial cycle, the partial fixed point is the empty relation. For a fixed arity on a finite universe, a relation requires polynomially many bits and there are exponentially many states, so iteration is evaluable in <PSPACE>. On finite ordered structures this logic captures PSPACE.
Back to article page
