/[mojave]/metaprl/theories/itt/itt_theory.ml
ViewVC logotype

Log of /metaprl/theories/itt/itt_theory.ml

Parent Directory Parent Directory | Revision Log Revision Log


Sticky Revision:
(Current path doesn't exist after revision 7950)

Revision 3584 - (view) (download) (annotate) - [select for diffs]
Modified Thu Apr 25 15:28:40 2002 UTC (19 years, 2 months ago) by nogin
File length: 2848 byte(s)
Diff to previous 3329
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.


Revision 3329 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 13 21:34:19 2001 UTC (19 years, 11 months ago) by nogin
File length: 2849 byte(s)
Diff to previous 3325
I've removed old Itt_int* theories and switched all the ITT to Yegor's
new theories.


Revision 3325 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 10 00:11:03 2001 UTC (19 years, 11 months ago) by nogin
File length: 2841 byte(s)
Diff to previous 3312
- Rewrote the Itt_esquash theory based on my "better_tt" ideas.
- Now esquash is a primitive operator and not a defined one.
- This change also broke a few FOL and CZF theories that relied
on a bunch of invalid rules that I had to remove from Itt_esquash.


Revision 3312 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 3 23:55:20 2001 UTC (19 years, 11 months ago) by kopylov
File length: 2874 byte(s)
Diff to previous 3307
- Now substitution (s1=s2 in S) for conclution (t in T[s1]) produces a wf subgoal
   s:S |- T[s] Type
(instead of s:S |- (t in T[s]) Type which was annoying)

- Now assertEqT is more powerful than it was.


Revision 3307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 2 22:34:20 2001 UTC (19 years, 11 months ago) by kopylov
File length: 3087 byte(s)
Diff to previous 3222
- added rules applyEquality to intro resource

- many rules (e.g. letT and elimination rules for the intersection and union types)
  produces equality hypotheses in the subgoals that rarely used in practice.
  Now such rules thin these hypotheses by default.
  To avoid this one can use doNotThinT = thinningT false.


Revision 3222 - (view) (download) (annotate) - [select for diffs]
Modified Tue May 8 22:00:34 2001 UTC (20 years, 1 month ago) by nogin
File length: 2854 byte(s)
Diff to previous 3058
- Fixed slot["raw", ...]
- Fixed couple small typos.


Revision 3058 - (view) (download) (annotate) - [select for diffs]
Modified Sun Sep 10 20:41:19 2000 UTC (20 years, 9 months ago) by jyh
File length: 2853 byte(s)
Diff to previous 2812
Last commit failed partway through...


Revision 2812 - (view) (download) (annotate) - [select for diffs]
Modified Tue Sep 7 00:44:30 1999 UTC (21 years, 9 months ago) by jyh
File length: 2463 byte(s)
Diff to previous 2775
Finally fixed the tutorial so that we have a derivation of
classical first-order logic.  The HTML docs are not yet up-to-date.


Revision 2775 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 4 13:13:44 1999 UTC (21 years, 11 months ago) by jyh
File length: 2393 byte(s)
Diff to previous 2773
Things seem to be working pretty smoothly now.  This is mostly minor
fixes.  Still need to fix the problems with the mp toploop.

    1. Proofs now use Alexey's ASCII format.  By default, proofs
       should be saved to CVS in .prla format.  You can generate ASCII
       files by using "make export", or you can use the "export ()"
       instead of the "save ()" command in the editor.  For speed,
       .prlb files are now saved in a raw, marshaled format.  When you
       edit a theory, the newest of .cmoz, .prlb, or .prla files is
       loaded.  There is a new command "convert" to convert between
       all the different proof file formats.
          convert -I ... [-raw|-term|-lib|-ascii] -impl file.cmoz
          raw: save the file in fast, raw format
	  term: save the file as <magic#>/<marshaled term_io>
	  lib: send the file to the Nuprl5 library
	  ascii: create a .prla file

       Developers: _please_ mention any changes to the basic data
          structures in your CVS logs.  The things that matter are:
          Refiner.Refiner.TermType.term
	  Filter_summary.summary_info
	  Tactic_boot_sig.TacticType.{tactic_arg,extract}
	  Proof_boot.io_proof

       Users: to be safe, save all your proofs using "make export"
          before doing a cvs update.

    2. "expand ()" and "expand_all ()" now work.  I also added
       "clean ()" and "clean_all ()" commands to remove those peasky
       dangling proof nodes when you are satisfied with a proof.  By
       default, proofs are saved only down to the innermost rule-box
       level, and primitive refinements are omitted.  I haven't added
       a "deep_save ()" command; it seems unecessary.

    3. Sorry, but I had to move theories/boot into the filter.  There
       are no major changes here, but the directory structure in
       filter has changed significantly.

    4. I added a THEORIES variable to the mk/config file that
       specifies what theories you want to compile.  This means that
       you don't have to edit all the Makefiles when you add a theory,
       and it also means that you can keep your own theories without
       having to commit them to cvs.


Revision 2773 - (view) (download) (annotate) - [select for diffs]
Modified Sun Jul 4 03:02:58 1999 UTC (21 years, 11 months ago) by nogin
File length: 2368 byte(s)
Diff to previous 2529
I wrote a decideT tactic, similar to Nuprl4 Decide tactic.

We need to prove some decidability rules and add them to the decide_resource
in order to make this tactic useful.


Revision 2529 - (view) (download) (annotate) - [select for diffs]
Modified Tue Dec 29 23:30:21 1998 UTC (22 years, 5 months ago) by jyh
File length: 2346 byte(s)
Diff to previous 2525
Added pigeonhole problem in editor/ml/test.ml.

To try it:

% ./mptop
# #use "y.ml";;
# refine timingT proveT;;


Revision 2525 - (view) (download) (annotate) - [select for diffs]
Modified Mon Dec 28 21:07:52 1998 UTC (22 years, 5 months ago) by jyh
File length: 2346 byte(s)
Diff to previous 2494
Numerous minor changes.

Added itt_fset: a theory of finite sets based on a list
implementation quotiented by equivalence under arbitrary
occurrences and ordering.

Added initial reflection theory.  Terms are quotiented by
alpha-equality, so normal well-formedness proofs are difficult,
and more work needs to be done to define free variables and
substitution.


Revision 2494 - (view) (download) (annotate) - [select for diffs]
Modified Tue Oct 13 01:14:08 1998 UTC (22 years, 8 months ago) by jyh
File length: 1991 byte(s)
Diff to previous 2493
I changed all the obvious places of Nuprl-Light, NL, nl, or any
other instance to MetaPRL, MP, or mp, etc.  The docs may be broken
but I'll fix them soon.  As usual, let me know if anything breaks.


Revision 2493 - (view) (download) (annotate) - [select for diffs]
Modified Mon Oct 12 22:40:01 1998 UTC (22 years, 8 months ago) by jyh
File length: 1995 byte(s)
Diff to previous 2456
Added "reflection" theory, for reflecting sentences in the meta-logic
into the Nuprl type theory.


Revision 2456 - (view) (download) (annotate) - [select for diffs]
Modified Sat Sep 5 22:31:37 1998 UTC (22 years, 9 months ago) by jyh
File length: 1957 byte(s)
Diff to previous 2439
Added license headers to each of the files in preparation for
the first major release.  The license is GNU public license; if
any of you have problems with that, let me know right away.  When
you add new code, you should credit yourself as the author.  When
you modify code, you should add a "Modified by:" to the header,
and possibly a short summary of your changes.

I tried to get the Author lists as correct as I remember, but there
are more than 550 files(!) and I may have made some mistakes. Please
add yourself if I didn't do it right.


Revision 2439 - (view) (download) (annotate) - [select for diffs]
Modified Thu Aug 13 20:26:48 1998 UTC (22 years, 10 months ago) by eli
File length: 798 byte(s)
Diff to previous 2325
Placed propDecideT in itt_prop_decide.


Revision 2325 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 14 15:44:03 1998 UTC (22 years, 11 months ago) by jyh
File length: 774 byte(s)
Diff to previous 2307
Intermediate version with auto tactic.


Revision 2307 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 17:55:31 1998 UTC (22 years, 11 months ago) by nogin
File length: 755 byte(s)
Diff to previous 2300
Removed $Log messages from all NL files.


Revision 2300 - (view) (download) (annotate) - [select for diffs]
Added Sun Jul 5 01:47:36 1998 UTC (22 years, 11 months ago) by jyh
File length: 1980 byte(s)
Itt_theory.ml{,i} are now different.


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