We introduce two algebraic propositional proof systems F-NS
and F-PC. The main difference of our systems from (customary)
Nullstellensatz and Polynomial Calculus is that the polynomials
are represented as arbitrary formulas (rather than sums of
monomials). Short proofs of Tseitin's tautologies in the
constant-depth version of F-NS provide an exponential
separation between this system and Polynomial Calculus.

We prove that F-NS (and hence F-PC) polynomially simulates
Frege systems, and that the constant-depth version of F-PC over
finite field polynomially simulates constant-depth Frege systems
with modular counting. We also present a short constant-depth
F-PC (in fact, F-NS) proof of the propositional pigeon-hole
principle. Finally, we introduce several extensions of our
systems and pose numerous open questions.