Hi,
I wrote down two approaches using Horn clauses to obtain P-complete goal 
bases. Each has an unintuitive condition; in the first case, it serves 
to make the problem P-hard (otherwise it would be trivial), and in the 
second case it serves to make it stay in P (otherwise it might become 
too hard).

It may be possible to somehow justify these conditions, or to replace 
them by justifiable ones. Especially in the second case, where I need 
the condition to prove membership in P, one may be able to come up with 
a smarter proof using some weaker condition.

In any case, I guess this is just a proof of concept, and maybe better 
classes can be found with the same approach.

By the way, deciding whether some given goal base is valid is trivial 
for both classes (I didn't use satisfiability to define them after all).
Unfortunately, I guess now the "old" decision problem for them is as 
difficult as the "new" one I suggest. Still I think the new one makes 
more sense, and we might try to find a concrete example of a goal base 
class where these two problems are really different (or prove it for the 
little example I use in Section 1.2, if possible).

What do you guys think?
Cheers
Andi