This tool lets you practice bringing propositions into disjunctive normal form. The tool lets you submit intermediate steps, and provides feedback on how to continue. In order to report better feedback, the tool only accepts one step at a time. Therefore, it is advisable to make small steps only.
Associativity of operators is implicit. For example, the system will not distinguish between (p ∧ q) ∧ r and p ∧ (q ∧ r). In this case there is no need to write the parentheses. On the other hand, commutativity of operators is not dealt with automatically. You are allowed to rewrite p ∧ q into q ∧ p, but please do so in a separate step.
When entering formulas, take into account that parentheses have to be used when mixing different operators. The proposition (p ∧ q) ∨ r is accepted, but dropping the parentheses would result in a syntax error.
The tool uses unicode symbols for presenting the logical operators. For this to work, a unicode font has to be available to the web-browser. In particular, when using Internet Explorer, make sure that the webpages are displayed in a font that supports unicode. Go to the "Internet Options" menu-item (under "Extra"), followed by "Fonts" (in the "General" tab). Here you can select the font to be used for latin-based texts. Selecting "Lucida Sans Unicode" as the font for the webpage will do. If support of unicode is lacking, a rectangular box will be shown instead of the operator.