Can well-formed formulas in predicate logic for a given signature be recognized in LOGSPACE?

Question

I read that visibly pushdown languages are supposed to model the typical simple formal languages like XML better than deterministic context free languages. The visibly pushdown languages can be recognized in LOGSPACE. I wonder whether the well-formed formulas in predicate logic for a given signature are a visibly pushdown language, or can at least be recognized in LOGSPACE.

Here is a typical well-formed formula in predicate logic, for the given signature $(f(\cdot,\cdot), g(\cdot))$:

$\forall x (f(x,y)=z \land g(z)=x)$

A corresponding context free grammar would be

$P \to T=T$
$P \to (P \land P)$
$P \to (P \lor P)$
$P \to \lnot P$
$P \to \forall V P$
$P \to \exists V P$
$T \to V$

$V \to x$
$V \to y$
$V \to z$

$T \to f(T,T)$
$T \to g(T)$

Some people prefer to use reverse polish notation:

$xyfz=zgx=\land x\forall$

A corresponding context free grammar would be

$P \to TT=$
$P \to PP\land$
$P \to PP\lor$
$P \to P\lnot$
$P \to PV\forall$
$P \to PV\exists$
$T \to V$

$V \to x$
$V \to y$
$V \to z$

$T \to TTf$
$T \to Tg$

Because I have now written down two explicit grammars, let the question just be whether these two grammars generate visibly pushdown languages, or can at least be recognized in LOGSPACE.