/[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 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