Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-02 13:36:04 -0700 (Wed, 02 Jul 2008)
Revision: 13092
Log message:

      working on phases 1 and 2

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-03 14:02:11 -0700 (Thu, 03 Jul 2008)
Revision: 13095
Log message:

      added box-to-right rule to phase 1
     next step - rework families support, because now it is fake - bases cases are not covered, families joining is not implemented

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-04 11:22:52 -0700 (Fri, 04 Jul 2008)
Revision: 13096
Log message:

      first draft of phase 1 finished

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-05 12:54:57 -0700 (Sat, 05 Jul 2008)
Revision: 13097
Log message:

      all phases finished in first draft, it compiles but never executed yet
     -This line, and those below, will be ignored--
     
     M    s4lp/hilbert_internal.mli
     M    s4lp/hilbert_internal.ml

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-08 18:07:04 -0700 (Tue, 08 Jul 2008)
Revision: 13100
Log message:

      compiles, runs and even checks up for self-referencial example.
     we still have to check more carefully because proof term and proof are kind of long (see the end of the file)

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-09 19:32:09 -0700 (Wed, 09 Jul 2008)
Revision: 13105
Log message:

      Changed the families handling code because merging of families was incorrectly implemented. It used to be amp from representatives to the whole family, but if you think even a bit, you'll realize that it can't work. Now it's a set (list) of sets (families), not very efficient but can be replaced with an ordered set with a natural(lexicographical) order on families.
     
     We forgot to replace every provisional from a principal family with the summ of all essential terms - we did it only for BoxRight rule, have to do it uniformly.

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-10 12:50:31 -0700 (Thu, 10 Jul 2008)
Revision: 13106
Log message:

      More progress on camlp4.  I wish they would document the quotation syntax somewhere!
     AFAIK, it is undocumented, and different from the old syntax too.

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-10 13:33:51 -0700 (Thu, 10 Jul 2008)
Revision: 13107
Log message:

      added phase1-2 substitution between families computation (assign) and realization per se (g2h)
     the substitution after g2h serves a different purpose - it replaces principla provisionals with terms evaluated in g2h

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-10 16:40:53 -0700 (Thu, 10 Jul 2008)
Revision: 13109
Log message:

      More progress in filter_ocaml, still a ways to go.

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-10 19:30:08 -0700 (Thu, 10 Jul 2008)
Revision: 13110
Log message:

      Added some code that extracts and prints all formulas that were claimed tautologies (and left unproven) in the proof.
     Most of these formulas are propositional tautologies and we can check them with JProver (if we like).
     Two other types of tautologies are:
     1. (A,t:A -> C) -> (t:A -> C)
     2. (A->t:B) -> (A->(t1+..+t+..tn):B)
     and variations of these forms (with side formulas from Gentzen-style rules)
     We have to discuss it with SNA, if we want to prove them explicitely or not, anyway it's a minor issue.

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-10 20:33:34 -0700 (Thu, 10 Jul 2008)
Revision: 13111
Log message:

      Ported patterns.

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-11 12:36:05 -0700 (Fri, 11 Jul 2008)
Revision: 13112
Log message:

      Halfway through types, lots of work to do.

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-11 14:44:10 -0700 (Fri, 11 Jul 2008)
Revision: 13113
Log message:

      Updated sig_item.

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-11 14:52:11 -0700 (Fri, 11 Jul 2008)
Revision: 13114
Log message:

      Part way through str_item

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-13 12:38:23 -0700 (Sun, 13 Jul 2008)
Revision: 13115
Log message:

      added connection with JProver.
     Now one can feed a statement for JProver to prove and then realize it in LP.
     
     ToDo:
     1.Currently only implicational fragment + NegLeft rule are implemented;
     NegRight and And/Or rules have to be added
     2.Multi-agent system is not supported though datatypes are already multi-modal and some code is but it is not complete

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-13 15:09:55 -0700 (Sun, 13 Jul 2008)
Revision: 13116
Log message:

      a tiny simplification

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-14 14:29:25 -0700 (Mon, 14 Jul 2008)
Revision: 13118
Log message:

      filter_ocaml.ml now almost compiles.  Except, the compiler keeps complaining that
     "this expression is not allowed on the rhs ot a let rec".  Not sure what is causing this...

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-14 14:45:32 -0700 (Mon, 14 Jul 2008)
Revision: 13119
Log message:

      Hoist some definitions out of the big recursive definition, and it compiles.

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-14 15:28:54 -0700 (Mon, 14 Jul 2008)
Revision: 13120
Log message:

      Filter compiles and runs, but we get this:
     
     Failure:
         No interface printer

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-14 17:42:47 -0700 (Mon, 14 Jul 2008)
Revision: 13121
Log message:

      eliminated explicit references to axiom indices and arithmetic over them (where necessitation was needed)

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-14 19:07:58 -0700 (Mon, 14 Jul 2008)
Revision: 13122
Log message:

      Added Nec rule, in its generic (not restricted to axioms) form.
     As a result, deduction theorem has to consider two cases - hyps-free and non-hyp-free but for an axiom. May, be it would be more straightforward to use axiom-nly Nec.
     But for now we follow Artemov's TCS paper.

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-14 19:13:19 -0700 (Mon, 14 Jul 2008)
Revision: 13123
Log message:

      New Campl4 uses an undocumented scheme for the printers, that I
     think is supposed to implement dynamic binding.  I can't figure it
     out, so just set the printer references manually.
     
     Tracking down the next problem, "illegal begin of interf".

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-14 20:56:30 -0700 (Mon, 14 Jul 2008)
Revision: 13124
Log message:

      more progress towards multi-modal case

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-15 19:17:14 -0700 (Tue, 15 Jul 2008)
Revision: 13125
Log message:

      Finally, all the basic stuff is port to Camlp4 3.10.
     
     However, I didn't bother to be careful in keep the new term format
     compatible.  The AST has changed so much, it seems almost impossible
     to do that.
     
     That means that the .prla file are filled with terms in the old format
     that cause errors.  Basically, we just need to ignore the errors.

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-15 22:05:36 -0700 (Tue, 15 Jul 2008)
Revision: 13126
Log message:

      Added AndRight rule and it exposed an error g2h code for BoxRight (lemma3 was implemented incorrectly and worked only for one hypothesis).
     fixed

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-16 08:54:44 -0700 (Wed, 16 Jul 2008)
Revision: 13127
Log message:

      added AndLeft

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-16 08:55:43 -0700 (Wed, 16 Jul 2008)
Revision: 13128
Log message:

      forgot to add these files a couple of days ago

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-16 09:26:50 -0700 (Wed, 16 Jul 2008)
Revision: 13129
Log message:

      added OrLeft

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-16 09:55:23 -0700 (Wed, 16 Jul 2008)
Revision: 13130
Log message:

      OrRight added

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-16 13:09:41 -0700 (Wed, 16 Jul 2008)
Revision: 13131
Log message:

      _Almost_ compiles with 3.10.  Term errors during .prla parsing are warnings only.
     
     I don't know how we did the backslash-opnames, like \subtype, but for now it is
     turned off.  You have to write "subtype".
     
     Note, the sequence [< is a single token.  A quotation needs a space around it.
     
        [<< 'A + 'B >>]    (* Incorrect *)
        [ << 'A + 'B >>]   (* Correct *)

Changes by: Yegor Bryukhov (ybryukhov at gmail.com)
Date: 2008-07-16 14:09:40 -0700 (Wed, 16 Jul 2008)
Revision: 13132
Log message:

      added NegRight.
     todo: finish multi-modal support.

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-16 14:41:09 -0700 (Wed, 16 Jul 2008)
Revision: 13134
Log message:

      Compiles with OCaml 3.10 (using omake 0.9.9).

Changes by: Jason J. Hickey (jyh at cs.caltech.edu)
Date: 2008-07-16 15:50:32 -0700 (Wed, 16 Jul 2008)
Revision: 13137
Log message:

      Fix all the theory files.