/[mojave]/metaprl/theories/itt/itt_logic.mli
ViewVC logotype

Log of /metaprl/theories/itt/itt_logic.mli

Parent Directory Parent Directory | Revision Log Revision Log


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

Revision 2921 - (view) (download) (annotate) - [select for diffs]
Modified Mon Mar 13 23:03:12 2000 UTC (21 years, 3 months ago) by steph
File length: 5243 byte(s)
Diff to previous 2880
 ----------------------------------------------------------------------
 Enter Log.  Lines beginning with `CVS:' are removed automatically

 Committing in .

 Modified Files:
 	itt_logic.ml itt_logic.mli
 ----------------------------------------------------------------------


Revision 2880 - (view) (download) (annotate) - [select for diffs]
Modified Wed Feb 2 18:19:32 2000 UTC (21 years, 4 months ago) by steph
File length: 5398 byte(s)
Diff to previous 2786
*** empty log message ***


Revision 2786 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 5 13:38:57 1999 UTC (21 years, 11 months ago) by jyh
File length: 4967 byte(s)
Diff to previous 2743
Added: Itt_logic.genAssumT : int list -> tactic
This tactical "generalizes" over a set of assumptions.  The first
assumption should be for a membership judgment.  For example:
   ...
i. H >- t in T list
   ...
j. H >- Q[t]
   ...
   H >- P[t]
   BY genAssumT [i; j]
1. H >- all l: T list. (Q[l] => P[l])
2. H; x: (all l: T list. (Q[l] => P[l])) >- P[t]


Revision 2743 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jun 23 04:50:29 1999 UTC (21 years, 11 months ago) by jyh
File length: 4928 byte(s)
Diff to previous 2674
This is a major release; I bumped the release number to 0.6.
WARNING: There are major changes here, and there may be problems
   with this version that prevent you from using your old proof.
   Save your work before using this version.
NOTE: If you decide to try this out, and you find problems,
   please(!) send me email so I can fix it.

Changes:
   1. The proof structure is totally changed, so that the proof
      editor edits the raw proof extracts.  This means that you
      can view the actions of the refiner down to the primitive
      rule applications.  In the proof editor, you can use
      "down 0" (or "cd "0") to descend into the proof of a rule box.
      Primitive proofs are called "extracts", and are labeled with
      brackets (like [extract]).  To expand the extract, use the command
      "unfold ()".  You should be able to get all the way down to
      the primitive rule/rewrite applications.

      This also means that the format of the proof files (the .prlb
      files) has changed.  The old proof files are still valid,
      but this is a hack and will be deprecated in the next
      few months.  I haven't yet added Alexey's ASCII proof
      files, but that will come with the next release.

      As usual, the "undo ()" command undoes the last proof step,
      including "unfold ()".  The "nop ()" command, reset the undo
      stack.  I also added a "redo ()" command that undoes the
      last undo.

      There is a simple rule-box proof cache for collecting proofs
      as you edit them.  If cached proofs are available, you will
      see them in brackets (like [* # * *]) on the status line.
      I haven't yet:( added the commands to use cached proofs.

   2. Refiner changes.  I added two new features: the "cutT <term>"
      tactic cuts in a new assumption.  Also, you can apply
      rewrites directly on assumptions, with the "rwc" and
      "rwch" operations, that take a clause argument.  Basically,
      this means that instead of folding the goal, you can unfold
      the assumption.  I believe this is sound; let me know if
      you think otherwise!

   3. Resource changes.  I added resource automation, built on
      the basic resource parsing Alexey added.  Ratherthan writing
      resource code for every rule, you can annotate most rules
      to generate the resource code directly.  You can see lots of
      examples in the Itt theory.  Basically, there are three useful
      resources annotations:
         intro_resource []: adds the rule as an introduction in dT
         intro_resource [SelectOption i]: adds to selT i dT
         elim_resource []: adds as an elimination rule to dT.
            This normally tries to thin the hyp that was eliminated.
         elim_resource [ThinOption]: don't thin the hyp

      Rules should be annotated with labels on their clauses,
      like [wf], [main], [assertion], etc.  This means that in
      most tactic aplcations, you no longer need to have the
      thenLT [addHiddenLabel "main"; ...] part.

      N.B.  This is the most likey parts of this release to
      cause problems, because I deleted most old resource code.

      Also, you can still write standard resource code, but there
      is no longer a d_resource--it has been broken into two parts:
      the intro_resource for application to goals, and elim_resource
      for application to hyps.

   4. The proof editor is multi-threaded, so you can work on multiple
      proofs simultaneously.  In the normal Emacs editor, this is
      no help for you.  But there is a new Java editor with the
      standard point-and-click interface, and it views the proof
      in HTML, with multiple windows etc.  The beautiful thing is
      that you can use display forms to add commands to edit windows.
      The sad thing is that I built it on NT, Java 1.2 is required,
      and I haven't tried the blackdown.org Java release on Linux.
      This editor is pending some bug fixes from Sun to get the
      fonts right (they call this a standard release?).

      In any case, here are the direct implications.  The display
      forms have an "html" mode.  The display form formatting in
      the module Rformat has been completely redone, but display
      _should_ be the same as it was before.

      It is likely that I will add an HTML dump, so we can send
      uneditable proofs around by email or on the web.  Check out
      the file theories/base/summary.ml to see some example HTML
      display forms.

      The other issue: your MetaPRL process starts a web server on
      YOUR local machine using YOUR process id on the "next" available
      TCP port, and it serves files only from the search path that you pass
      MetaPRL.  I realize that this has security implications.  This
      is necessary to get browser access to the working MetaPRL proof.
      Is this crazy?  Let me know your beliefs, religious or
      otherwise.

   5. There are numerous minor changes.  I redid parts of the WeakMemo,
      Term_header_constr, and TermHash.  The theories/tactic directory
      has been split into tactic/boot (which is not compiled by MetaPRL),
      and theories/tactic (which is).

Jason


Revision 2674 - (view) (download) (annotate) - [select for diffs]
Modified Wed May 26 00:41:08 1999 UTC (22 years ago) by nogin
File length: 4904 byte(s)
Diff to previous 2669
I removed @ from the parameter syntax for meta-parameters. Now
[xxx:s] is parsed as a meta-string parameter (MString "xxx") and
["xxx":s] is parsed as a string parameter (Sting "xxx")

I also copied .cmoz files to .prlb files until I've reached a fixpoint.


Revision 2669 - (view) (download) (annotate) - [select for diffs]
Modified Sun May 23 21:55:17 1999 UTC (22 years ago) by jyh
File length: 4906 byte(s)
Diff to previous 2529
This is a major modification to how parameters are handled.
1. All level parmeters are now meta.  That is, univ[@i:l] is
   exactly the same as univ[i:l].  The rewriter handles
   lavel expressions, so matching with levels like
   univ[3 | i':l | j:l] should work correctly.

   The syntax still requires the @ for meta-parameter of
   other types.  For instance, token["hello world":t] is
   a normal token, and token[@"hello world":t] is a
   token with a meta-parameter.

2. There are no more parameter expressions.  For instance,
   the term natural_number[@i + @j] is not valid anymore.
   To replace them, the module theories/base/base_meta.ml
   defines ML rewrites that implement the same functionality.
   For example,
      meta_sum{number[12]; number[5]} --> number[17]

3. There is no term natural_number[@i:n] any more.  This was
   always a bad name, since it has always been possible for the
   parameter to be negative.

4. The Itt_equal.cumulativity rule is no longer defined as a
   side-condition.  It now uses Base_meta.meta_lt to define
   inclusion on level expression.  Cumulativity expansion
   should be performed automatically by the dT tactic.
   So:
      sequent ['ext] { ... >- univ[@i:l] = univ[@i:l] in univ[@j:l] }
      BY dT 0
   should always either succeed or fail, without producing
   subgoals.

I haven't fully tested the side-conditions.  As usual, let me know
if you see anything strange.  Next, I'm looking at the
rewriter free variable soundness problem.


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: 4995 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: 4981 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: 4954 byte(s)
Diff to previous 2456
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 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: 4958 byte(s)
Diff to previous 2380
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 2380 - (view) (download) (annotate) - [select for diffs]
Modified Sun Aug 2 17:12:26 1998 UTC (22 years, 10 months ago) by jyh
File length: 3799 byte(s)
Diff to previous 2376
Modified rewriter to handle Alexey's new sequents.  The rewriter is
now moved to a new directory refiner/rewrite.  Clause numbers in
TermMan now start with 1.  The tactics seem to work, but there may
be some lurking problems with hypothesis numbering.


Revision 2376 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 31 14:35:45 1998 UTC (22 years, 10 months ago) by jyh
File length: 3413 byte(s)
Diff to previous 2336
Added TPTP theory, and Ensemble library.  Fixed sequent displays.
BUG: rewrites fail on sequents.


Revision 2336 - (view) (download) (annotate) - [select for diffs]
Modified Tue Jul 21 22:47:13 1998 UTC (22 years, 10 months ago) by jyh
File length: 4028 byte(s)
Diff to previous 2333
Added NL toploop so that we can compile NL native code.


Revision 2333 - (view) (download) (annotate) - [select for diffs]
Modified Fri Jul 17 15:39:32 1998 UTC (22 years, 11 months ago) by jyh
File length: 3977 byte(s)
Diff to previous 2325
CZF is complete, although we may wish to add pairing and inf.


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: 3698 byte(s)
Diff to previous 2314
Intermediate version with auto tactic.


Revision 2314 - (view) (download) (annotate) - [select for diffs]
Modified Wed Jul 8 15:42:11 1998 UTC (22 years, 11 months ago) by jyh
File length: 2879 byte(s)
Diff to previous 2309
Pushed higherC into the refiner for efficiency.


Revision 2309 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jul 6 21:39:34 1998 UTC (22 years, 11 months ago) by jyh
File length: 2473 byte(s)
Diff to previous 2307
Working czf_itt_set.


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: 2289 byte(s)
Diff to previous 2244
Removed $Log messages from all NL files.


Revision 2244 - (view) (download) (annotate) - [select for diffs]
Modified Mon Jun 15 22:33:52 1998 UTC (23 years ago) by jyh
File length: 3328 byte(s)
Diff to previous 2190
Added CZF.


Revision 2190 - (view) (download) (annotate) - [select for diffs]
Modified Thu May 28 13:48:44 1998 UTC (23 years ago) by jyh
File length: 3105 byte(s)
Diff to previous 2047
Updated the editor to use new Refiner structure.
ITT needs dform names.


Revision 2047 - (view) (download) (annotate) - [select for diffs]
Modified Wed Aug 6 16:18:55 1997 UTC (23 years, 10 months ago) by jyh
File length: 2966 byte(s)
Diff to previous 2032
This is an ocaml version with subtyping, type inference,
d and eqcd tactics.  It is a basic system, but not debugged.


Revision 2032 - (view) (download) (annotate) - [select for diffs]
Added Mon Apr 28 15:52:46 1997 UTC (24 years, 1 month ago) by jyh
File length: 1681 byte(s)
This is the initial checkin of Nuprl-Light.
I am porting the editor, so it is not included
in this checkin.

Directories:
    refiner: logic engine
    filter: front end to the Ocaml compiler
    editor: Emacs proof editor
    util: utilities
    mk: Makefile templates


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