Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-04 18:04:42 -0700 (Mon, 04 Jul 2005)
Revision: 7554
Log message:
We have at least partly working S4-prover. It can prove reflexivity, transitivity,
normality and self-referential example from Kuznets & Brezhnev paper.
Didn't test it for anything else yet.