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