Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-09-22 13:43:54 -0700 (Thu, 22 Sep 2005)
Revision: 7777
Log message:

      1.Original set of prefix unification rules was incomplete for S4nJ, so it was slow on certain problems.
      I discovered t while working on a paper and now I believe the rules are complete.
      
      2.Because of (1) original formulation of Muddy Children
      could be solved in less than a second (vs half a minute before). But I replaced with with two more interesting formulations so the total time to check s4_tests actually increased.
      
      3.It seems also that the optimization which forces Jprover
      to prefer conclusion as a source of contradictions backfires in some cases:
      consider A1...An >- B & C
      and A1...An is complex
      it will try to "prove" B,A1...An first and then for C,A1...An and in some cases it might not be able to reuse the unifier of A1...An from B,Ai for C,Ai
      I'm not sure yet that this is actually what happens but I have examples when A >- B & C takes much more time than the sum of A >- B and A >- C

Changes	Path
+138 -16	metaprl/refiner/reflib/jtunify.ml
+40 -8	metaprl/theories/s4lp/s4_tests.ml
Binary	metaprl/theories/s4lp/s4_tests.prla