EDIT: Now with a concrete request to CAS experts (see the end of the post).
Let $G$ be a finite group, and $V$ a finite-dimensional representation of $G$. The classical invariant theory of $G$ and $V$ is a study of the $G$-invariants in the $K$-algebra $K\left[V\right]=\mathrm{S}\left(V^{\ast}\right)$, where $\mathrm{S}$ means the symmetric algebra. One has results like the Noether theorem, which says that over a field of characteristic $0$, the $G$-invariants in this $K$-algebra $\mathrm{S}\left(V^{\ast}\right)$ are generated (as a $K$-algebra) by the $G$-invariants in its submodule $\mathrm{S}^1\left(V^{\ast}\right)\oplus \mathrm{S}^2\left(V^{\ast}\right)\oplus ...\oplus \mathrm{S}^{\left|G\right|}\left(V^{\ast}\right)$.
Is there a similar theory, with similar bounds, for the $K$-algebra $\wedge \left(V^{\ast}\right)$ ? Actually this looks a bit simpler, because $\wedge^k \left(V^{\ast}\right)$ is nonzero only for $k\leq\dim V$; but $\dim V$ might still be greater than $\left|G\right|$. If there is an analogue of Weyl's theorem (Theorem A in 8.3 of Kraft-Procesi - see the Example in §8.5 for how I want to apply it), then we could limit ourselves to the case of $V$ being the regular representation, and then Noether's bound would follow. But there is no direct analogue of Weyl's theorem (in the sense of replacing $K\left[V^p\right]$ by $\wedge \left(V^{\ast p}\right)$ and $K\left[V^n\right]$ by $\wedge \left(V^{\ast n}\right)$).
The only thing from classical invariant theory which I can extend to this "anticommutative" (because $\wedge^k \left(V^{\ast}\right)$ can be seen as "anticommutative" polynomials on $V$) invariant theory is the Molien series, which takes the form
$\sum\limits_{d=0}^{\infty} \dim \left( \left(\wedge^d V\right)^G\right) T^d = \frac{1}{\left|G\right|}\sum\limits_{g\in G} \det\left(1+Tg\right)$
in our anticommutative setting, again only in the characteristic $0$ case. (Note that I have switched from $V$ to $V^{\ast}$, but this should not matter in the end since the the dimension of the invariants in some given representation always equals the dimension of the invariants in its dual - when we are in the characteristic $0$ case at least.)
Concrete request to anyone who has some experience with computer algebra systems:
Consider the exterior algebra freely generated by the differential forms $dx_1$, $dx_2$, ..., $dx_n$, $dy_1$, $dy_2$, ..., $dy_n$, $dz_1$, $dz_2$, ..., $dz_n$ over $\mathbb Q$. (This is the exterior algebra of a $3n$-dimensional vector space.)
Let the symmetric group $S_3$ act on this algebra by permuting $x$, $y$, $z$ (leaving the numeric indices unchanged).
For every $k\in\left\lbrace 1,2,...,n\right\rbrace $, the sum $dx_1\wedge dx_2\wedge ...\wedge dx_k + dy_1\wedge dy_2\wedge ...\wedge dy_k + dz_1\wedge dz_2\wedge ...\wedge dz_k$ is an invariant under this action. Does it lie in the subalgebra generated by invariants of smaller degree? (Note that it is enough to consider homogeneous invariants, so that there cannot be degree-reducing cancellations. Also note that it is easy to find a generating set of all invariants of given degree just by writing out all the monomials and averaging them over the action of $S_3$.) A negative answer for $n=k=7$ (or higher) would destroy the Noether bound in the anticommutative case.
I played with the idea of coding the exterior algebra as an algebraic type in Haskell, but finding out whether an element is generated by elements of smaller degree means solving a system of linear equations, and I don't have enough experience to code Gaussian elimination in Haskell. Other than that, there must surely be a CAS that knows how to work with anticommuting variables?