A Python tool for testing normalization in Natural Term Logic

https://github.com/owl77/natlog/blob/main/ntltest3.txt

This tool allows you to interactively reduce NTL terms and to ultimately check that the normal form is independent of the path chosen. In the example above we start from 

$\Pi^{(1,1,2)} \Upsilon^{\{1,4\}\{2\}\{3\}} \Pi^{(1,3)} \Pi^{(1,1)} C D D D D C B C$

and we derive the normal form 

\[ \Upsilon^{\{1,2\}\{3\}\{4\}\{5\}} \Pi^{(1,4)} C \Pi^{(1,1,1,1,1)} D \Pi^{(1,1,1,1,1)} D C I I I I I I I I \Pi^{(4,1,1,1,1)} D \Upsilon^{\{4\}\{1\}\{2\}\{3\}\{5\}\{6\}} \Pi^{(1,2,1,1,1)} D B C C I I I I I I \]

by following several different paths.  Here the primitive terms $B,C,D$ have arities $1,2,5$ respectively.

The program is run from the command line : python -i reductions.py and in general one needs to specify the primitive terms and their arities through the command AddPrimitive(name, value). But $B,C$ and $D$ above come by default.