An explicit algorithm to test whether a string of symbols is or is not well-formed in this language. Consider the set of five symbols, $\{ (, ), p, ', *\}$. A variable is defined as $p$ followed by zero or more $'$s. A wff is inductively defined as follows: $1$. Every variable is a wff. $2$. If $x$ and $y$ are formulas, so is $(x*y)$. $3$. Nothing else is a formula. This is really just a simplified version of a propositional logic language. My problem, though, is with clause 3 of the definition. It is easy to prove that a particular sequence of symbols is a wff. How, though, does one actually prove that a particular sequence, like $p**pp$, is NOT a wff? More precisely, and this is my real question, is there an explicit algorithm that takes a string and returns Yes if it is a wff, and No if it is not? And can someone describe the algorithm?
 A: You're asking a particular question:

How… does one actually prove that a particular sequence, like p∗∗pp, is NOT a wff

and a general question:

is there an explicit algorithm that takes a string and [ decides if it is a wff ]

The particular question has a shorter answer.  The rules you gave require that a wff must begin with p (rule 1) or with ( (rule 2).  The string p**pp begins with p so if it is a wff it must be a variable.  But a variable is a p followed by zero or more 's, and p**pp is not that, so it is not a variable.  So by rule 3, it is not a wff.
The more general question has a very interesting answer.
There are many explicit algorithms that do what you want.  They come under the general heading of “parsing algorithms”.  A parsing algorithm takes an unstructured sequence of symbols and decides if it can be understood as a meaningful utterance in a certain language. In your example the language is the syntax of wffs. Parsing is an interesting topic, and it is impossible to give a complete answer here.  (I highly recommend Parsing Techniques: A Practical Guide by Grune and Jacobs, available for free download from the author's web site.)
I can outline one example an algorithm that parses the language you described.  This uses the method of recursive descent parsing:

*

*You imagine that the parser will scan over the symbols of the input from left to right.

*You write a function that recognizes a variable.  This is easy: if the next unscanned symbol is p the function will consume the p and then consume any following ' symbols, and yield success; otherwise it yields failure, which indicates that the unscanned part of the input does not look like a variable

*You write a function that recognizes if the input begins with a wff, and if so scans the entire wff:

*

*It first uses the variable-recognizing function to see if it can recognize a variable at the beginning of the unscanned input.  If so, it yields success, because a variable is a wff.

*Otherwise, the function looks to see if the next unscanned symbol is a (.  If not, it can fail immediately because every wff that is not a variable begins with a (

*If the upcoming symbol is a (, then it consumes the (.  Then it calls itself recursively scan the following wff.  If this recursive call fails, the failure is propagated back up, because what we have is ( followed by a non-wff.

*But if the ( is followed by a valid wff, the function then looks to see if the following symbol is *.  If not, it fails immediately.

*But if there is a *, the function consumes it and makes a second recursive call, looking for a second wff.

*If this second recursive call also succeeds then the function checks to see if the upcoming symbol is ), and reports success if it is.



