Prenex Normal Form Generator

Welcome to the Prenex Normal Form Generator. This converter will take a formula of first-order logic and transform it into prenex normal form.

• Use any lowercase letter a-z for variables.
• Use A for the universal quantifier "forall" and use E for the universal quantifier "exists".
• Use any other uppercase letter, B-D or F-Z, to denote a quantifier-free subformula.
  • Include free variables in parentheses:
    • P(x,y) means P depends on x and y;
    • P(x) means P depends only on x;
    • P means P depends on no variables
• Use ampersand & for "and" and use the vertical bar | for "or".
• Use -> for "implies" and use <-> for "if and only if".
• Use ~ for negation.

About

The heart of the PNFG is written in C. The user-interface is a mishmash of PHP, JavaScript and Ajax.

This is an alpha version of the Generator. Please report any bugs to alexander@math.ohio-state.edu

When you're finished here, make sure to check out the Inverse Graphing Calculator!