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;&nbs
