In this file I'll try to record the differences in the various patchlevels of Otter 3.0. The most recent entries are at the end. -------------------------------------------------------- Otter 2.99 released November 25, 1993. -------------------------------------------------------- Many small changes. Otter 3.0.0 released January 24, 1994. -------------------------------------------------------- Check for errors when reading clause id from terminal, flag interactive_given, routine find_interactive_clause(). FormEd only: parsing strings read interactively, routine str_2_formula(). Problem with dynamic demodulators that have answer literal before equality. (Answer lits are not propogated during demodulation, so I can't see any use for answer lits on input demodulators, but they can occur indynamic demodulators.) Changed contract_lin(), insert_imd(), delete_imd(), new_demod(), back_demod(), post_process(), so that they use ith_literal(), which skips answer lits. Also changed check_input_demod() to allow answer lits on input demodulators. Otter 3.0.1 - DOS version released Feb 22, 1994. -------------------------------------------------------- Optimized forward subsumption for nonunit clauses: require that found literal be first literal. Routine forward subsume() in file clause.c. Mar. 21, 1994. Bug in unit deletion when answer literals with fresh variables introduced. Factor_simp crashes because variables not renumbered. Fix: in unit_del(), renumber variables if ANY answer literals introduced. Result is otter301b. March 31, 1994. Added code to translate otter input for Davis-Putnam model searcher: set(dp_transform). Result is otter301dp. Apr. 13, 1994. Slight change to Davis-Putnam translator so that it outputs vraiable names with "v" instead of plain integers. May 23, 1994. Kunen convinced me to make answer literals sound. In particular, if they occur on demodulators, then they should be inherited by rewritten clauses. Since inheriting during demodulation would slow it down, would take a lot of time to code, and would be of questionable value, I'll simply not let demodulators have answer literals. Fix: check_input_demod(), pre_process(); new routine num_literals_including_answers(). NOTE: Subsumption still ignores answer literals, and factoring still attempts to factor answer literals. Result is otter301c. June 8, 1994. In proggen() (process generated clauses) moved cl_merge() after factor_simplify() to make construction of proof objects easier. June 8, 1994. When input clauses are changed in procgen() (due to flag process_input), e.g., by demod, unit_del, or factor_simp, the original input clause is now assigned an ID and appears in proofs. The new inference rule "copy" indicates this. Changed header.h, pre_process(), and print_clause(). Motivation: to make proofs easiser to read and to ease proof object construction. June 8, 1994. When equality literals are flipped, add an entry to the justification list. Changed order_equalities(), order_equalities_lrpo(), post_process(), header.h, proc_gen(), print_clause(), maybe others??. Motivation: to make proofs easiser to read and to ease proof object construction. June 9--16, 1994. Various changes related to construction of proof objects. Otter 3.0.2 - UNIX version released June 17, 1994 -------------------------------------------------------- July 14, 1994. Bug in FPA indexing, because abs(2^31) returns 2^31, a negative number! Change one line in hash_path(), file fpa.c. Result is otter302a. July 14, 1994. Bug (feature?) about symbol order of dynamically-introduced symbols. (Arose with sort_literals, $SUM, without lex([...]) command. Change lex_compare_sym_nums() so that if either has no lex value, then call compare_for_auto_lex_order() to comprare. Note that this may change behavior, because before the fix, if one symbol has lex_val and the other does not, then the one with lex_val is smaller. Result is otter302b. August 5, 1994. Bug with dynamic hot list. When making hot inference with a clause C, if new clause was added to hot list, then when return to making hot inferences with C, the ordinary index would be used instead of the hot index. Result: lose a few hot inferences, get a lot of bogus (but sound) hot inferences. Also, one other small bug: heat_level wsa not copied to new hot list clauses. Bugs fixed. Result is otter302c. ----------------------------------------------------------- August 23, 1994. Added new flag `log_for_x_show' which causes some statistics to be periodically logged to a special file so that the user can have a real-time X display of some properties of the search. August 24, 1994. Added two new statistics: PASSIVE_SIZE and HOT_SIZE. August 25, 1994. Added $dots for weight templates. Added parameter MAX_ANSWERS. ----------------------------------------------------------- Otter 3.0.3 released August 26, 1994. ----------------------------------------------------------- Sept. 21, 1994. (Veroff,Kunen) Bug getting ancestors with [...,flip,1,...], because the 1 does not refer to a clause. Change the flip position to a list (like all other positions). Now get [...,flip.1,...], (note period). Changed post_process(), proc_gen(), and finish_translating(). Oct 24, 1995. Deleted GEOMETRIC_REWRITE (which occurred after demod), and added GEOMETRIC_REWRITE_BEFORE and GEOMETRIC_REWRITE_AFTER (demod). Jan 4, 1995. Overbeek requested an extension to weighting. This includes the new command "overbeek_terms([])." When an argument of an atom is being weighed, if it is an instance of a term in overbeek_terms, then it gets weight 0. Jan 12, 1995. Overbeek requested a change (see preceding) so that we check for a noncomplexifying instance. The result is otter303b. Jan 22, 1995. Veroff found a bug about reordering equalities in nonunits. Equalities that should not be flipped are sometimes flipped. Changed order_equalities() in weight.c. The result is otter303c. Feb 21, 1995. Yuan Yu pointed out that max_answers doesn't work. Fix is s/MAX_LITERALS/MAX_ANSWERS/ in process.c (line 411 in 3.0.3, line 415 in current). Looks like it wasn't tested when first installed. The result is otter303d. Feb 21, 1995. log_for_x_show() in misc.c had new_style procedure declaration (so it wouldn't work with cc). Fixed. March 7, 1995. Bug in ancestor_subsume (wos). If, during a given clause, you keep more than one ocurrence, back subsumption (because it didn't check anc_subsume()), deletes all but the first. The fix is to have back_subsume() check anc_subsume() (file clause.c). Fixed. The result is otter303e. March 31, 1995. Enhancement suggested by Ingo Dahn: quantified formulas can now appear in proofs, just like clauses do. The skolemized input clauses can have the quantified formula as parent, e.g., [clausify,4]. One gets this feature by setting the new flag formula_history. The result is otter303f. April 7, 1995. Updated build_proof_object so that it can build proof objects with lex-dependent demodulation. April 9, 1995. Installed primitive "hints" mechanism. (It will be changed when the real hints mech. is installed.) April 11, 1995. Some cleanup and bug fixes from Art Quaife (email #27, 9/6/94). Two bugs: getppid() call in init_log_for_x_show() (misc.c) undefined for nonNUIX systems. Move to nonport.c and call only if TP_NAMES is defined. variant() in check.c forgot to tpos=*trp. In av.c, discarded routines term_ptr_get_size() and is_tree_get_size(), because obsolete. Fixed "unreachable break"s in several places. Unit deletion doesn't work if forward subsumption is disabled. Fixed by changing index_lits_all() and un_index_lits_all(). If the two symbols given to the make_evaluable command have different arities, CRASH! Fixed by including check in read_a_file(). Passive list units used for unit deletion. The manual says that the passive list is used only for subsumption and unit conflict. Fixed unit_del() in file clause.c April 12, 1995. Removed all ROO code and references (#ifdefs). April 12-13, 1995. Install some of Veroff's features: (1) Debugging: DEBUG_FIRST DEBUG_LAST VERBOSE_DEMOD_SKIP (2) Hints: FSUB_HINT_ADD_WT BSUB_HINT_ADD_WT EQUIV_HINT_ADD_WT KEEP_HINT_SUBSUMERS (3) Evaluable symbols: $UNIQUE_NUM, $RENAME(_,_); April 21, 1995. Add flag PROOF_WEIGHT. If set, (1) the "weight" of a proof is printed along with its level and length, and (2) ancestor subsumption uses "weight" instead of the proof length. The weight of a proof is the number of leaves in the proof tree, that is, the number of OCCURRENCES of input clauses in the proof tree. The result is otter303g. April 25, 1995. Bug (wos). If more than 32767 symbols, CRASH!, because term->sym_num was short, and no check in new_sym_num(). Fix: make sym_num unsigned short (so we can have 65535 symbols), and put check in new_sym_num(), so it will abend instead of crash. April 25, 1995. Secret flag, hyper_symmetry_kludge. The result if otter303h. May 18, 1995. Bug (kunen). Unit deletion with a unit containing answer literals. This can cause an infinite loop, incorrect answers, or a crash. The problem is a leftover context pointer in a substitution. Otter was designed for this to be ok, but I forgot that when updating unit_del to handle answers. The solution is to set the context pointer to NULL when binding variables in is_retrieve(). I changed imd_retrieve() analogously. May 18, 1995. Bug (Ohlbach). set(auto), set(free_all_mem) -> CRASH! when printing statistics at the end of the run. Because free_all_mem deletes lists, then stats (level 1) tries to look at lists. Fixed by including more checks in print_*_brief() in misc.c. otter303i ------------ June 5, 1995. DP preprocessing - delete some subsumed clauses. June 16, 1995. DP preprocessing - change form of output; output ordinary clauses as well as relational clauses, and all clauses get IDs (in preparations for Olga's MACE enhancements). otter303j ------------ June 20--23, 1995. Veroff visit. We made a great many changes. Here is a summary. 1. New parameters to decide dynamic demodulators when lrpo is clear: dynamic_demod_depth (default -1) dynamic_demod_rhs (default 1) Here is the new code. /* equality alpha=beta */ else if (var_subset(beta, alpha)) { if (Flags[DYNAMIC_DEMOD_ALL].val) return(1); /* make it a demodulator */ else { wt_left = weight(alpha, Weight_terms_index); wt_right = weight(beta, Weight_terms_index); if (wt_right <= Parms[DYNAMIC_DEMOD_RHS].val && wt_left - wt_right >= Parms[DYNAMIC_DEMOD_DEPTH].val) return(1); /* make it a demodulator */ } } If these parameters are not used, Otter should behave ase before. 2. New parameters to adjust the pick_given weight of clauses. age_factor (default 0) distinct_vars_factor (default 0) Here is the new code. /* c is a newly kept clause that already has its ordinary pick-weight. */ if (Parms[AGE_FACTOR].val != 0) c->pick_weight = c->pick_weight + (Stats[CL_GIVEN] / Parms[AGE_FACTOR].val); if (Parms[DISTINCT_VARS_FACTOR].val != 0) c->pick_weight = c->pick_weight + (distinct_vars(c) * Parms[DISTINCT_VARS_FACTOR].val); 3. Special_unary processing has been improved. If you use this feature, check the code in lex_order() and lex_order_vars() to see how it works now. 4. The hints mechanism has been overhauled. From hints.c: The main purpose of the hints mechanism is to set or adjust the pick-given weight of clauses. A hint H can apply to a clause C in 3 ways: H subsumes C (forward subsume, fsub), C subsumes H (back subsume, bsub), and H is equivalent to C (equiv, which implies fsub and bsub). 2 more ways, which apply to unit clauses only, to be added later: H and C unify H anc C have the same shape (identical-except-variables) Another purpose of hints is to retain clauses that would otherwise be discarded because the purge-gen weight is too high. The Flag KEEP_HINT_SUBSUMERS (default clear) says to skip the purge-gen test on generated clauses that subsume hints (i.e., bsub). The Parms are FSUB_HINT_WT FSUB_HINT_ADD_WT BSUB_HINT_WT BSUB_HINT_ADD_WT EQUIV_HINT_WT EQUIV_HINT_ADD_WT These can be overridden for individual hints with corresponding attributes on the hints, e.g., p0(a,x) # bsub_hint_wt(200) # fsub_hint_wt(100). If the Parms (attributes) are not set, they are not used; if you have a list of hints with no attributes, and you don't set any hint parms, the hints won't be used for anything. If more than Parm (attribute) might apply, equiv is tested first, then fsub, then bsub. If you use both WT and ADD_WT, then BOTH can apply, e.g., when the hint p # bsub_hint_wt(200) # bsub_hint_add_wt(20). applies to a clause, the clause gets pick-given weight 220. The hint attributes and parameters are compiled into a special structure that is attached to the hint clause with the parents pointer. This causes several problems. (1) Compiled hints must be printed with print_hint_clause() instead of print_clause(), and (2) the Parms in effect at the start of the search are compiled in; if the user changes hint parms during the search, this will have no effect. 5. A new attribute mechanism has been installed. This allows users to attach supported attributes to clauses, and allows Otter programmers to easily add new attributes. Each attribtue has a type in [boolean, integer, double, string, otter-term]. W.r.t. I/O, attributes look just like positive literals with one argument. The name of the attribute is the "predicate symbol", and the value is the argument. Attributes are appended to clauses with the "#" operator. For example, the following clause has two literals and two attributes (integer and string). p | q # bsub_hint_wt(-10) # label("This is a label"). We think the Boolean and integer types will be useful to have flags and parameters apply only to particular clauses. The first set of attributes are for the hints mechanism. bsub_hint_wt fsub_hint_wt equiv_hint_wt bsub_hint_add_wt fsub_hint_add_wt equiv_hint_add_wt These have type integer, and correspond to the ordinary hint parameters of the same names, and can be used to override the ordinary parameters for particular hint clauses. Another implemented attribute is label, whose type is string. The way it works is that if the pick-given weight of a clause is changed by a hint with a label attribute, the clause gets a copy of the label attribute. ------------ July 6, 1995. DP preprocessing - fix g(0)=1 bug, introduce flag dp_int_domain to say that integers are domain elements, and make several small changes. ------------ otter303k - July 7, 1995. ------------ July 14, 1995. Improve demodulation in proof object construction. July 26, 1995. Prevent paramodulation from t=t in para_from rule. July 27, 1995. Install Slaney's Scott fragments, all with #ifdef SCOTT. otter303l - Aug 4, 1995. August 9, 1995. A few minor corrections to the manual. (The manual does not document any of the new features.) August 10, 1995. Change dp_transform so that Sos and Dedmodulators are used as well as Usable. This is so that ordinary Otter input files (except for passive list) can be used for MACE input. August 16, 1995. A few small things suggested by Mark Stickel for the Macintosh version. --------------- Otter 3.0.4 released -- August 16, 1995. --------------- Sept 24, 1995 -- 3 minor corrections in the examples directory. wos/manyval.sparc2 is missing the statistics, wos/README is missing, and examples/README refers to a 486 instead of a Sparc2. I'll just silently rerelease 3.0.4, because Otter hasn't changed. --------------- Otter 3.0.4 rereleased -- Sept. 24, 1995. --------------- Nov 16, 1995. Minor bug (incompleteness) in build_proof_object that sometimes causes abend with lex-dependent demodulators. Fixed. Result is otter304a. Feb 12, 1996. Very minor bug: auto output message in misc.c corrected. Feb 28, 1996. Added flag "discard_non_oriented_eq", which will, if order_eq is set, discard nonorientable positive equality units. Result is otter304b. May 6, 1996. Bug in forward subsumption when doing ancestor subsumption with nonunits. I believe the only bad effect of the bug is that subsumption can be incomplete, that is, a subsumed clause will be kept. This is not a major bug, because (a) almost no one uses ancestor subsumption (b) when it is used, it is almost always with units, (c) when the problem occurs, an error message goes to stdout, (d) ancestor subsumption is highly experimental and not well understood anyway. To fix, move clear_subst_1(tr) call in forward_subsume(). Result is otter304c. April 2, 1997. New flag "discard_xx_resolvable", which causes nonunit clauses containing a literal that can be resolved with x=x to be deleted. (For new-foundations project.) Result is otter304d. April 12, 1997. Change the format of proof objects. I added a new field to lines in proof objects. If the new field is not empty, it gives the ID number of the corresponding (equivalent) line in the ordinary Otter proof. Before: ( ) After: ( ) ---------------- June 1997. Several changes to prepare for CASC-14 (CADE-14 contest). 1. New flag set(tptp_eq). Ordinarily, a predicate symbol is recognized as equality for paramodulation and demodulation if it is "=", or if it starts with "EQ", "eq", or "Eq". If tptp_eq is set, a predicate symbol is equality iff it is "equal". This is because TPTP has nonequality predicate symbols that start with "eq". 2. A new automatic mode. I wish to be able to introduce new auto modes and keep all of the old auto modes. But if the user has to choose between auto modes, the program is not really automatic. Therefore, I'll have flags "auto1", "auto2", ..., for the auto modes, and also have a flag "auto" (like a symbolic link) which which specifies the default auto mode. Two new flags: auto1 and auto2. auto1 specifies the old auto mode, and auto2 the new one. The default will be auto2. (So if you you wish your old auto input files to work the same way with the new otter, you should use set(auto1). See README.305 for a description of the new auto mode. The result of these changes is called otter305-beta, the version used for CASC-14 (July 16, 1997). August 21, 1997. Two new parameters: warn_mem and warn_mem_max_weight. These are used together to reset the max_weight (to warn_mem_max_weight), when a specified amount of memory (warn_mem) has been used. For example, if you wish to reset the max_weight to 10 after 90 megabytes of memory has been used, include the following in your input file. assign(warn_mem, 90000). assign(warn_mem_max_weight, 10). September 12, 1997. Bug reported by Dale Myers. If the search is stopped before the first given clause is used (for example max_given=0) the would-be first given clause is lost. Ordinarily this doesn't matter, because the search is over. But if you have set(print_lists_at_end), that clause will not appear in the output. Easy fix in file main.c. September 16, 1997. I moved the extra source code for the FormEd program into a subdirectory called formed, which has its own makefile for FormEd. Sept?--Nov?, 1997. Otter now catches the SIGUSR1 signal; when it happens, statistics are sent to the output file, and Otter exits with code 113. The reason for this is so that if you have a long-term Otter jobs that is no longer attached to a login shell (i.e., you started Otter in the background, then logged out, then logged in again), you can kill Otter and get statistics. To kill Otter and get statistics at the end of the output, run "kill -USR1 ". This probably works only under UNIX. ----------- November 1997. Dale Myers (Univ. of HI Math Dept) visited for three weeks, and we installed a splitting rule. Mohammed Almulla (Univ. of Kuwait) was also visiting, and he contributed to the effort. See split.txt in the documentation directory. Splitting uses the UNIX fork() system call, so I doubt it will work as is for Macintosh or Microsoft. The splitting rule required the introduction of a new flag set(back_unit_deletion), which causes any new unit to be used to remove literals from existing clauses. Analogous to back demodulation. This flag should also be useful when not splitting. Also, to make more sense of output files when splitting is used, I changed some of the messages that go to the output file---for example, the first few lines and the last few lines of the output. Also, a new flag BELL (default set). If you clear it, Otter won't ring the bell when important things (like a proof) happen. Requested by Dale Myers. ------------- Feb 19, 1998. Preparing for the release of 3.0.5. I had been planning to make the new auto mode (auto2) the default, but I have changed my mind---the old auto mode (auto1) will be the default. (set(auto) gives the default auto mode.) The reasons: (1) auto1 is closer to being complete, and (2) users will be annoyed if their old auto files don't work with 3.0.5. --------------- Otter 3.0.5 released -- February 19, 1998. ---------------