Emperors and Tree Prover Updates
I've uploaded another revision of the emperors paper. The best thing about this version is that it's four pages shorter than the previous ones.
Unrelatedly, I've removed the Herbrand restriction from my tree prover. The restriction says that a Gamma node should not be expanded more often than there are closed terms on the branch. But currently, the prover doesn't keep track of the number of closed terms, it only keeps track of the number of function symbols (including 0-place function symbols, i.e. individual constants). So if a lot of s(0), s(s(0)), etc. are on a branch (as in this proof, where I noticed the bug), the prover wrongly applied the Herbrand restriction, thinking all of them are only two closed terms.
All my testcases work just as well without the Herbrand restriction. If you find a case where the performance got worse, please let me know. It shouldn't be difficult to fix it (rather than removing it completely).