/[mojave]/metaprl/theories/s4lp/s4_logic.ml
ViewVC logotype

Log of /metaprl/theories/s4lp/s4_logic.ml

Parent Directory Parent Directory | Revision Log Revision Log


Links to HEAD: (view) (download) (annotate)
Sticky Revision:

Revision 9655 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 31 18:16:04 2006 UTC (14 years, 7 months ago) by nogin
File length: 16394 byte(s)
Diff to previous 9653
- In browser mode, use "/foo" relative URLs instead of the
  "https://host:port/foo" ones whenever possible. This is needed in order to
  make it easier to access the MetaPRL session indirectly (e.g. via an ssh
  tunnel).

  Only three places will now use the FQ URL:
   - startup message 
   - autologin file
   - form passed to the external editor

- A few display form fixes and improvements.



Revision 9653 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 31 05:41:14 2006 UTC (14 years, 7 months ago) by nogin
File length: 16382 byte(s)
Diff to previous 9652
Fixing a typo


Revision 9652 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 31 05:33:38 2006 UTC (14 years, 7 months ago) by nogin
File length: 16378 byte(s)
Diff to previous 9023
Added iforms - diamond, iff (untested)


Revision 9023 - (view) (download) (annotate) - [select for diffs]
Modified Wed Apr 5 15:12:37 2006 UTC (15 years, 2 months ago) by yegor
File length: 15613 byte(s)
Diff to previous 8705
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.

Revision 8705 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 15 06:59:08 2006 UTC (15 years, 4 months ago) by nogin
File length: 14122 byte(s)
Diff to previous 7802
- Filter_reflection: module names should not be capitalized.

- OMakefile_theories: rules for generating .p4 and .p4i for the reflected
  theories (these are pretty-printed versions of the generated OCaml code;
  useful for debugging the filter).

- OMakefile_theories: in rev 8704 I've ordered the new dependencies for the
  reflect_% files incorrectly (the theory .SUBDIRS did not have them in
  scope); fixed.

- Filter_prog: generate the show_loading debugging call at the beginning and
  end of every theory.

- A _huge_ number of theory files: removed the manual "show_loading" calls as
  they will now be automatically generated.


Revision 7802 - (view) (download) (annotate) - [select for diffs]
Modified Thu Sep 29 15:23:04 2005 UTC (15 years, 8 months ago) by nogin
File length: 14209 byte(s)
Diff to previous 7583
Implemented the type-sensitive interpretation of binding contexts. Now 

arg{| <H> >- 'C |}

that is currently parsed as

arg{| <H<||>[]> >- 'C<|H|>[] |}

will get parsed as

arg{| <H<||>[]> >- 'C<||>[] |}

(i.e. 'C no longer depends on H) when arg is declared as

declare sequent [arg] { Ignore : ... >- ...} : ...
`


Revision 7583 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 12 06:15:11 2005 UTC (15 years, 11 months ago) by yegor
File length: 14308 byte(s)
Diff to previous 7581
Now I have problem with recosntruction of the correct ordering of inferences.


Revision 7581 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 12 01:40:04 2005 UTC (15 years, 11 months ago) by yegor
File length: 13706 byte(s)
Diff to previous 7580
Some minor fixes.
Wise men added but they don't work for some reason.


Revision 7580 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 12 01:11:31 2005 UTC (15 years, 11 months ago) by yegor
File length: 14171 byte(s)
Diff to previous 7577
S4 is working again.
Now I have to test multi-modal behavior.
I also added S4LP to the "theories=all" list


Revision 7577 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 11 07:25:47 2005 UTC (15 years, 11 months ago) by yegor
File length: 14073 byte(s)
Diff to previous 7576
Groundwork for multi-modal S4.
At this moment S4 is actualy broken, but at least ITT is not :)


Revision 7576 - (view) (download) (annotate) - [select for diffs]
Modified Sat Jul 9 22:21:58 2005 UTC (15 years, 11 months ago) by yegor
File length: 13783 byte(s)
Diff to previous 7563
Added an example that shows that LP-multiplicity has no counterpart in S4.


Revision 7563 - (view) (download) (annotate) - [select for diffs]
Modified Thu Jul 7 02:30:10 2005 UTC (15 years, 11 months ago) by nogin
File length: 13662 byte(s)
Diff to previous 7557
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".


Revision 7557 - (view) (download) (annotate) - [select for diffs]
Added Tue Jul 5 01:58:35 2005 UTC (15 years, 11 months ago) by yegor
File length: 13678 byte(s)
Merging S4-prover to the main trunk


This form allows you to request diffs between any two revisions of this file. For each of the two "sides" of the diff, enter a numeric revision.

  Diffs between and
  Type of Diff should be a

  ViewVC Help
Powered by ViewVC 1.1.26