Prefix Notation For Propositional Formulas

Prefix notation, or also called Polish notation, is a way of writing mathematical expressions without the use of parentheses. Unlike the traditional, Infix notation that places operators betwen operands (like A+B), in Prefix notation the operators come before the operands (like +AB). It was introduced by Polish logician Jan Łukasiewicz.

Because of the structure of Prefix notation, it doesn't rely on parentheses. If you really want to, it's possible to insert parentheses into Prefix notation formula, but there is exactly 1 way to define the order of Prefix formula operators. For example, take a formula ((p→q)∧(q→r))→((p∨q)→r). Its Prefix form is →(∧(→(pq)→(qr)))(→(∨(pq)r)), or if parentheses are removed, →∧→pq→qr→∨pqr.

The algorithm that transforms an Infix formula to Prefix behaves like this:

1. For every item (atom or operator) in the input formula, do the following backwards:
   • If the current item is an atom (p, q, r, ...) then append it straight to the result.
   • If the current item is close parenthesis, push it to the stack.
   • If the current item is a negation operator, pop all negations from the stack straight into result. Push the current negation into stack.
   • If the current item is conjunction ∧, pop all operators with higher priority (that is negations), from the stack straight into result. Push the current conjunction into stack.
   • If the current item is disjunction ∨, pop all operators with higher priority (negations, disjunctions) from the stack straight into result. Push the current disjunction into stack.
   • If the current item is implication →, pop all the operators with higher priority (negations, disjunctions, conjunctions) from the stack straight into result. Push the current implication into stack.
   • If the current item is open parenthesis, pop the items from the stack straight into result, until a close parenthesis is reached in the stack. Dismiss the close parenthesis and just pop it from the stack and throw away.
2. Pop remaining stack items straight to the result.
3. Reverse the result.