Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-04-05 15:28:23 -0700 (Wed, 05 Apr 2000)
Revision: 2926
Log message:

      
      
      Full first order prover for J plus (incomplete) proof reconstruction
      in LJ, LJmc and LK.
      Moreover, jprover starts from sequent
      

Changes  Path
+1 -1 metaprl/editor/ml/nuprl_jprover.ml
+1 -1 metaprl/editor/ml/nuprl_jprover.mli
+1154 -215 metaprl/refiner/reflib/jall.ml
+6 -3 metaprl/refiner/reflib/jall.mli
+75 -134 metaprl/refiner/reflib/jtunify.ml
+2 -1 metaprl/refiner/reflib/jtunify.mli
+3 -1 metaprl/theories/itt/itt_logic.ml
+3 -1 metaprl/theories/itt/itt_logic.mli

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2000-04-13 12:18:43 -0700 (Thu, 13 Apr 2000)
Revision: 2932
Log message:

      committed jprover/nuprl interface changes
      

Changes  Path
+10 -4 metaprl/editor/ml/nuprl_jprover.ml
+3 -0 metaprl/editor/ml/nuprl_jprover.mli
+2 -0 metaprl/editor/ml/nuprl_run.mli
+8 -8 metaprl/library/nuprl5.ml

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-04-13 16:24:44 -0700 (Thu, 13 Apr 2000)
Revision: 2933
Log message:

      
      First-order jprover with sequents unique name generation
      

Changes  Path
+292 -103 metaprl/refiner/reflib/jall.ml

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-04-13 16:26:25 -0700 (Thu, 13 Apr 2000)
Revision: 2934
Log message:

      I started writing a formal description of the syntax of sequent schemas
      that are used in rule specifications and when proving derived rules.
      
      I am planning to give a formal definition of what it means for a sequent
      specification to be a refinement of another sequent specification.
      
      After that I am going to start proving that the way we use rules on sequent
      schemas instead of ordinary sequents when proving derived rules is valid.
      Since under the current implementation it is _not_ completely valid,
      I will only sketch a proof, but this should be enough to understand
      what we need to add to make it completely valid.
      

Changes  Path
+2 -0 metaprl/doc/htmlman/user-guide/mp-axiom.html

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-04-15 15:26:32 -0700 (Sat, 15 Apr 2000)
Revision: 2935
Log message:

      Added more files to "make clean".
      

Changes  Path
+1 -1 metaprl/doc/Makefile

Changes by: Lori Lorigo (lorigo at sbcglobal.net)
Date: 2000-04-18 11:52:46 -0700 (Tue, 18 Apr 2000)
Revision: 2938
Log message:

      adding threaded call for jprover/nuprl connection
      

Changes  Path
+1 -1 metaprl/editor/ml/nuprl_jprover.ml
+1 -1 metaprl/editor/ml/nuprl_jprover.mli
+3 -0 metaprl/editor/ml/nuprl_run.ml
+1 -0 metaprl/editor/ml/nuprl_run.mli

Changes by: Aleksey Nogin (nogin at cs.caltech.edu)
Date: 2000-04-24 01:54:41 -0700 (Mon, 24 Apr 2000)
Revision: 2941
Log message:

      Added some information and some ideas:
      - FO Unification status and bugs
      - by-context free variables problem
      - dynamic tactics resource to allow easy redefining of tactics.
      - read-only theories to avoid unnecessary resource checkpointing.
      
      Spell-checked.
      

Changes  Path
+16 -3 metaprl/BUGS

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-04-26 08:40:47 -0700 (Wed, 26 Apr 2000)
Revision: 2942
Log message:

      JProver with complete proof reconstruction -- Beta proofs and Proof
      permutations
      

Changes  Path
+1201 -78 metaprl/refiner/reflib/jall.ml

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-04-26 14:11:31 -0700 (Wed, 26 Apr 2000)
Revision: 2943
Log message:

      JProver with unique name v0_jprover for undeclared parameters
      

Changes  Path
+35 -4 metaprl/refiner/reflib/jall.ml

Changes by: Stephan Schmitt (sschmitt at sapient.com)
Date: 2000-04-27 08:50:52 -0700 (Thu, 27 Apr 2000)
Revision: 2946
Log message:

      minor modifications
      

Changes  Path
+2 -0 metaprl/refiner/reflib/jall.ml