A Python tool for testing normalization in Natural Term Logic

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

This tool allows you to interactively reduce NTL terms and to ultimately check that the normal form is independent of the path chose. 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,5\}\{2\}\{3\}\{4\}} \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 \Pi^{(1,2,1,1,1)} D B C C I I I I I I$

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