Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-01 09:15:20 -0800 (Sun, 01 Jan 2006)
Revision: 8387
Log message:

      Rephrased the Provable intro rules, using the SubLogic judgment
      instead of a fixed logic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-01 12:56:24 -0800 (Sun, 01 Jan 2006)
Revision: 8388
Log message:

      Added initial Provability tactic.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-01 13:53:31 -0800 (Sun, 01 Jan 2006)
Revision: 8389
Log message:

      Added Itt_list_set for new set-style theorems about lists.
      Eventually we should move some theorems from Itt_list2 into
      this file.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 11:27:09 -0800 (Mon, 02 Jan 2006)
Revision: 8390
Log message:

      Added less ambiguous names for some of the refiner functions (for names
      like "eq", "hyps", "concl", etc.).
      
      Partial progress in Provable theorems, added a unification tactic.
      
      This commit is mainly just in case we have a power failure here--
      it is raining very hard.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 16:23:06 -0800 (Mon, 02 Jan 2006)
Revision: 8391
Log message:

      Added vector binders to the BTerm normalizer.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 16:27:30 -0800 (Mon, 02 Jan 2006)
Revision: 8392
Log message:

      Rename Meta_extensions_theory to Meta_context_theory.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-02 17:32:11 -0800 (Mon, 02 Jan 2006)
Revision: 8393
Log message:

      Still working on well-formedness of reflected vector terms.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-03 13:05:49 -0800 (Tue, 03 Jan 2006)
Revision: 8394
Log message:

      Added a simple forward-chaining tactic in support/tactics/forward.ml
      It is a lot like dT elimination, but it checks that progress is being made.
      Perhaps there is a more generic way to do it.  The proof cache used to
      do forward chaining, and I imagine JProver does too.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-04 08:30:00 -0800 (Wed, 04 Jan 2006)
Revision: 8396
Log message:

      Changed the proof witness code in Itt_hoas_sequent_proof from
      unification-based to naming-based.
      
      Added more forward reasoning.  We have most of the facts, but
      we need a few more about mk_bterm, mainly that if a mk_bterm
      is well-formed, so are its subterms.  The theorems in
      Itt_hoas_bterm_wf are currently unproved.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-04 17:26:50 -0800 (Wed, 04 Jan 2006)
Revision: 8397
Log message:

      Completed proofs in Itt_hoas_bterm_wf. However, I added a well-formedness
      subgoal (subterms in List) to mk_bterm_wf_forward. Does it matter?
      
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-01-04 17:51:15 -0800 (Wed, 04 Jan 2006)
Revision: 8398
Log message:

      Now really proved theorems in Itt_hoas_bterm_wf, with useless well-formedness subgoals removed.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-05 13:16:41 -0800 (Thu, 05 Jan 2006)
Revision: 8401
Log message:

      Include the SVN revision number (when available) in the MetaPRL version string.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-05 17:18:52 -0800 (Thu, 05 Jan 2006)
Revision: 8406
Log message:

      - Minor clean-up of the debugging code.
      - Added a license header.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-05 20:29:45 -0800 (Thu, 05 Jan 2006)
Revision: 8408
Log message:

      Re-added the Itt_hoas_sequent.bterm2_is_bterm rule.  However, this is
      not recommended because this kind of rule can break normal dT reasoning.
      
      Instead, I think these kind of rules are better accomplished with some
      kind of forward chaining (even the autoT kind should work fine, but I
      don't know how to enable it).
      
      Replaced the tactic in Pmn_core_terms.intro_term_TyAll with a terminating
      version.  Currently, expand_all () takes about 10sec for me.  Let me
      know if it doesn't terminate for you.
      
      Re-added pmn_core_terms.prla, so that you get the terminating tactics.
      Will remove this again once we all the proofs work.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-05 22:36:35 -0800 (Thu, 05 Jan 2006)
Revision: 8409
Log message:

      (Issue 560) Give a better error message when a theory does not exist.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-05 22:42:29 -0800 (Thu, 05 Jan 2006)
Revision: 8410
Log message:

      (Issue 561) The format of editor/ml/mldebug.dir is different on Windows.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-06 08:43:04 -0800 (Fri, 06 Jan 2006)
Revision: 8411
Log message:

      Updated the incomplete proofs.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 10:50:37 -0800 (Fri, 06 Jan 2006)
Revision: 8413
Log message:

      Incrementing the version numbers for the ASCII and binary formats to account
      for the new "const" modifier added in rev 8383.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 14:14:27 -0800 (Fri, 06 Jan 2006)
Revision: 8415
Log message:

      Spelling fixes

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 15:40:10 -0800 (Fri, 06 Jan 2006)
Revision: 8416
Log message:

      Revision-based status checking.
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-01-06 17:55:10 -0800 (Fri, 06 Jan 2006)
Revision: 8417
Log message:

      Fixed the problem noticed by Aleksey - one-only-constraint case was treated incorrectly

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 21:31:31 -0800 (Fri, 06 Jan 2006)
Revision: 8418
Log message:

      - Itt_nat should extend Itt_omega
      
      - Now that "meta" is a virtual theory (that is needed for "omake doc"), it
        needs to be listed explicitly in THEORIES_ALL (in mk/defaults)
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 22:16:30 -0800 (Fri, 06 Jan 2006)
Revision: 8419
Log message:

      - Updated arithT to generate fewer wf subgoals.
      - Proved all the rules that were left unproven in Itt_int_arith.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-06 23:27:00 -0800 (Fri, 06 Jan 2006)
Revision: 8420
Log message:

      Minor omegaT optimization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-07 00:07:35 -0800 (Sat, 07 Jan 2006)
Revision: 8421
Log message:

      Another minor omegaT optimization (that should reduce the number of wf
      subgoals that it generates).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-07 09:14:17 -0800 (Sat, 07 Jan 2006)
Revision: 8422
Log message:

      Making "omake clean" more clean.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-07 10:43:32 -0800 (Sat, 07 Jan 2006)
Revision: 8423
Log message:

      Simplfy the BTerm normalizer a bit.  This now uses a single
      sweepDnC pass to push binds into the subterms, then does
      a rippling phase.
      
      This cuts the number of primitive steps by about a factor of 3,
      but it is still huge, around 30k for wf_term_TyAll.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-07 11:36:28 -0800 (Sat, 07 Jan 2006)
Revision: 8424
Log message:

      Adding poplmark/naive to the "THEORIES=all" list.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-07 13:36:44 -0800 (Sat, 07 Jan 2006)
Revision: 8425
Log message:

      In proof browsing UI ("down 0"), give more information about the rewrites.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-08 12:51:03 -0800 (Sun, 08 Jan 2006)
Revision: 8427
Log message:

      Updated the forward-chainer to use a more efficient algorithm (bug #562).
      
      Made some progress with reflection, intro_term_TyFun is now proved.
      
      The following rule would be *really* nice, but I don't know if it
      is true or provable.
      
         <H>; append{l1; l2} in list; <J>; l1 in list; l2 in list >- C -->
         <H>; append{l1; l2} in list; <J> >- C
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-01-08 15:57:10 -0800 (Sun, 08 Jan 2006)
Revision: 8430
Log message:

      Added sqsimple{BTerm{'n}} to sqsimple resource
      
      Note: I have not proven bterm_sqsimple2 in order not to create conflict with
      Jason's work.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-08 21:01:22 -0800 (Sun, 08 Jan 2006)
Revision: 8431
Log message:

      Ok, enough for now.  The basic rules in Pmn_core_terms are proved.
      
      Forward-chaining has the following problem--a forward chaining
      rule might introduce a wf subgoal that would normally be proved
      by forward chaining on a later hyp.  Using forward chaining on
      the wf subgoal will result in a loop.  NOTE: wrt forward chaining,
      this is a major issue.
      
      For the moment, I added precedences to the forward chainer.  This
      is only a temporary fix.
      
      Added a fair number of new rules.  This is ad-hoc at the moment.
      Basically, I just see what isn't proved, and I add the appropriate
      theorems.  I'm not sure if we can make this systematic, but we
      should think about it.
      
      All rules in Pmn_core_terms are proved, but just *look* at the stats!
      500k primitive steps is totally--umm--amazing/terrible etc.
      Time for expand_all ():
         User time 293.000000; System time 2.820000; Real time 340.365773
      
         Refiner status:
            wf_term_TyTop
            is a derived object with a complete grounded proof (1 rule boxes, 3164 primitive steps, 248 dependencies)
         Refiner status:
            wf_term_TyFun
            is a derived object with a complete grounded proof (1 rule boxes, 15765 primitive steps, 249 dependencies)
         Refiner status:
            wf_term_TyAll
            is a derived object with a complete grounded proof (1 rule boxes, 35857 primitive steps, 254 dependencies)
         Refiner status:
            wf_Types
            is a derived object with a complete grounded proof (1 rule boxes, 38 primitive steps, 260 dependencies)
         Refiner status:
            mem_term_TyTop_Types
            is a derived object with a complete grounded proof (1 rule boxes, 101 primitive steps, 264 dependencies)
         Refiner status:
            mem_term_TyFun_Types
            is a derived object with a complete grounded proof (1 rule boxes, 103 primitive steps, 264 dependencies)
         Refiner status:
            mem_term_TyAll_Types
            is a derived object with a complete grounded proof (1 rule boxes, 105 primitive steps, 264 dependencies)
         Refiner status:
            intro_term_TyTop
            is a derived object with a complete grounded proof (1 rule boxes, 14782 primitive steps, 295 dependencies)
         Refiner status:
            intro_term_TyFun
            is a derived object with a complete grounded proof (1 rule boxes, 254485 primitive steps, 295 dependencies)
         Refiner status:
            intro_term_TyAll
            is a derived object with a complete grounded proof (1 rule boxes, 491120 primitive steps, 300 dependencies)
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-01-09 12:51:02 -0800 (