Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 00:48:25 -0700 (Fri, 01 Jul 2005)
Revision: 7522
Log message:
One more list converted to map
| Changes | Path |
| +30 -37 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 01:13:15 -0700 (Fri, 01 Jul 2005)
Revision: 7523
Log message:
another sets turned to map
| Changes | Path |
| +26 -24 | metaprl/refiner/reflib/jall.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-01 01:44:31 -0700 (Fri, 01 Jul 2005)
Revision: 7524
Log message:
More comment formatting. Now every toplevel "doc" item has an _implicit_
@begin[doc]...@end[doc] wrapper around it (except for "doc docoff") and
explicit @begin[doc]...@end[doc] and @doc{...} should no longer be used.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-01 01:53:25 -0700 (Fri, 01 Jul 2005)
Revision: 7525
Log message:
The MMC part of the previous commit
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 13:17:33 -0700 (Fri, 01 Jul 2005)
Revision: 7526
Log message:
one more list converted to set
| Changes | Path |
| +11 -4 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 13:39:48 -0700 (Fri, 01 Jul 2005)
Revision: 7527
Log message:
another set instead a list
| Changes | Path |
| +4 -6 | metaprl/refiner/reflib/jall.ml |
| +10 -10 | metaprl/refiner/reflib/jordering.ml |
| +10 -10 | metaprl/refiner/reflib/jtunify.ml |
| +3 -3 | metaprl/refiner/reflib/jtunify.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-01 15:46:17 -0700 (Fri, 01 Jul 2005)
Revision: 7528
Log message:
When reporting an interface <-> implementation mismatch, give the loc of the
mismatched item (in the _.mli_ file).
| Changes | Path |
| +41 -35 | metaprl/filter/base/filter_summary.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 16:20:23 -0700 (Fri, 01 Jul 2005)
Revision: 7529
Log message:
more lists converted to maps
| Changes | Path |
| +34 -30 | metaprl/refiner/reflib/jall.ml |
| +15 -19 | metaprl/refiner/reflib/jordering.ml |
| +3 -3 | metaprl/refiner/reflib/jtunify.ml |
| +6 -6 | metaprl/refiner/reflib/jtunify.mli |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 16:42:25 -0700 (Fri, 01 Jul 2005)
Revision: 7530
Log message:
one more set instead of list
| Changes | Path |
| +13 -8 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 17:31:58 -0700 (Fri, 01 Jul 2005)
Revision: 7531
Log message:
more sets
| Changes | Path |
| +34 -34 | metaprl/refiner/reflib/jall.ml |
| +9 -8 | metaprl/refiner/reflib/jordering.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 17:47:13 -0700 (Fri, 01 Jul 2005)
Revision: 7532
Log message:
and more sets
| Changes | Path |
| +15 -19 | metaprl/refiner/reflib/jall.ml |
| +3 -8 | metaprl/refiner/reflib/jordering.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 18:17:23 -0700 (Fri, 01 Jul 2005)
Revision: 7533
Log message:
more maps
| Changes | Path |
| +26 -12 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 18:34:26 -0700 (Fri, 01 Jul 2005)
Revision: 7534
Log message:
more sets
| Changes | Path |
| +6 -6 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 19:40:32 -0700 (Fri, 01 Jul 2005)
Revision: 7535
Log message:
started to store some substitutions in maps
| Changes | Path |
| +52 -64 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 20:02:28 -0700 (Fri, 01 Jul 2005)
Revision: 7536
Log message:
almost all substitutions are now maps
| Changes | Path |
| +22 -24 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-01 20:41:22 -0700 (Fri, 01 Jul 2005)
Revision: 7537
Log message:
removed an unused function
| Changes | Path |
| +0 -9 | metaprl/refiner/reflib/jall.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-07-02 07:02:24 -0700 (Sat, 02 Jul 2005)
Revision: 7538
Log message:
Update to match the recent changes to omake.
| Changes | Path |
| +3 -2 | metaprl/OMakefile |
| +1 -1 | metaprl/editor/ml/OMakefile |
| +0 -1 | metaprl/theories/itt/OMakefile |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-02 13:51:53 -0700 (Sat, 02 Jul 2005)
Revision: 7539
Log message:
instead of collecting a sublist and then testing if its empty, return boolean as you go over theoriginal.
| Changes | Path |
| +5 -5 | metaprl/refiner/reflib/jall.ml |
| +0 -0 | metaprl/refiner/reflib/jordering.ml |
Changes by: ( at unknown.email)
Date: 2005-07-02 13:51:53 -0700 (Sat, 02 Jul 2005)
Revision: 7540
Log message:
This commit was manufactured by cvs2svn to create branch 'S4-jprover'.
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-02 15:17:19 -0700 (Sat, 02 Jul 2005)
Revision: 7541
Log message:
minor optimization
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-02 15:31:58 -0700 (Sat, 02 Jul 2005)
Revision: 7542
Log message:
started to work on S4 part in jprover
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-02 19:53:00 -0700 (Sat, 02 Jul 2005)
Revision: 7543
Log message:
added support for multi-conclusion sequents but there's a lot of work for the other side of the interface
| Changes | Path |
| +58 -35 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 00:14:33 -0700 (Sun, 03 Jul 2005)
Revision: 7544
Log message:
it finally compiles
| Changes | Path |
| +30 -0 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 13:03:55 -0700 (Sun, 03 Jul 2005)
Revision: 7545
Log message:
Reformatting mainly: there were several deeply nested if-s, I made flat indentation.
| Changes | Path |
| +203 -210 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 14:18:21 -0700 (Sun, 03 Jul 2005)
Revision: 7546
Log message:
the ways negation and implication are converted to tree nodes are different for intiotionistic and classical/s4 logics
| Changes | Path |
| +218 -139 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 15:47:05 -0700 (Sun, 03 Jul 2005)
Revision: 7547
Log message:
cleaning other places that were tightly bound to J
| Changes | Path |
| +21 -5 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
| +12 -18 | metaprl-branches/S4-jprover/refiner/reflib/jtunify.ml |
| +5 -4 | metaprl-branches/S4-jprover/refiner/reflib/jtunify.mli |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 16:23:04 -0700 (Sun, 03 Jul 2005)
Revision: 7548
Log message:
Some time ago I unintentionally introduced a deviation from canonical algorithm
which amazingly didn't show up anywhere,
just in case, I'm returning it to its canonical form.
| Changes | Path |
| +5 -3 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 19:11:22 -0700 (Sun, 03 Jul 2005)
Revision: 7549
Log message:
more S4-related modifications
| Changes | Path |
| +91 -19 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 19:29:18 -0700 (Sun, 03 Jul 2005)
Revision: 7550
Log message:
same predicate was computed on every iteration, moved it outside
| Changes | Path |
| +17 -11 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 19:51:54 -0700 (Sun, 03 Jul 2005)
Revision: 7551
Log message:
moved computation of another predicate outside of recursive function
| Changes | Path |
| +28 -8 | metaprl-branches/S4-jprover/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 22:49:13 -0700 (Sun, 03 Jul 2005)
Revision: 7552
Log message:
Gentzen style S4 and its connection with Jprover
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-03 23:13:01 -0700 (Sun, 03 Jul 2005)
Revision: 7553
Log message:
my S4 does not have so I simplified its interface with Jprover
| Changes | Path |
| +16 -36 | metaprl-branches/S4-jprover/theories/s4lp/s4_logic.ml |
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 by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-04 18:33:07 -0700 (Mon, 04 Jul 2005)
Revision: 7555
Log message:
1. assumptions were incorrectly ordering in and_intro, fixed.
2. more examples, all working properly:
box(a & b) => box a & box b
box a & box b => box(a & b)
box(a => a)
box box(a => a)
box a or box b => box(a or b)
| Changes | Path |
| +17 -3 | metaprl-branches/S4-jprover/theories/s4lp/s4_logic.ml |
| +3746 -3549 | metaprl-branches/S4-jprover/theories/s4lp/s4_logic.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-04 18:41:32 -0700 (Mon, 04 Jul 2005)
Revision: 7556
Log message:
forgot .cvsignore
| Changes | Path |
| Properties | metaprl-branches/S4-jprover/theories/s4lp |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-04 18:58:35 -0700 (Mon, 04 Jul 2005)
Revision: 7557
Log message:
Merging S4-prover to the main trunk
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-05 13:03:57 -0700 (Tue, 05 Jul 2005)
Revision: 7558
Log message:
Added Nuprl_font!tensor; more dforms for Nuprl_font!circ.
| Changes | Path |
| +5 -0 | metaprl/support/display/nuprl_font.ml |
| +1 -0 | metaprl/support/display/nuprl_font.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-05 17:43:22 -0700 (Tue, 05 Jul 2005)
Revision: 7559
Log message:
If Jprover generates a subgoal with a conclusion that is identical to the
original one, report it as a "JProver failed to make progress" and abort.
| Changes | Path |
| +6 -1 | metaprl/theories/itt/itt_logic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-05 18:50:55 -0700 (Tue, 05 Jul 2005)
Revision: 7560
Log message:
**** WARNING: breaks binary compatibility! ****
This changes the string comparison in String{Set,Table,MTable} and
Lm_symbol.compare (which is also used in SymbolSet) to a slightly faster one
(compare the string lengths _first_, only compare individual characters when
strings have the same length). If you need the lexicographical order (which
was used before), use LexString{Set,Table,MTable} instead.
| Changes | Path |
| +4 -2 | metaprl/filter/base/filter_magic.ml |
| +4 -4 | metaprl/support/shell/shell_core.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-05 18:57:30 -0700 (Tue, 05 Jul 2005)
Revision: 7561
Log message:
removed the last place where string encoding was used
| Changes | Path |
| +5 -17 | metaprl/refiner/reflib/jall.ml |
| +1 -2 | metaprl/refiner/reflib/jtypes.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-05 22:05:33 -0700 (Tue, 05 Jul 2005)
Revision: 7562
Log message:
Forcing JProver to use atoms from conclusion first.
Now it can prove jprover_tests/barber (again).
| Changes | Path |
| +22 -11 | metaprl/refiner/reflib/jall.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-06 19:30:10 -0700 (Wed, 06 Jul 2005)
Revision: 7563
Log message:
This is a huge commit that is mostly no-op:
- Updated the standard preamble text to point to the correct location for the
documentation and to avoid mentioning Nuprl.
- Changed "Nuprl-Light" -> "MetaPRL" in a few places (amazingly, we still had
those).
- Split the Nuprl_font file into Mpfont and Mpsymbols.
- Protected a few display forms in ITT with a "doc docoff".
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-06 19:34:06 -0700 (Wed, 06 Jul 2005)
Revision: 7564
Log message:
More preamble changes
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-06 19:51:34 -0700 (Wed, 06 Jul 2005)
Revision: 7565
Log message:
Probably a non-working draft of lifting lemma and deduction theorem procedures
on abstract (non-MetaPRL) Hilbert proofs.
| Changes | Path |
| +1 -0 | metaprl/theories/s4lp/OMakefile |
| Added | metaprl/theories/s4lp/hilbert_internal.ml |
| Properties | metaprl/theories/s4lp/hilbert_internal.ml |
| Added | metaprl/theories/s4lp/hilbert_internal.mli |
| Properties | metaprl/theories/s4lp/hilbert_internal.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-06 20:15:53 -0700 (Wed, 06 Jul 2005)
Revision: 7566
Log message:
Added symbols: box, bigcirc.
| Changes | Path |
| +6 -0 | metaprl/support/display/mpsymbols.ml |
| +2 -0 | metaprl/support/display/mpsymbols.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-06 21:41:32 -0700 (Wed, 06 Jul 2005)
Revision: 7567
Log message:
Added Mpsymbols!multimap
| Changes | Path |
| +3 -0 | metaprl/support/display/mpsymbols.ml |
| +1 -0 | metaprl/support/display/mpsymbols.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-06 23:26:56 -0700 (Wed, 06 Jul 2005)
Revision: 7568
Log message:
Adding a preminimary implementation of the ILC basics in MetaPRL
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-07 09:24:25 -0700 (Thu, 07 Jul 2005)
Revision: 7569
Log message:
Minor display forms update
| Changes | Path |
| +1 -1 | metaprl/support/display/base_dform.mli |
| +7 -6 | metaprl/support/display/summary.ml |
| +2 -1 | metaprl/theories/ilc/ilc_core.ml |
| +1 -1 | metaprl/theories/ilc/ilc_core.mli |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-07-07 14:06:11 -0700 (Thu, 07 Jul 2005)
Revision: 7570
Log message:
Convert to using normal conditionals for metaprl.tex to get it to work
on FC4 (I don't know why it doesn't work there).
| Changes | Path |
| +95 -116 | metaprl/theories/ocaml_doc/ocaml_doc_mod1.ml |
| +9 -5 | texinputs/metaprl.tex |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-09 15:21:58 -0700 (Sat, 09 Jul 2005)
Revision: 7576
Log message:
Added an example that shows that LP-multiplicity has no counterpart in S4.
| Changes | Path |
| +2 -0 | metaprl/theories/s4lp/s4_logic.ml |
| +6685 -6647 | metaprl/theories/s4lp/s4_logic.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-11 00:25:47 -0700 (Mon, 11 Jul 2005)
Revision: 7577
Log message:
Groundwork for multi-modal S4.
At this moment S4 is actualy broken, but at least ITT is not :)
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-11 15:56:18 -0700 (Mon, 11 Jul 2005)
Revision: 7578
Log message:
Yesterday I added two new position kinds indexed by integers to support multiple modalities.
I decided to merge them with old Var, NewVar and Const kinds to keep number of cases
in matches under control.
Non-modal uses of those kinds use index 0.
For modal cases 0 means J-modality which implies all other modalities.
| Changes | Path |
| +6 -6 | metaprl/refiner/reflib/jall.ml |
| +47 -60 | metaprl/refiner/reflib/jordering.ml |
| +20 -8 | metaprl/refiner/reflib/jtunify.ml |
| +3 -5 | metaprl/refiner/reflib/jtypes.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-11 17:21:59 -0700 (Mon, 11 Jul 2005)
Revision: 7579
Log message:
Better error messages when trying to turn something weird into a variable.
| Changes | Path |
| +10 -7 | metaprl/refiner/rewrite/rewrite_build_contractum.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-11 18:11:31 -0700 (Mon, 11 Jul 2005)
Revision: 7580
Log message:
S4 is working again.
Now I have to test multi-modal behavior.
I also added S4LP to the "theories=all" list
| Changes | Path |
| +1 -1 | metaprl/mk/defaults |
| +23 -6 | metaprl/refiner/reflib/jtunify.ml |
| +8 -6 | metaprl/theories/s4lp/s4_logic.ml |
| +8873 -8706 | metaprl/theories/s4lp/s4_logic.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-11 18:40:04 -0700 (Mon, 11 Jul 2005)
Revision: 7581
Log message:
Some minor fixes.
Wise men added but they don't work for some reason.
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-11 18:55:53 -0700 (Mon, 11 Jul 2005)
Revision: 7582
Log message:
Apparently the prefix unification algorithm is incorrect,
I'll see what can be done about it.
| Changes | Path |
| +11 -2 | metaprl/refiner/reflib/jordering.ml |
| +7 -0 | metaprl/theories/s4lp/s4_tests.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-11 23:15:11 -0700 (Mon, 11 Jul 2005)
Revision: 7583
Log message:
Now I have problem with recosntruction of the correct ordering of inferences.
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-12 14:46:19 -0700 (Tue, 12 Jul 2005)
Revision: 7584
Log message:
Committing Limin's current version of the ILC theory (with a few minor
cosmetical changes).
| Changes | Path |
| Properties | metaprl/theories/ilc |
| +62 -0 | metaprl/theories/ilc/ilc_core.ml |
| +3 -0 | metaprl/theories/ilc/ilc_core.mli |
| +1 -1 | metaprl/theories/itt/itt_logic.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-12 14:51:33 -0700 (Tue, 12 Jul 2005)
Revision: 7585
Log message:
Updating CVS instructions with the latest information.
| Changes | Path |
| +4 -5 | metaprl/doc/htmlman/mp-cvs-rw.html |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-12 15:11:45 -0700 (Tue, 12 Jul 2005)
Revision: 7586
Log message:
Some fixes in the unification algorithm - it is (still) too agressive in
unifying incompatible modalities.
| Changes | Path |
| +23 -7 | metaprl/refiner/reflib/jtunify.ml |
| +6 -1 | metaprl/theories/s4lp/s4_tests.ml |
| +1 -0 | metaprl/theories/s4lp/s4_tests.mli |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-12 15:54:07 -0700 (Tue, 12 Jul 2005)
Revision: 7587
Log message:
- Added the impl_intro to the intro resource
- Added an "axiom" rule.
| Changes | Path |
| +5 -3 | metaprl/theories/ilc/ilc_core.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-12 15:56:53 -0700 (Tue, 12 Jul 2005)
Revision: 7588
Log message:
a little 'better' unification
| Changes | Path |
| +24 -19 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-12 17:02:30 -0700 (Tue, 12 Jul 2005)
Revision: 7589
Log message:
Do not atempt to use ITT-JProver on non-ITT sequents.
| Changes | Path |
| +1 -0 | metaprl/theories/itt/itt_equal.ml |
| +1 -0 | metaprl/theories/itt/itt_equal.mli |
| +6 -4 | metaprl/theories/itt/itt_logic.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-12 18:28:34 -0700 (Tue, 12 Jul 2005)
Revision: 7590
Log message:
To make life easier added integer index to NewVarQ as well
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jall.ml |
| +15 -14 | metaprl/refiner/reflib/jordering.ml |
| +13 -17 | metaprl/refiner/reflib/jtunify.ml |
| +1 -1 | metaprl/refiner/reflib/jtypes.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-12 18:33:41 -0700 (Tue, 12 Jul 2005)
Revision: 7591
Log message:
added 2 more tests
| Changes | Path |
| +4 -0 | metaprl/theories/s4lp/s4_tests.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-12 19:06:45 -0700 (Tue, 12 Jul 2005)
Revision: 7592
Log message:
simplified multimodal compatibility conditions
| Changes | Path |
| +42 -51 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-12 22:02:37 -0700 (Tue, 12 Jul 2005)
Revision: 7593
Log message:
Minor code simplification
| Changes | Path |
| +7 -21 | metaprl/refiner/reflib/jall.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-12 22:22:51 -0700 (Tue, 12 Jul 2005)
Revision: 7594
Log message:
A few more minor code simplifications
| Changes | Path |
| +2 -4 | metaprl/refiner/reflib/jall.ml |
| +7 -35 | metaprl/refiner/reflib/jordering.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-13 06:57:12 -0700 (Wed, 13 Jul 2005)
Revision: 7595
Log message:
Use opname instead of operator as a "predicate" identifier in JProver. Opname
is a coarser approximation than the more precise operator, but handling
opnames is more efficient and works correctly in presence of nested sequents.
| Changes | Path |
| +15 -15 | metaprl/refiner/reflib/jall.ml |
| +1 -1 | metaprl/refiner/reflib/jtypes.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-13 07:39:00 -0700 (Wed, 13 Jul 2005)
Revision: 7596
Log message:
Getting rid of the "multiple ways to build scanner <scanner
theories/itt/scan-ocaml-gen_int_bench.ml>" warning.
| Changes | Path |
| +1 -2 | metaprl/theories/itt/OMakefile |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-13 07:47:19 -0700 (Wed, 13 Jul 2005)
Revision: 7597
Log message:
Implemented "omake FORCE_REALCLEAN=1 realclean" allowing for a forced
"realclean".
| Changes | Path |
| +4 -1 | metaprl/OMakefile |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-13 13:07:01 -0700 (Wed, 13 Jul 2005)
Revision: 7598
Log message:
A pair of an item and a list was returned as a list, changed it to a real pair.
| Changes | Path |
| +36 -26 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-13 15:59:52 -0700 (Wed, 13 Jul 2005)
Revision: 7599
Log message:
more tests
| Changes | Path |
| +2 -0 | metaprl/theories/s4lp/s4_tests.ml |
| +382 -195 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-13 20:12:35 -0700 (Wed, 13 Jul 2005)
Revision: 7601
Log message:
from now on positions are compared by their indices only
| Changes | Path |
| +3 -5 | metaprl/refiner/reflib/jordering.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-13 20:32:55 -0700 (Wed, 13 Jul 2005)
Revision: 7602
Log message:
replaced several =-comparisons of positions with defined comparison
| Changes | Path |
| +4 -7 | metaprl/refiner/reflib/jall.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-14 15:18:41 -0700 (Thu, 14 Jul 2005)
Revision: 7603
Log message:
Added an ad-hoc profiling mechanism.
| Changes | Path |
| +1 -0 | metaprl/editor/ml/mp_top.ml |
| +0 -1 | metaprl/editor/ml/shell_mp.ml |
| +2 -0 | metaprl/filter/filter/filter_main.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-14 16:13:02 -0700 (Thu, 14 Jul 2005)
Revision: 7604
Log message:
Setenv MP_DEBUG earier to make sure all the .SUBDIRS directives are in scope.
| Changes | Path |
| +4 -4 | metaprl/OMakefile |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-14 16:45:28 -0700 (Thu, 14 Jul 2005)
Revision: 7605
Log message:
two more (=) replaced with position_eq
| Changes | Path |
| +2 -2 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-14 17:01:34 -0700 (Thu, 14 Jul 2005)
Revision: 7606
Log message:
more (=) replaced with position_eq
| Changes | Path |
| +2 -2 | metaprl/refiner/reflib/jall.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-14 17:30:24 -0700 (Thu, 14 Jul 2005)
Revision: 7607
Log message:
When the same debug flag is created several times, make sure debug_description
match.
| Changes | Path |
| +1 -1 | metaprl/filter/base/filter_grammar.ml |
| +0 -6 | metaprl/filter/filter/filter_parse.ml |
| +2 -2 | metaprl/filter/filter/term_grammar.ml |
| +2 -12 | metaprl/theories/itt/itt_omega.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-14 18:00:43 -0700 (Thu, 14 Jul 2005)
Revision: 7608
Log message:
Added code for ad-hoc profiling of top-level tactics. The profiling is
controlled by the "profile_tactics" debug variable.
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-14 18:35:45 -0700 (Thu, 14 Jul 2005)
Revision: 7609
Log message:
more position_eq instead of =, one place needs = because index 0 is not globally unique
| Changes | Path |
| +17 -14 | metaprl/refiner/reflib/jall.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-14 19:22:46 -0700 (Thu, 14 Jul 2005)
Revision: 7610
Log message:
The record_reduceT tactic had rwh on top of higherC, fixing.
| Changes | Path |
| +1 -1 | metaprl/theories/itt/itt_record.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-14 20:48:22 -0700 (Thu, 14 Jul 2005)
Revision: 7611
Log message:
Added rewrite profiling to tactic_profile.
| Changes | Path |
| +7 -3 | metaprl/tactics/proof/rewrite_boot.ml |
Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2005-07-15 11:50:45 -0700 (Fri, 15 Jul 2005)
Revision: 7613
Log message:
Minor optimization.
| Changes | Path |
| +2 -4 | metaprl/tactics/proof/rewrite_boot.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-15 13:28:42 -0700 (Fri, 15 Jul 2005)
Revision: 7614
Log message:
one more test
| Changes | Path |
| +2 -0 | metaprl/theories/s4lp/s4_tests.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-15 13:41:22 -0700 (Fri, 15 Jul 2005)
Revision: 7616
Log message:
replaced generic jprover_bug exception with more specific ones refering to a particular function where a problem happened
| Changes | Path |
| +39 -36 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-15 16:25:29 -0700 (Fri, 15 Jul 2005)
Revision: 7617
Log message:
finally it is smart enough to apply rules in the right order while proving
K1 K2 p => K1 K2 K2 p
| Changes | Path |
| +46 -33 | metaprl/refiner/reflib/jall.ml |
| +276 -232 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-15 16:34:25 -0700 (Fri, 15 Jul 2005)
Revision: 7618
Log message:
!!! Wise men puzzle proved !!!
(by prover, not by me)
| Changes | Path |
| +132 -71 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-15 18:27:05 -0700 (Fri, 15 Jul 2005)
Revision: 7619
Log message:
muddy children are also partially working but the problem here seems to be in performance
| Changes | Path |
| +2 -0 | metaprl/refiner/reflib/jall.ml |
| +37 -0 | metaprl/theories/s4lp/s4_tests.ml |
| +1 -0 | metaprl/theories/s4lp/s4_tests.mli |
| +732 -43 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-15 18:27:53 -0700 (Fri, 15 Jul 2005)
Revision: 7620
Log message:
forgot to remove a couple of debug messages
| Changes | Path |
| +2 -2 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-16 16:27:24 -0700 (Sat, 16 Jul 2005)
Revision: 7621
Log message:
2 and 3 muddy children problems are solved.
3 children problem takes 120 seconds on mojave3 !!!
4 children seems to be way too hard for current path-searching algorithm because
of its unintelligent use of multiplicities.
Currently I keep a pair of debug messages on (in S4 only).
| Changes | Path |
| +4 -2 | metaprl/refiner/reflib/jall.ml |
| +84 -21 | metaprl/theories/s4lp/s4_tests.ml |
| +2 -0 | metaprl/theories/s4lp/s4_tests.mli |
| +1952 -570 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-16 18:46:48 -0700 (Sat, 16 Jul 2005)
Revision: 7622
Log message:
I changed a theorem statement and its proof became "infinite", this commit removes the proof.
| Changes | Path |
| +1 -1 | metaprl/theories/s4lp/s4_tests.ml |
| +346 -358 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-16 19:01:50 -0700 (Sat, 16 Jul 2005)
Revision: 7624
Log message:
replaced a list with a map
| Changes | Path |
| +14 -12 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-16 19:14:43 -0700 (Sat, 16 Jul 2005)
Revision: 7625
Log message:
removed an unused parameter in a group of functions
| Changes | Path |
| +12 -12 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-16 19:16:31 -0700 (Sat, 16 Jul 2005)
Revision: 7626
Log message:
replaced a custom function with Set.filter
| Changes | Path |
| +3 -10 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-16 19:37:10 -0700 (Sat, 16 Jul 2005)
Revision: 7627
Log message:
several renamings and one custom functions replaced with List.fold_left
| Changes | Path |
| +11 -8 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-16 20:56:22 -0700 (Sat, 16 Jul 2005)
Revision: 7628
Log message:
more on conversion lists to maps
| Changes | Path |
| +34 -32 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-16 21:45:51 -0700 (Sat, 16 Jul 2005)
Revision: 7631
Log message:
more list converted to maps
| Changes | Path |
| +26 -27 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-17 17:10:57 -0700 (Sun, 17 Jul 2005)
Revision: 7635
Log message:
replaced a couple of (=) with position_eq and made one function tail-recursive
| Changes | Path |
| +0 -2 | metaprl/refiner/reflib/jall.ml |
| +2 -0 | metaprl/refiner/reflib/jordering.ml |
| +12 -15 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-18 19:56:26 -0700 (Mon, 18 Jul 2005)
Revision: 7639
Log message:
Until now, before calling unify_mm jprover used to apply previously found
substitutions to the current pair of terms.
As far as I understand, it could be very expensive potentially.
So now it uses substitution as an additional set of equations.
I failed to use unify_mm's type eqnlist to store intermediate solutions
from iteration to iteration because I still need substitutions out of it.
It seems that getting substituion directly from unify and getting eqnlist with
manual convertion to a substitution produce different results :(
| Changes | Path |
| +51 -48 | metaprl/refiner/reflib/jall.ml |
| +6 -4 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-18 22:57:38 -0700 (Mon, 18 Jul 2005)
Revision: 7640
Log message:
Jprover used to replace original free variables with ground terms
and then restore them at the end.
I'm working on eliminating such behavior.
There is a potential for clashes between metaprl and jprover variables
but I haven't seen any yet. And there is always a treatment against
clashes - Lm_symbol.new_number though it might make jprover a bit slower.
| Changes | Path |
| +23 -30 | metaprl/refiner/reflib/jall.ml |
| +0 -1 | metaprl/refiner/reflib/jtypes.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-19 02:40:02 -0700 (Tue, 19 Jul 2005)
Revision: 7641
Log message:
Use Lm_symbol.new_number for unique indices instead of local counter.
This is in order to avoid clashes between jprover-vars and original vars in terms.
| Changes | Path |
| +84 -101 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-19 02:57:27 -0700 (Tue, 19 Jul 2005)
Revision: 7642
Log message:
Second and the last local counter replaced with Lm_symbol.new_number
| Changes | Path |
| +1 -4 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-19 19:35:36 -0700 (Tue, 19 Jul 2005)
Revision: 7643
Log message:
There is one more counter for unique indices, with this commit it is localized
in jtunify
| Changes | Path |
| +20 -21 | metaprl/refiner/reflib/jall.ml |
| +3 -8 | metaprl/refiner/reflib/jtunify.ml |
| +7 -10 | metaprl/refiner/reflib/jtunify.mli |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-20 15:28:18 -0700 (Wed, 20 Jul 2005)
Revision: 7644
Log message:
1.Made one exception more verbose
2.Fixed a typo
| Changes | Path |
| +4 -2 | metaprl/theories/itt/itt_logic.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-20 15:33:59 -0700 (Wed, 20 Jul 2005)
Revision: 7645
Log message:
Until now Jprover used to replace all originally free variables with ground terms
and than recover tham at the final stage.
It also used to inject its own ground terms which are actually variables in certain sense.
Aleksey complained about its interaction with nested sequents.
All this is now gone, jprover injects no ground terms, all of them are now variables.
The only side effect which you might not like is that I use Lm_symbol.new_number
and during check-status this index goes beyond 900000 (may be even above a million),
I don't know if it is ever exposed to a user. If this happens I can return to
usage of local counters though it might complicate the code a bit.
| Changes | Path |
| +95 -96 | metaprl/refiner/reflib/jall.ml |
| +33 -13 | metaprl/refiner/reflib/jordering.ml |
| +0 -11 | metaprl/refiner/reflib/jtunify.ml |
| +1 -2 | metaprl/refiner/reflib/jtypes.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-20 15:37:21 -0700 (Wed, 20 Jul 2005)
Revision: 7646
Log message:
Fixing a typo
| Changes | Path |
| +1 -1 | metaprl/theories/itt/itt_logic.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-20 15:50:43 -0700 (Wed, 20 Jul 2005)
Revision: 7647
Log message:
turned a group of functions into tail-recursive form
| Changes | Path |
| +7 -9 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-20 16:24:49 -0700 (Wed, 20 Jul 2005)
Revision: 7648
Log message:
a bunch of minor optimizations
| Changes | Path |
| +24 -45 | metaprl/refiner/reflib/jall.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-20 16:41:01 -0700 (Wed, 20 Jul 2005)
Revision: 7649
Log message:
replaced a couple of (=) with position_eq
| Changes | Path |
| +3 -5 | metaprl/refiner/reflib/jall.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-07-21 09:33:49 -0700 (Thu, 21 Jul 2005)
Revision: 7650
Log message:
Totally revising the file chapter.
| Changes | Path |
| +222 -198 | metaprl/theories/ocaml_doc/ocaml_doc_mod1.ml |
Changes by: ( at unknown.email)
Date: 2005-07-21 09:33:49 -0700 (Thu, 21 Jul 2005)
Revision: 7651
Log message:
This commit was manufactured by cvs2svn to create branch
'jprover-rule-based-unif'.
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 11:09:16 -0700 (Thu, 21 Jul 2005)
Revision: 7652
Log message:
I started to work on rule-based prefix unification in jprover.
The potential benefits:
1.It's easier to adapt to other logics
2.One of possible resolutions for contination problem
Right now it's pretty naive and check-status is 50secs slower but
s4_tests/mch3 which used to run for 120 secs runs for 80 secs now.
I think the latter speed up is due to tail-recursive code of this new
implementation.
| Changes | Path |
| +159 -150 | metaprl-branches/jprover-rule-based-unif/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 11:44:12 -0700 (Thu, 21 Jul 2005)
Revision: 7653
Log message:
Made the rules' map more intelligent - after a rule found applicable use a predefined
list of rules to try next (not all of the remaining rules).
| Changes | Path |
| +19 -17 | metaprl-branches/jprover-rule-based-unif/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 12:02:40 -0700 (Thu, 21 Jul 2005)
Revision: 7654
Log message:
a slight tune up
| Changes | Path |
| +1 -1 | metaprl-branches/jprover-rule-based-unif/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 12:55:38 -0700 (Thu, 21 Jul 2005)
Revision: 7655
Log message:
one rule was not applicable after another, so I removed it.
| Changes | Path |
| +1 -4 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 13:06:28 -0700 (Thu, 21 Jul 2005)
Revision: 7656
Log message:
minor optimizations
| Changes | Path |
| +117 -91 | metaprl-branches/jprover-rule-based-unif/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 13:45:20 -0700 (Thu, 21 Jul 2005)
Revision: 7657
Log message:
I don't understand why rev_append worked in this place, rolling back to append
| Changes | Path |
| +1 -1 | metaprl-branches/jprover-rule-based-unif/refiner/reflib/jtunify.ml |
Changes by: Jason Hickey (jyh at cs.caltech.edu)
Date: 2005-07-21 14:14:55 -0700 (Thu, 21 Jul 2005)
Revision: 7658
Log message:
Modified the chapter on files.
| Changes | Path |
| +0 -3 | metaprl/mllib/comment_parse.mll |
| +521 -532 | metaprl/theories/ocaml_doc/ocaml_doc_mod1.ml |
| +36 -0 | metaprl/theories/ocaml_doc/ocaml_doc_mod2.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 15:13:34 -0700 (Thu, 21 Jul 2005)
Revision: 7659
Log message:
preparations for continuation support
| Changes | Path |
| +31 -64 | metaprl-branches/jprover-rule-based-unif/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 17:41:41 -0700 (Thu, 21 Jul 2005)
Revision: 7660
Log message:
The infrastructure for continuation in prefix unification is ready.
Even the time of check-status is almost back to normal.
| Changes | Path |
| +78 -76 | metaprl-branches/jprover-rule-based-unif/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 18:46:34 -0700 (Thu, 21 Jul 2005)
Revision: 7661
Log message:
Replaced an append with rev_append
| Changes | Path |
| +2 -7 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-21 20:15:06 -0700 (Thu, 21 Jul 2005)
Revision: 7662
Log message:
another (=) replaced with position_eq
| Changes | Path |
| +1 -1 | metaprl/refiner/reflib/jtunify.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-22 11:44:28 -0700 (Fri, 22 Jul 2005)
Revision: 7663
Log message:
It's amazing, continuation worked well from the first try without any debugging!
check-status time is down by 100secs;
muddy children problem dropped from 120 secs to 40 secs
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-22 12:08:14 -0700 (Fri, 22 Jul 2005)
Revision: 7664
Log message:
Merging continuation code into the main trunk
| Changes | Path |
| +29 -37 | metaprl/refiner/reflib/jall.ml |
| +252 -214 | metaprl/refiner/reflib/jtunify.ml |
| +12 -2 | metaprl/refiner/reflib/jtunify.mli |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-22 12:24:36 -0700 (Fri, 22 Jul 2005)
Revision: 7665
Log message:
With the new unification algorithm muddy children problem for 4 children
is proved in 30 seconds vs "infinite" time before (it worked for hours and didn't terminate).
| Changes | Path |
| +164 -177 | metaprl/theories/s4lp/s4_tests.prla |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-28 17:03:08 -0700 (Thu, 28 Jul 2005)
Revision: 7666
Log message:
S4-to-LP realization compiles but definitely does not work yet.
(that's for implicative fragment only)
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-28 17:47:03 -0700 (Thu, 28 Jul 2005)
Revision: 7667
Log message:
Sounds funny, but I missed the stage when non-essential boxes are actually converted to proof terms.
| Changes | Path |
| +28 -20 | metaprl/theories/s4lp/s4_internal.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-28 18:15:46 -0700 (Thu, 28 Jul 2005)
Revision: 7668
Log message:
Now box should be timely converted to proof terms, it's time to see how the whole thing works.
| Changes | Path |
| +47 -30 | metaprl/theories/s4lp/s4_internal.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-29 14:26:39 -0700 (Fri, 29 Jul 2005)
Revision: 7669
Log message:
Now it seems to be capable of realizing S4 proof of box(a -> a) in LP.
| Changes | Path |
| +1 -0 | metaprl/theories/s4lp/hilbert_internal.mli |
| +116 -79 | metaprl/theories/s4lp/s4_internal.ml |
Changes by: Yegor N. Bryukhov (ybryukhov at gc.cuny.edu)
Date: 2005-07-29 14:33:50 -0700 (Fri, 29 Jul 2005)
Revision: 7670
Log message:
Forgot to remove debug messages.
| Changes | Path |
| +0 -13 | metaprl/theories/s4lp/s4_internal.ml |
