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.
      

Changes  Path
+48 -61 metaprl-branches/S4-jprover/refiner/reflib/jall.ml
+57 -14 metaprl-branches/S4-jprover/refiner/reflib/jordering.ml
+26 -19 metaprl-branches/S4-jprover/refiner/reflib/jtunify.ml
+4 -1 metaprl-branches/S4-jprover/refiner/reflib/jtunify.mli
+10 -1 metaprl-branches/S4-jprover/theories/s4lp/s4_logic.ml
Added metaprl-branches/S4-jprover/theories/s4lp/s4_logic.prla
Properties metaprl-branches/S4-jprover/theories/s4lp/s4_logic.prla