Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-04-01 13:07:36 -0800 (Sat, 01 Apr 2006)
Revision: 8984
Log message:

      Allow sequents with non-zero depth.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-01 13:24:51 -0800 (Sat, 01 Apr 2006)
Revision: 8985
Log message:

      Filter_reflection follow-up to Alexei's previous commit.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-04-01 13:35:56 -0800 (Sat, 01 Apr 2006)
Revision: 8986
Log message:

      Fixed some broken proofs.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-01 13:52:15 -0800 (Sat, 01 Apr 2006)
Revision: 8987
Log message:

      Couple of minor optimizations.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-01 14:28:52 -0800 (Sat, 01 Apr 2006)
Revision: 8988
Log message:

      Moved couple of lemmas from itt_list_sloppy to itt_nat.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-01 16:20:04 -0800 (Sat, 01 Apr 2006)
Revision: 8989
Log message:

      Modified the sequent_bterm forward rule.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-01 17:24:27 -0800 (Sat, 01 Apr 2006)
Revision: 8990
Log message:

      Added 2 nth_hyp rules.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-04-01 22:54:06 -0800 (Sat, 01 Apr 2006)
Revision: 8991
Log message:

      Now I define Sequent<--> Sequent{0}. I did not make it as iform, because it would break a lot of proofs

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-02 00:10:31 -0800 (Sun, 02 Apr 2006)
Revision: 8992
Log message:

      Fully proved the test rule in Pmn_core_terms_test.
      

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-04-02 00:37:04 -0800 (Sun, 02 Apr 2006)
Revision: 8993
Log message:

      Fixed a broken proof

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-04-02 00:47:16 -0800 (Sun, 02 Apr 2006)
Revision: 8994
Log message:

      Proved two simple theorems

Changes by: Alexei Kopylov (kopylov at cs.caltech.edu)
Date: 2006-04-02 00:49:13 -0800 (Sun, 02 Apr 2006)
Revision: 8995
Log message:

      Fixed the last broken proof

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-02 15:35:45 -0700 (Sun, 02 Apr 2006)
Revision: 8996
Log message:

      Minor optimization in autoT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-02 18:08:08 -0700 (Sun, 02 Apr 2006)
Revision: 8997
Log message:

      Small optimization of the elim part of autoT.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-02 19:41:39 -0700 (Sun, 02 Apr 2006)
Revision: 8998
Log message:

      Another "elim in autoT" optimization.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-02 20:41:59 -0700 (Sun, 02 Apr 2006)
Revision: 8999
Log message:

      autoT: split the reduceT step into two: "rw reduceC 0" and "reduceHypsT" and
      reordered "rw reduceC 0" to happen _before_ the "onSomeHyp dT" step instead of
      after. This speeds up "status-all" by over 25%!
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-02 21:06:29 -0700 (Sun, 02 Apr 2006)
Revision: 9000
Log message:

      Added equalityElimination rule (which postulates that any witness for an
      equality is an "it") to AutoOK part of elim (instead of the AutoComplete part
      of it, where it used to be). I've also added an appropriate guard to it to
      make sure that it will only be used when it can actually make progress.
      
      P.S. This commit breaks three proofs in itt_hoas_bterm_wf; will fix those
      in a little while.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-02 21:18:10 -0700 (Sun, 02 Apr 2006)
Revision: 9001
Log message:

      Added bterm_neq_var and var_neq_bterm to the elim resource as Xin requested.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-02 21:51:41 -0700 (Sun, 02 Apr 2006)
Revision: 9002
Log message:

      - Forward: allow forward-chaining rules to thin the original hyp.
      
      - Reflection: In forward-chaining rules that are "if and only if", thin the
        original hyp, whenever possible.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 02:12:22 -0700 (Mon, 03 Apr 2006)
Revision: 9003
Log message:

      Follow some forward-chaining rules by an appropriate reduceC to simplify the arithmetic in
      CVar{...} and BTerm{...} arguments in newly generated hyps.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 02:55:28 -0700 (Mon, 03 Apr 2006)
Revision: 9004
Log message:

      Wrote another elimination tactic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 04:48:21 -0700 (Mon, 03 Apr 2006)
Revision: 9005
Log message:

      We no longer need reduceC in the forward-chainer.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 16:49:30 -0700 (Mon, 03 Apr 2006)
Revision: 9013
Log message:

      For rules that already have an nth_hyp annotation, the elim annotation is
      unnecessary.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 19:07:02 -0700 (Mon, 03 Apr 2006)
Revision: 9014
Log message:

      Wrote another elimination tactic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 20:31:54 -0700 (Mon, 03 Apr 2006)
Revision: 9015
Log message:

      Working on elimination tactics, made some progress.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 20:58:47 -0700 (Mon, 03 Apr 2006)
Revision: 9016
Log message:

      I finally figured out why I was getting these weird linking errors with
      reflect_ theories! The problem is that since there is no .mli (only .ppi),
      then compiling the .ppo would _both_ produce the .cmx _and_ overwrite the
      .cmi! So anything compiled against the old .cmi (the one created out of .ppi)
      will become stale!
      
      To fix it, I've added "-intf-suffix .ppi" to appropriate reflection rules.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 21:00:37 -0700 (Mon, 03 Apr 2006)
Revision: 9017
Log message:

      More progress with the elimination tactic.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-03 21:29:34 -0700 (Mon, 03 Apr 2006)
Revision: 9018
Log message:

      Fixed the forwardChainT bug that Xin found.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-04 01:16:33 -0700 (Tue, 04 Apr 2006)
Revision: 9019
Log message:

      Added a proper implementation of the forwardT tactic that only brings in
      forward-chaining information for one hyp and does not chain. (Jason had this
      in his implementation, but my reimplementation was missing it until now and
      Xin's proofs need it).
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-04 14:34:53 -0700 (Tue, 04 Apr 2006)
Revision: 9020
Log message:

      Updated the proof with Aleksey's improved forwardT implementation.
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-04-04 20:29:10 -0700 (Tue, 04 Apr 2006)
Revision: 9021
Log message:

      Some progress on sequent normalization.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-04 23:39:42 -0700 (Tue, 04 Apr 2006)
Revision: 9022
Log message:

      Mostly proved subtyping is reflexive (Reflect_pmn_core_logic_test.intro_rule_test_ref); there are only a few well-formedness subgoals left unproven:
      
      /reflect_pmn_core_logic_test/intro_rule_test_ref/1/1/1/1/1/5
      /reflect_pmn_core_logic_test/intro_rule_test_ref/1/1/1/1/1/12
      /reflect_pmn_core_logic_test/intro_rule_test_ref/1/1/1/1/1/2/6/1
      /reflect_pmn_core_logic_test/intro_rule_test_ref/1/1/1/1/1/2/7/1
      
      -- They look hard to prove to me. Please take a look!
      
      

Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2006-04-05 08:12:37 -0700 (Wed, 05 Apr 2006)
Revision: 9023
Log message:

      Display forms added, I also use reduce-resource as unfold-resource. It is ok for S4LP since it does not have a notion of computation.

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-05 14:18:03 -0700 (Wed, 05 Apr 2006)
Revision: 9024
Log message:

      More progress on elimination tactics. They are now mostly complete, except for
      the "big step elimination" rule, where we get the following unproved subgoals:
      
      - A few wf subgoals for the "bindn {..sequent_bterm{0}}" in
        pnm_core_judgments. Hopefully they will go away at the same time we fix them
        for the intro rules.
      
      - The subgoals corresponding to the "subtheory" cases. Currently the
        assumptions we generate for subtheories in these "big step elimination"
        rules are simply incorrect and we need to figure out what to do about it. It
        seems that the best thing to do would be to fully expalnd the subtheories
        (so that we get cases for all the rules, including the ones from
        subtheories), but this approach might have its own downsides.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-05 18:07:32 -0700 (Wed, 05 Apr 2006)
Revision: 9025
Log message:

      Minor optimization.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-05 18:08:13 -0700 (Wed, 05 Apr 2006)
Revision: 9026
Log message:

      Changed the forward rule for sequent_bterm. It is now more general.
      Also modified "sequent_bterm_depth" to make it more general.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-05 20:53:49 -0700 (Wed, 05 Apr 2006)
Revision: 9027
Log message:

      Added sequent_bterm_depth back to the reduce resource.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-05 23:18:36 -0700 (Wed, 05 Apr 2006)
Revision: 9028
Log message:

      "bind_in_bind_ge" shouldn't be in the intro resource: if the term has the form bind{n; y. bind{n2; z. e[y; z]}}, then 'n can be smaller than 'm.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-05 23:58:11 -0700 (Wed, 05 Apr 2006)
Revision: 9029
Log message:

      Added support for "vsequent{...} in SequentRelax"; updated the proof in Reflect_pmn_core_logic_test.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-06 12:24:05 -0700 (Thu, 06 Apr 2006)
Revision: 9030
Log message:

      Recommit this file.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-06 13:55:50 -0700 (Thu, 06 Apr 2006)
Revision: 9031
Log message:

      Updated the proof for "Pmn_core_terms_test.tyExp_left"
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-06 14:13:30 -0700 (Thu, 06 Apr 2006)
Revision: 9032
Log message:

      When we have a hyp of the form t=number[n] in (int|nat), dT should try
      performing the substitution.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-06 15:51:24 -0700 (Thu, 06 Apr 2006)
Revision: 9033
Log message:

      This one should work. I re-did all the proof and regenerated the file.
      

Changes by: Xin Yu (xiny at cs.caltech.edu)
Date: 2006-04-07 00:12:14 -0700 (Fri, 07 Apr 2006)
Revision: 9036
Log message:

      Use forwardChainT to make the proofs much easier.
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-07 16:30:18 -0700 (Fri, 07 Apr 2006)
Revision: 9037
Log message:

      Prohibit JProver in the automatic reflection proofs (we do not need it and it
      is taking _way_ too long to fail).
      

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2006-04-10 19:52:51 -0700 (Mon, 10 Apr 2006)
Revision: 9047
Log message:

      Require OMake 0.9.6.9
      

Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2006-04-17 10:09:12 -0700 (Mon, 17 Apr 2006)
Revision: 9092
Log message:

      Updated the magic number to match changes in libmojave.