harrisj: Thanks for the bouquet. It's only because I happen to be good at remembering this esoteric excreta.

You mentioned verification in P-time, and I think it's worth exploring what that means. One technical definition of the class NP is:

NP is the class of decision problems (languages)Lsuch that there is a polynomial time functionf(x,c)wherexis a string,cis another string whose size is polynomial in the size ofx, andf(x, c)=Trueif and only ifxis inL.

(taken from the comp.theory FAQ)

As an example, *x* might be a graph,
*c* might be a path in that graph, and *f(x, c)*
is the function "is *c* a Hamiltonian path in the graph
*x*?"

There are at least *three* kinds of questions that
you may want to ask about this problem, given *x*.
They are:

- Is
*x*in*L*, that is, does there exist*c*such that*f(x, c)=True*? That question corresponds to "does the graph have a Hamiltonian cycle"? Or "is the number composite"? This is called a "decision problem", and is*not*necessarily verifiable in P (unless P=NP, of course), because verifying an answer is identical to finding the answer. - Given
*x*, give me a*c*which proves that*x*is in*L*. This kind of problem is trivially certifiable in P, because all you need to do is take the certificate*c*and compute the value of*f(x, c)*. This question corresponds to "find me a Hamiltonian cycle in this graph", or "find me factors of this number". - Given
*x*, find me the certificate*c*which minimises (or maximises) some cost function*cost(c)*. This is called an "NP optimisation problem", and corresponds to something like "find me the Hamiltonian cycle of minimal distance" (i.e. the travelling salesman problem). I don't know whether this kind of problem is certifiable in P or not. Could someone please let me know?

Now to EXPTIME. EXPTIME-hard problems are not certifiable in P-time if the certificate is polynomial in the size of the input. If they were, you could construct a nondeterministic polynomial algorithm to solve them. (Nondeterministically guess the certificate in NP time then test it in P time.) So I guess EXPTIME-hard public-key systems and zero-knowledge proof systema aren't feasable. Darn.

If the certificate were not polynomial in the size of the input, that might be a different matter. That is, certifying EXPTIME-hard problems might be polynomial in the size of the certificate. I'm not sure about that one.

EXPTIME-hard problems often turn up when dealing with logic and theorem proving (e.g. constraint systems, conditional logic) or formal languages and the machines which generate/recognise them (e.g. tree automata). Here are some example EXPTIME-complete problems:

- Evaluation of datalog queries for single rule programs containing only a single clause.
- For tree automata, the intersection problem (i.e. given two tree automata, is the intersection of their languages empty) and equivalence problem (do two given tree automata accept the same language)
- Removing recursion from formulas in the mu calculus (i.e. given a recursive formula, give me a non-recursive equivalent if it exists)
- Satisfiability for definite set constraints
- Determining a winning strategy for chess generalised to an N*N board or go generalised to an N*N board. I'm not entirely sure how you generalise chess piece movement, but there you go.

And just for fun, here are a couple of NEXPTIME-complete problems:

- Satisfiability for two-variable first-order logic.
- Provability in first-order multiplicative additive linear logic

Naturally, NEXPTIME-complete problems are certifiable in EXPTIME.

Happy theory nerding.