Normalizer program

In this section I will briefly explain how to use the normalizer program at http://tcw2.ppsw.rug.nl/~towr/TEST/test.php. At the top of the programs page you will see a brief explanation of the syntax, underneath which are written some examples. Table 8 shows how to translate logical expressions to the right syntax

table 8.

name	normal	program
falsum	$\bot$	false
verum	$\top$	true
OR	p$\vee$q	or(p,q)
AND	p$\wedge$q	and(p.q)
NOT	$\neg$p	not(p)
Known	$K p$	K(p)
Maybe	$Mp$	M(p)

To normalize an expression you simply write in the inputfield and press the button 'submit query'. If you want the output in tree-form you can check the 'use tree' box.
After you have submitted an expression the page will reload showing the normalizing process one step at a time. The part of the expression that has changed is colored red when it has been reduced, and green when it has been rewritten. If a rule form table six has been used (normalization rules for S5) $\lambda$, $\pi$ and $K\beta$ or $M\beta$ are colored purple, yellow and blue respectively.

Sourcecodes for the program can be found at the end of the page.