> PS I think Martin Mueller was doing some things with PN recently. Yes, he developed it into a proof set search, which takes transpositions into account. http://www.cs.ualberta.ca/~mmueller/publications.html Tapani Raiko