Every formula is logically equivalent to a

Every quantifier in a formula can be classified as a\E w \A x P(w, x) => \A y \E z P(z, y) \A w \A y \E x \E z (P(w, x) => P(z, y)) \A w \A y \E x (P(w, x) => P(x, y))

Formulas can be transformed systematically into prenex formulas using changes of bound variables and the following logical validities.

\A x P <=> P (x not free in P) \E x P <=> P (x not free in P) \A x ~P <=> ~\E x P \E x ~P <=> ~\A x P \A x (P /\ Q) <=> \A x P /\ \A x Q \E x (P /\ Q) <=> \E x P /\ Q (x not free in Q) \A x (P \/ Q) <=> \A x P \/ Q (x not free in Q) \E x (P \/ Q) <=> \E x P \/ \E x Q \A x (P => Q) <=> \E x P) => Q (x not free in Q) \A x (P => Q) <=> P => \A x Q (x not free in P) \E x (P => Q) <=> \A x P => \E x Q F(\A x P) <=> (F(true) /\ \A x P) \/ (F(false) /\ ~\A x P)

The instantiate and fix commands enable users to eliminate certain prenex-universal and prenex-existential quantifiers from facts. The generalization and specialization proof methods provide the corresponding functionality for conjectures.