-------- LADR 2009-11A ---------- November 4, 2009. Online Examples. Somewhere along the line, the XML/XSL/HTML rendering of the tables for interpretations broke in Firefox (ok in Safari, don't know about IE). I suspect it's a Firefox problem, because using xsltproc separately to translate the XML to HTML produces HTML that Firefox renders correctly. This is beyond me. Help? November 3, 2009. Newauto. Oct 1 fix causes big slowdown in fof-prover9 jobs that spawn hundreds of children. Undo that fix and fix it in a different, kludgey way by inserting "flip_matches_hint" into symbol table at start of forking_search. Any other lables that might be introduced by children should be handeled similarly. November 3, 2009. Prover9, Mace4, LADR. Change default max_megs from 200 to 500. This also affects other LADR programs like prooftrans. October 28, 2009. Prover9. Bug appears when using prolog_style_variables with weighting rules: the special symbol "_" in weighting rules is treated as an ordinary variable. Fixed by changing the definition of prolog_style_variables so that they don't include symbols that start with "_". October 1, 2009. Newauto. Bug appears when child search introduces new hint label ("flip_matches_hint"). Fix by changing new_symbols_since_mark() (in ladr/symbols.c) so that *all* new symbols are reported. July 9, 2009. Prover9. Very minor bug: at top of proof, the line "Maximum clause weight" always prints integer, even if floating-point. Fixed. June 29, 2009. Ladr_to_tptp. Bug causes $F ("false" in LADR) to be treated as a constant. Fixed so that it translates to $false ("false" in TPTP). May 22, 2009. Prover9. Bug in production mode when compiled for 64-bit computers. Line 103 in ladr/dollar.c: sizeof(int) should be sizeof(void *). Fixed. April 9-10, 2009. apps.src. New program to generate constant definitions for TRC experiments: gen_trc_defs. LADR: flat demodulation: when clearing substitutions, also check and clear "alternative" field. This fixed a problem caused by nonstandard use of flatterms in new app gen_trc_defs; the change should not affect prover9. March 17, 2009. Interpformat and Isofilter: would crash in some cases when the Mace4 job used op commands to declare print/parse properties. Fixed by introducing "simple_parse" flag in parse.c. This avoids problems when special symbols are used in standard prefix form, e.g., interps in standard form. March 12, 2009. Mace4. Bug (segfault) in some cases when input formula simplifies to $T or to $F. Fixed. February 26, 2009. Prover9. Production mode bug: segfault when doing arithmetic (op_code out of range in rewrite). Fixed. -------- LADR 2009-02A ---------- February 1-24, 2009. Prover9. New "production mode" which uses hyperresolution along with new rewriting system (conditional rewrite rules and ability to rewrite atomic formulas) to do things like forward-chaining state-space searches. See the HTML manual "More Features -> Production Mode". February 19, 2009. Prover9. New parm eval_var_limit (for semantic guidance). This simply changes eval_limit based on the size of the largest interpretation. See the manual. January 25-26, 2009. Prover9. Preliminary work on extending hyperresolution for evaluable antecedents and consequents. January 21, 2009. LADR. The October 21 change of giving "--" built-in parsing property op(500, infix, "--") took away the ability to write terms like --x (without space) using unary minus. I think this important, so I'm rescinding that Oct 21 change. The "--" symbol was used for binary minus in the Mace4 built-in arithmetic, so from now on, we'll have to write, e.g., "x + -y" instead of "x -- y". (Symbols in LADR cannot be overloaded, so we cannot use "-" for both unary negation and binary minus.) LADR has been updated so that it no longer accepts "op" declarations for "--", "---", "----", ... . Also, it no longer accepts declarations for "''", "'''", "'''", ... . These are special-case restrictions so that the prefix operation "-" can be input and output without space for nested occurrences, e.g., "--x = x". Similarly, for postfix operation "'", e.g., "x'' = x". Unfortunately, this change messes up the programs tptp_to_ladr and ladr_to_tptp, because they rely on an operation "--". A kludge gets around the problem. January 20, 2009. Prover9. A new experimental feature was enabled by mistake: assign(complexity, 1). This causes clause weights to get floating-point values by default. It has been disabled. -------- LADR 2009-01A ---------- (unannounced) January 15, 2009. Mace4. Bug (reported bu Peter Jipsen) when using set(skolems_last): it can miss some (nonisomorphic) models. Fixed. Prover9. Minor change requested by Bob Veroff: hints count message. Newauto. Minor change requested by Veroff: change prepend to append. December (mid). Prover9. Complexity function for weighting (preliminary work). assign(complexity,1) breaks ties when selecting given clauses, based on a complexity measure: more complex has lower weight. Not in the manual. December 11, 2008. Mace4. User-declared skolem functions do not work with skolems_last option. Fixed. -------- LADR 2008-11A ---------- November 15, 2008. Mace4. New option set(arithmetic) builds in some integer arithmetic. See the Prover9 HTML manual. November 7, 2008. Mace4. Previously, a domain element out of range would always cause a fatal error, even if higher domain sizes had been specified. Now, it will simply skip the domain size and try the next size. October 26, 2008. Prover9. Bug when action, triggered by kept-clause-count, asserts a clause, e.g., kept = 10 -> assert(-p | a | b). (reported by Ken Kunen). Clause is asserted repeatedly until segfault. Fixed by moving one line of code. I can't understand why that line of code was where it was; if there was a good reason, this fix might cause some other problem. October 23, 2008. LADR. New type of option is accepted: "floatparm". This allows assignment of floating-point values to some of the parameters, e.g., assign(max_weight, "10.2"). Floating-point values must be enclosed in double quotes. Prover9. Floating-point values can be used for the parameters that control weighting: max_weight, variable_weight, constant_weight, not_weight, or_weight, sk_constant_weight, prop_atom_weight, nest_penalty, depth_penalty, var_penalty, default_weight. Integers can still be used for these. Also, weighting rules can have floating-point values (in double quotes) as well as integers. October 23, 2008. Prover9. Parm skolem_penalty has been removed; it was for an experiment, and it never made much sense. October 21, 2008. Mace4. New flag order_domain builds in the relations < and <= (less-than, less-than-or-equal) on the members of the domain (in the same way that the flag integer_ring builds in the operations +,*,- as the ring of integers mod n). Also, when integer_ring is set, the operation "--" is built-in as binary minus. (So you can write x -- y instead of x + -y.) Mace4. Accepts new list, list(distinct) to say that lists of objects are distinct. E.g., list(distinct). [a,b,c]. [d,e]. end_of_list. is shorthand for formulas(assumptions). a!=b. a!=b. b!=c. d!=e. end_of_list. LADR. "--" and "++" get built-in parsing properties: op(500, infix, ["--", "++"]). October 18, 2008. Interpformat. Add option "wrap" which encloses interps in list(interpretations). ... end_of_list. October 10, 2008. Prover9. Change hints matching so that non-orientable equality units are tried both ways when looking for a matching hint. When the flip matches a hint, append a label "flip_matches_hint" to the clause. October 7, 2008. Ladr_to_tptp. Yet more changes. More parentheses output. New command-line options: -p says to output all parentheses. -q says to single-quote unacceptable TPTP symbols, e.g., x*y becomes '*'(x,y) instead of tptp0(x,y). Tptp_to_ladr. New command-line option: -q says to double-quote unacceptable LADR symbols. October 2, 2008. Prover9. Bug: assign(demod_size_limit, -1) is supposed to mean infinity, but it doesn't. It causes demodulation to stop prematurely. While looking at this, we decided that a better parameter would be demod_increase_limit, which would terminate demodulation when the size (symbol count) of the clause increases more than the limit. So demod_size_limit is eliminated, and demod_increase_limit (default 1000) is introduced. Also, the warning messages about demod_step_limit and demod_increase_limit have been improved. -------- LADR 2008-09A ---------- August 30, 2008. LADR. clause_ident failed to check sign when checking identity of literals. Fixed. That routine is used in several places; prooftrans caused the bug to appear (missing hints). August 28, 2008. Changelog. Reverse so that most recent entries are at the beginning. August 27, 2008. Prover9 Manual. It incorrectly said that max_weight=-1 means infinity (no limit). Fixed. August 22, 2008. Prooftrans, Directproof. These failed if the empty clause has an answer attribute with more than 1000 characters (buffer limit, not buffer overrun). Fixed. Prooftrans. Previously, the order of the arguments "expand" and "renumber" was irrelevant; it always expanded first. Now, it does the transformations in the order given on the command line. August 18, 2008. Prover9. Hint degradation: weights were artificially high, because the number of previous matches included clauses that were later forward subsumed. Fixed. Prover9. When generating Skolem functions, allow them to to occur in the hints list. When building up sets of hints by iteration, this change prevents generating new Skolem functions in each search. This involved substantial changes to code in symbol_check_and_declare. The routine accept_list takes an additional argument. August 14, 2008. Prover9. Force evaluation (w.r.t. semantics) just before clauses are "kept". Previously, clauses were evaluated only when needed by keep/delete rules or given-selection rules. The change makes sure false clauses have the "false" label if print_kept prints them. Prover9. Crash if sos is full (sos_limit) and all are high priority (e.g., hints), because a "worst" clause cannot be found. Fix: allow "worst" clauses to be high priority. -------- LADR 2008-08A ---------- (unannounced) August 5, 2008. Prover9: Another incompatibility of lex_order_vars with KBO. For example, with lex_order_vars, m(x,y,z) < m(z,y,x), but NOT m(x',y,z') < m(z',y,x'), because, although x and z are comparable, but x' and z' are not. A patch: when trying to compare f(alpha) and f(beta), go right to comparing alpha and beta, rather than checking the variable condition. This fixes this particular problem, but there may be similar ones lurking. (The change applies also without lex_order_vars, but it should not change the behavior in that that case.) Tptp_to_ladr: stupid inefficiency in list processing causes inputs with many formulas to take a very long time. Fixed. -------- LADR 2008-07A ---------- (unannounced) July 9, 2008. All code: get rid of variable declarations that are not at the beginning of a block. (To satisfy old compilers.) -------- LADR 2008-06A ---------- June 23, 2008. Prover9. Produce more output during preprocessing. Previously, in the section "CLAUSES FOR SEARCH", there could be justifications like [back_rewrite(9),rewrite([11(3)])], with clauses 9 and 11 not appearing before that point, because they had already been disabled, e.g., by back rewriting. Now, most clauses that get IDs during preprocessing are output (if print_initial_clauses is set). June 21, 2008. LADR (ladr_to_tptp and tptp_to_ladr). The May 14 changes caused a problem: operations of different parse types with the same precedence: declare_parse_type("|", 502, INFIX_RIGHT); declare_parse_type("~|", 502, INFIX); declare_parse_type("&", 503, INFIX_RIGHT); declare_parse_type("~&", 503, INFIX); This is not allowed in LADR. Solution: don't support ~| or ~&. June 12, 2008. Prover9. Remove the May 18 weighting code (too slow and broken). New code: allow a user/programmer to write weighting functions in C, and then refer to the new function, say func42, in weighting rules like this: weight(f(x,y) = call(func42,x) + weight(y). See the new source file ladr/weight2.c. Prover9. Suppress selector_report in "Low Water" messages, unless assign(stats, all). Prover9. Bug with assign(sos_limit, -1). (E.g., clear(auto_limits)). -1 is supposed to mean infinity, but Prover9 was interpreting is as a small limit, causing sos_empty. Fixed. June 11, 2008. Prover9. Bug reported by Michael Beeson. Unit deletion, in which the unit contains an answer attribute with variables: variables do not get instantiated. Fixed. Prover9. Another (minor) answer literal bug: When a proof has answers, a message containing the answer goes to stderr and at the start of the proof. When there were multiple answers, only the first was printed. (The empty clause at the end of the proof correctly printed all answers.) Fixed. May 18, 2008. Prover9. Experiment to allow weighting function to call an external program to compute the weight. Works on Mac (very slowly), fails in linux (system call popen() works differently.) -------- LADR 2008-05B ---------- May 15, 2008. Prooftrans. Added Bob Veroff's "tagged" output format. This involved some new code in ladr/{just.c,ioutil.c}. May 14, 2008. LADR (ladr_to_tptp and tptp_to_ladr). Several changes (from Geoff Sutcliffe) on parse/print declarations: "=>" and several other TPTP operations changed from INFIX_RIGHT (xfy) to INFIX (xfx). -------- LADR 2008-05A ---------- May 7, 2008. Prover9. The weighting rules now can include a vars(term) operation, which is the number of (distinct) variables in the term. This is analogous to the depth(term) operation. Prover9. The SELECTOR REPORT is printed only with assign(stats,all). Prover9. When a kept clause does not match any given_selection rules, a warning is printed (previously, it caused a fatal error). Fof-prover9. Efficiency bug when there are many (>50) subproblems having to do with new symbols. Fixed by considering function/relation symbols only. April 23, 2008. Prover9. Bug in new given_selection code: "positive" is true if any positive literals. Same for "negative". Fixed. This bug also affected list(keep) and list(delete). April 14, 2008. Expand_proof bug (called by prooftrans, directproof) occurs for assert-by-action with immediate simplification. It was producing justifications like [assumption,rewrite...]. Expand_proof could not handle it. Instead of fixing expand_proof, the assertion was changed so that if it is immediately simplified, a "copy" inference is inserted. The reason: [assumption,rewrite...] in a proof is bad, because you don't see what the actual assumption is. April 13, 2008. Directproof. Bug causes coredump. Trivial case not handled: flip negative equality, then implicit resolution with x=x. Fixed. -------- LADR 2008-04A ---------- March 24--28, 2008. LADR. New language to specify clauses by various properties. For example, "weight < 40 & (horn | variables = 3)". This will be used for deciding which clauses to keep and for selecting given clauses. See next paragraph. Prover9. Use the new language in three ways: (1) list(keep). end_of_list. (2) list(delete). end_of_list. (3) list(given_selection). ... end_of_list. See the HTML manual (new sections "Advanced Features"). list(delete) is a generalization of max_weight, max_vars, etc. list(given_selection) is a generalization of weight_part, age_part,etc. Max_weight, weight_part, etc. will still be accepted, but those operations will now be implemented by the new mechanisms. These are big changes to Prover9, and there are probably some bugs. The way sos_limit works has been changed. It has always been an ad hoc heuristic, and it still is, but it is now simpler. Warning: searches that use sos_limit *will* behave differently in the new Prover9. The new parm sos_keep_factor adjusts how sos_limit works. New naming convention for releases. March 21, 2008. Prover9. Minor bug involving lex_order_vars and hints. Fix: renumber variables in hints, just after orienting and before indexing (also for back-demodulated hints). -------- LADR March-2008A ---------- (unannounced release) February 28, 2008. Prover9. Bug involving hints with sos_limit. Clauses matching hints (i.e., really good clauses) were being deleted by sos_limit to make room for clauses that might not be as good. Also, this bug can cause clauses to be inferred, kept, deleted, inferred, kept, deleted, ... . Fixed. February 19, 2008. Tptp_to_ladr. The Feb 14 precedence change (~) was no good. After discussion with Geoff and Josef, we decided that the previous precedences were okay, so undo the Feb 14 change. -------- LADR Feb-2008B ---------- (unannounced release) February 15, 2008. LADR. Give a better error message (and catch the error sooner) if variables are used as atomic formulae, e.g., xor(x,y) <-> ((x & -y) | (-x & y)) February 14, 2008. Clausefilter. Accept new command-line option "ignore_nonevaluable" which says to skip evaluations when the formula contains symbols not in the interpretation. Tptp_to_ladr. Change precedence of ~ (TPTP spec changed). February 8, 2008. Prover9. Fix default_parts bug (clearing does nothing) introduced on Jan 29. -------- LADR Feb-2008 ---------- (unannounced release) February 4, 2008. Prover9. New action "assert(some_clause)" causes the clause to be generated and processed when the action is triggered, e.g., list(actions). given=100 -> assert(x*y=y*x). end_of_list. This does not work for non-clausal formulas. February 4, 2008. Prover9. Minor bug: failed to renumber variables after one kind of simplification (removing literal s!=t when s & t unify and do not instantiate any other literal). This causes a problem only when expanding a proof internally (e.g., newauto). Fixed. January 29, 2008. Directproof. Fix bug that caused it to fail if the unit conflict involves a flip. January 29, 2008. Prover9/LADR. Change options processing a bit so that options in the GUI make more sense. Introduce a new kind of options dependency that resets options to defaults. Several meta-options (lightest_first, breadth_first, random_given, auto2, raw) did nothing when cleared. This is okay for Prover9, but not for the GUI, which displays current values of options. -------- LADR Jan-2008 ---------- (unannounced release) January 25, 2008. Prover9. Two new flags for paramodulation: para_into_vars (paramodulate into variables) and para_from_small (paramodulate from smaller sides of oriented equalities). These are not needed for finding refutations, but they can be useful for *deriving* interesting things (fishing expeditions) and for transforming a bidirectional proof into a forward proof. Use with caution. January 23, 2008. Prooftrans. Some answer attributes were not being inherited in translated proofs. Fixed by declaring answer attributes to be inheritable. -------- LADR Dec-2007 ---------- December 12, 2007. Prover9. New flag "raw", which is a sort of anti-auto mode. This removes restrictions on inference rules and other limits on the search, allowing users to start from scratch and roll their own strategies. To see exactly what it does, set(raw) and look at the output. December 9, 2007. Mace4. New stringparm "iterate" takes values in [all, evens, odds, primes, nonprimes]. "all" is default. E.g., assign(iterate, odds). This supersedes set(iterate_primes) and set(iterate_nonprimes), and those two flags become meta-options which just assign to "iterate". December 5, 2007. New program isofilter2, which uses a different algorithm: canonicalize the interps so that isomorphic iff identical. It also accepts a file of discriminators to cut down the number of permutations. Results are mixed. Isofilter (the original version). Add new option specifying a file of discriminator clauses. Results are good. Dprofile: new program to see how discriminators behave. December 4, 2007. Prover9. Allow restrict_denials to be used for non-Horn sets. It usually doesn't make much sense for non-Horn sets (because negative clauses usually don't correspond to the conclusion), so let the user beware. December 3, 2007. Prooftrans. Get rid of multiple "Comments from original proof" messages. These occurred when running prooftrans on the output of a previous prooftrans job. Prover9. New parm: assign(multiple_interps, false_in_some). Default is false_in_all, which is the previous behavior. If there are multiple interpretations, this parm determines how a clause is labeled "false": false in some of the interps or false in all of the interps. Mace4. Bug calculating the maximum domain element in the input: it was always >=0; it should be -1 when there are none. This caused some extra isomorphic models to be produced in some cases. November 19, 2007. Prover9. New parameter backsub_check (default 500) tells Prover9, when it reaches the specified number of given clauses, to disable back subsumption if the percentage of kept clauses that have been back subsumed is less than 5%. Previously, this test was wired in (at 500 given clauses), so behavior will be the same with the default value. ladr_to_tptp. Four changes: (1) a <-> b translated correctly. (2) Attributes on all formulas simply deleted. (3) TPTP symbols that are different from the corresponding LADR symbols (e..g, <=) can now be used as ordinary function or predicate symbols in the LADR formulas; they are given new names. (4) Clausal (CNF) goals are made into non-clausal (FOF) goals. Isofilter. New command-line option "output" tells which operations to output. Syntax is the same as the "check" option. Although "check" and "output" will frequently be used together with the same operations, e.g., isofilter check '*' output '*', they are independent. Also, change ignore_constants option so that constants are neither checked nor output. October 22, 2007. Mace4. Undo the Oct 7 change to domain_size dependency, and change how domain sizes are specified: start_size (new parm, default 2) end_size (new parm, default -1 (infinity)) domain_size (meta: copy value to start_size and end_size) We'll keep iterate_up_to for a while, and make it a synonym for end_size. That way, input (before Oct-2007) should behave well. Note that that default end_size (iterate_up_to) is -1, not 10. Mace4. New flag iterate_nonprimes (analogous to iterate_primes). Mace4. There was an (arbitrary, I think) limit of 200 on the domain size. I have removed this. October 18, 2007. Prover9. While working on adding the notion of dependent option to the GUI, I decided that the dependent options in Prover9 should be simplified. From now on, options that update other options will be called meta options, and the only thing they do will be to update other options (there might be a few exceptions). The changes: 1. New flag auto_setup, whose role is to change eq_defs and predicate_elim (previously controlled by auto_inference. auto_setup is dependent on auto. 2. The back_unit_deletion flag has been removed. Now, there is just 'unit_deletion', and back unit deletion is always done when unit_deletion is set. 3. Back demodulation is set by default. 4. The flag positive_inference has been removed. (Positive inference happens by default, because literal_selection is max_negative by default. LADR. New flag ignore_option_dependences. If set, dependencies on options will be ignore during input. Dependencies will be enabled after input, because options can change after input (e.g., auto_inference, actions). This flag will be used by the GUI, because the GUI will be handling dependencies. -------- LADR Oct-2007 ---------- October 7, 2007. Mace4. Remove option dependency: domain_size=n -> iterate_up_to=0. Now, if you want to search only one domain size, you'll have to assign to both domain_size and iterate_up_to (to a value <= domain_size). Prover9: Change literal_selection option value: maximal_negative -> max_negative. October 6, 2007. Prooftrans and Interpformat: change exit codes. 0: at least one proof/model processed. 2: no proof/model processed. 1: error. October 4, 2007. Prover9 and Mace4: new flag assign(report_stderr, ) sends "some" statistics to stderr every n seconds and at the end. This is for the GUI "Info" button. October 3, 2007. Interpformat: There is now a default format: "standard2". (Previously a format had to be given.) Mace4: Change flag names: print_models to print_models_tabular, print_models_standard to print_models. Mace4: Do not print === MODEL === for print_models_tabular, because interpformat cannot handle it. September 25, 2007. Mace4: Change max_seconds and max_seconds_per so that -1 means infinity. (For consistency with Prover9 options.) Update Mace4 HTML manual with these changes. September 24, 2007. LADR: Added primitive conditional inclusion for input. The only conditions so far are "Prover9" and "Mace4". if(Prover9). assign(max_given, 100). end_if. if(Mace4). assign(domain_size, 5). end_if. The conditions can be nested (though I don't see how that would be useful so far). September 18, 2007. LADR: Change error messages for syntax errors and some other input errors such as unrecognized options. Mark the beginning of error as well as the end. This is so that errors can be highlighted in the GUI. Also fix 2 parsing bugs: 'f(.' and '[.' were crashing. -------- LADR Aug-2007 ---------- August 3, 2007. Interpformat, Mace4. Change the name of the interpretation format "portable" to "standard". This is the format that LADR programs use. This change was made so we could use "portable" for the following. Interpformat. Introduce a new output format "portable" to be used for input to Python, GAP (and possibly Java and Javascript). The new portable format is similar in structure to "standard", but it is made up of natural numbers, double-quoted strings, and lists. See the manual page "Interpformat". July 18, 2007. Prover9. Handling of redundant hints has been improved w.r.t. labels and bsub_hint_wt attributes. Bsub_hint_wt attributes on redundant (equivalent) hints are copied to the original (retained) hint. If a hints ends up with more than one bsub_hint_wt attribute, the first is used. When searching for matching hints, if an equivalent hint is available, it is used; otherwise the first subsumee is used. June 30, 2007. LADR. New language feature: allow the user to redefine several built-in operations such as equality, disjunction, attribute. For example, redeclare(equality, "=="). redeclare(negated_equality, "=/="). redeclare(disjunction, "&&"). The redeclarable operations are: true, false, conjunction, disjunction, negation, implication, backward_implication, equivalence, universal_quantification, existential_quantification, attribute, equality, negated_equality. Note: When a redeclaration occurs, the parsing/printing properties (infix, precedence, etc.) are copied from the old symbol to the new one. June 18, 2007. Prover9. New flag limit_hint_matchers (default clear). Setting the flag causes max_{weight,literals,vars,depth} to be applied to clauses that match hints. -------- LADR June-2007 ---------- June 14, 2007. LADR: Change printing of variables (standard style) to x,y,z,u,w,v5,v6,v7,... . (That is, don't use "v".) This avoids confusing terms like (v v v), because "v" is commonly used as the lattice join operation. June 13, 2007. Prooftrans: fix the "proliferating ops problem", add option striplabels, and append labels to hints only if asked to do so. See the updated HTML manual. June 12, 2007. Prover9: Disabled rule pos_binary_resolution. The parameter literal_selection (maximal_negative) will be used to do positive binary resolution (and positive paramodulation). The reason: before the change, we could have pos_binary_resolution without positive paramodulation, which blocks proofs. Change breadth_first "Starting on level" messages so they don't appear if some other part has been set. June 4, 2007. Newauto, newsax, autosketches (non-documented experimental programs): updates for expand_relational_defs broke these programs. Fixed by including call to embed_formulas_in_topforms. -------- LADR May-2007 ---------- May 21-23, 2007. Prover9: Added flag set(expand_relational_defs) (default clear), which causes Prover9 to look for relational definitions in the assumptions, and use them to expand all occurrences of the defined relation in the input, before the start of the search. See the HTML manual, page "More Prep". May 6-11, 2007. Prover9: *MAJOR* changes to binary resolution and paramodulation for non-unit clauses. The goal is improved performance for non-unit, especially non-Horn, problems. There are several changes in flags and parameters. See the Prover9 HTML manual page "Inference Rules". An unfortunate consequence of these changes is that paramodulation for (unit) equational problems can behave differently from previous versions, because paramodulants can be derived in a different order, causing given clauses to be selected in a different order. May 9, 2007. Change default predicate symbol precedence so that equality is the smallest instead of the largest. In problems with both equality and non-equality predicates, this change usually causes resolution to occur before paramodulation. May 8, 2007. Separate the lex([...]) command into two commands: function_order([...]) and predicate_order([...]). (The old lex([...]) command will continue to be accepted, and it is now a synonym for function_order([...]).) May 8, 2007. Bob Veroff reminded me that the parsing code can accept ambiguous terms, for example, if ~ is prefix and ' is postfix with the same precedence, the term (~ x ') is accepted. (Prolog systems (all Prologs??) have the same problem.) Fix: do not allow declarations of two different symbols with different parse types and the same precedence. This applies also to built-in declarations, so the error may be confusing. Also change built-in precedence of op(400, prefix, -) to op(350, prefix, -), because people tend to use 400 for infix ops. April 19, 2007. Prover9, minor bug: If predicates were eliminated in preprocessing, they were still listed in the symbol precedence for the search (at the top of the order). Fixed. April 18-19, 2007. Ken Kunen reminded me that Prover9 doesn't paramodulate from variables, making it incomplete when there are (positive) equality literals t=x in which variable x does not occur in term t. A new flag: para_from_vars (default set). Note that this is almost always irrelevant for purely equational (unit) problems. April 16, 2007. prooftrans: bug reading proofs containing justifications with more than 256 rewrites. There is a hard limit of 256 on the arity of symbols. Fix: change format of rewrite justifications from "rewrite(step1,step2, ...)" to "rewrite([step1,step2, ...])". After the fix, you can use the new prooftrans prooftrans only with new prover9 outputs, and old prooftrans only with old prover9 outputs. Related: check for arity-too-big when building terms. April 16, 2007. LADR: yet another parsing bug. Terms like "h(v) * (x + y)" (assuming v is infix (the default)) are parsed incorrectly (parser thinks v is binary and * is unary. Fixed. -------- LADR April-2007 ---------- April 12, 2007. Mace4: fixed 2 bugs in signal handling. Apps.src: updated clausefilter, clausetester, interpfilter so that they work for non-clausal formulas as well as clauses. April 9, 2007. Prooftrans bug: fatal error expanding new_constant inference with secondary justification. Fixed. April 6, 2007. Prover9, added parm var_penalty, which can be used to penalize clauses by the number of (distinct) variables. At the end of the weighing process, the weight is increased by n * number_of_variables. N can be negative, which lowers the weight. Update manual. April 5, 2007. Prover9, Bugs: max_depth, max_vars, max_literals can delete clauses that match hints. Also, sos_keep can delete clauses that match hints. These were fixed by reorganizing the cl_process_delete code. April 3, 2007. Isofilter: very slow memory leak. Fixed (zap_interp failed to free comments). April 2, 2007. Prover9, new flags and parms for selecting the given clause: parm random_part: picks random clauses from sos; flag random_given: random_part=1, other parts (except hints) 0; parm random_seed: (-1 means use "random seed"); flag default_parts: clearing sets ALL parts to 0. -------- LADR March-2007 ---------- March 16, 2007. Two new utilities to support the TPTP language: ladr_to_tptp: Prover9 input file -> TPTP problem file. tptp_to_ladr: TPTP problem file -> Prover9/Mace4 formulas. These are still in development and do not yet support all of the TPTP features. Eventually, Prover9 and Mace4 will accept the TPTP language directly. March 15, 2007. Prover9: insert several fflush() so that output is better behaved when stderr is sent to the same file as stdout. March 12, 2007. Prover9: new parms max_depth and depth_penalty. Prover9: new command-line option -p causes all output to be fully parenthesized. This is mostly to check and debug parsing declarations (op commands). March 7, 2007. LADR: Bug in clausify_prepare causes result of Skolemization to be more complex than necessary. Fixed. Prover9: max_megs limit caused fatal error if it occurred in CNF translation (before search). Fixed. LADR: Several substantial changes to basic parsing of terms: 1. Previously, some legal terms were rejected. For example, if you have a binary infix op, say *, and you use it as a unary op, and write it in standard form, say p(*(x)), it would be rejected. (Input cannot have a symbol with multiple arities, but if it is declared, but not used, that does not count.) Several cases like this have been fixed, but there may still be related problems. 2. Parsing/printing of quantified formulas has been changed. Previously, "p | all x q | r" would be rejected. Now it is accepted with association "p | (all x q) | r". Also, fewer parentheses are output for quantified formulas. Quantifiers have lower precedence (bind tighter) than other logic operations, so "all x p -> q" means "(all x p) -> q". When in doubt, include parentheses and look at the output. March 5, 2007. Bug in manual (Clauses and Formulas section): the "cons" operator is shown as "|" (as in Prolog), but it is really ":". Fixed. February 27, 2007. Prooftrans (from Kinyon): bug with options "expand renumber". The transformed proof can have strage IDs, e.g., 27A. Fixed. February 12, 2007. Prover9 bug: KBO and fold_eq, in a problem with exactly one unary operation, that happens to be an equational definition. Fold_eq can arrange the precedence in a way that violates the KBO rules, causing non-termination. Fix: do not change precedence of special unary op (such symbol is still folded). January 30, 2007 Updated the Mace4 pages of the (HTML) Prover9 Manual. Previously the Mace4 pages were cursory, with reference to the out-of-date (2003) tech memo. Now the HTML version is reasonably complete. January 26, 2007 Hints are now back demodulated (as in Otter). January 22-25, 2007 Prover9: Major overhaul of the given clause selection code. A new source file prover9.src/picker.c was introduced; the files ladr/sos.c and prover9.src/control_sos.c are now gone. BEWARE: YOU WILL NOTICE A DIFFERENCE. Even with the same input, given clauses will probably be selected in a different order from previous versions, resulting in different searches. There is no way to opt for the old method. The main difference has to do with the selection ratio. Previously, if a clause of a particular type was not available, another type could be substituted. Now, if none is available, that type is skipped. Because of this change, the default values of true_part and false_part have been changed from 2 to 4. Also, there is a new parameter "weight_part", which is used for basic selection-by-weight. (Previously, true_part and false_part were used in a round-about way for simple selection-by-eight.) There is a new (meta-)flag "lightest_first", which sets weight_part=1 and all other parts to 0 (except hints_part). Also, "pick_given_ratio" now sets weight_part=n, age_part=1, true_part=false_part=0. Selection by Hints: Previously clauses that matched hints were given preference simply by adjusting their weights. Now, clauses that match hints have their own component of the selection ratio: "hints_part", with default value infinity, and those clauses now get ordinary weights. In summary, the components of the selection ratio are (with defaults): age_part 1 true_part 4 false_part 4 weight_part 0 hints_part INT_MAX Other "_part"s may be added in the future. The manual has been updated to reflect all of these changes. January 24, 2007 Prover9 bug: answer attributes not instantiated for the "xx" (resolve with x=x) simplification rule. The first version of this rule simply removed instances of x!=x, so answer attributes didn't have to be instantiated. However, the rule was changed so that it removes s!=t, when s and t are unifiable without instantiating any other literals in the clause. When I made the change, I overlooked the fact that it can instantiate answer attributes. Fixed. --------- LADR-Jan-2007 ---------- January 4, 2007 December 11, 2006 Isofilter: A new option to specify exactly the symbols to be used for the isomorphism checks. (Sort of a generalization of "ignore_constants".) It is given on the command line, e.g., the command "isofilter check '+ *'" says to consider only those two operations (any other operations are still printed in the results). If there is more than one operation, or if some of the operations might be interpreted by the shell, include single quotes as in the example. This was prompted by Joao Araujo. December 8, 2006 Improve warning messages for symbols missing from lex command and extra symbols in lex command. December 5, 2006 Prover9 (bug reported by Sebastian Sonntag): Predicate elimination changes the basic clause properties so auto_denials gets the wrong count of number of negative clauses. Fix: move basic_clause_properties() after predicate elimination. December 3, 2006 Prooftrans: change heading on "prooftrans ivy" output. --------- LADR-November-2006 ---------- November 22, 2006 Remove index-test directory (because it's 4MB). November 21, 2006 Prover9 bug (Kinyon): Multiple proofs of the same denial when reuse_denials was clear. This was caused by negative_clause call on compressed disabled clauses. Fix: put yet another flag (negative compressed) in Topform. --------- LADR-October-2006 ---------- October 24, 2006. ladr: read_term_list(), in ladr/ioutil.c, is very slow when reading big lists because of a silly inefficiency. Fixed. Include index-test. This is a test program for a project of Michael Kohlhase. See index-test/jobs/README. October 16, 2006. ladr: If the % character that starts an ordinary comment is the last character on a line, then the following line is ignored. (I got the operator precedence wrong in an expression a = b == c). Fixed. September 14, 2006. Prover9: minor bug fixed: do not check max_literals or max_vars for restricted denials. --------- LADR-September-2006 ---------- September 13, 2006. Prover9: Change the way restrict_denials is implemented. Previously, restricted denials would get weight=0 and go into sos, so they would not be deleted by max_weight and they would be selected right away as given clauses. That caused an annoyance: adding or taking away a denial could changed the search, because sequence of given clauses would change. The fix: restricted denials now go directly into usable (e.g., when back demodulated), bypassing sos. Also, the ordinary weighting function is applied to them, but they are NOT deleted if heavier than max_weight. August 31, 2006. Prover9: Rolf Schwitter reminded me that answer attributes do not work correctly for non-clausal formulas. Solution: (1) Do not allow proper subformulas of non-clausal formulas to have any attributes. (2) Do not allow answer attributes on non-clausal formulas to have variables. Update the manual. Answer attributes with variables do make sense for formulas and subformulas in some cases, and we might accept them some day. One of the problems is that the attribute operator # is not good enough for arbitrary formulas, because we need to know whether it acts as conjunction or as disjunction. August 29, 2006. ladr: Change printing of XML proofs (prooftrans), adding a "type" attribute: . The types (so far) are goal, assumption, deny, clausify. Also change proof3.dtd and proof3.xsl so that the different types are displayed differently. August 28, 2006. Prover9: Give goal formulas the attribute "label(goal)". These formulas appear in proofs, and the label is to emphasize that these formulas have not been negated and will not be used for inferences. August 25, 2006. Prover9: Changed warning message for shared constants in denials so that it simply prints the shared constants instead of all of the pairs of clauses that share constants. Prover9: I think that sos_limit is too aggressive in deleting clauses, so I'm changing the default from 10,000 to 20,000. Also, the point at which prover9 starts being more selective about keeping clauses was changed from .5 to .9 (fullness of sos). As always, experts may wish to clear(auto_limits). August 23, 2006. Prover9: Fix variable declaration in prover9.src/prover9.c. Mace4: Fix formatting in mace4.src/print.c. Updated SOBB-II to use LADR-August-2006A. --------- LADR-August-2006A ---------- August 11, 2006. Mace4: Change the default value of "iterate_up_to" from 0 to 10, and introduce an option dependency: if "domain_size" is changed, change "iterate_up_to" to 0. If iterate_up_to is changed, it all behaves as before. These changes were made so that if no options are given (in the input file or on the command line), then it will start at domain_size=2, and iterate up to 10. Previously, it would try 2 and then terminate. August 8, 2006. Prover9, semantic guidance. If there is more than one interpretation, a clause is marked "false" if it is false in ALL (previously SOME) interpretations. The reason: In experiments, I found that I wanted fewer false clauses. August 1, 2006. Prover9: print_gen -> print_kept. Also improve print_gen messages. Prover9/LADR: change CAC redundancy so that (xy)z=x(yz) and x(yz)=y(xz) are both kept. Implement back CAC simplification. July 31, 2006. Bug: did not accept negative integer attributes. Fixed. July 30--31, 2006. Reorganize include structure in ladr/ and prover9.src/. July 25, 2006. Mace4: Prolog_style_variables specified on the command line (-V1) does not work. (I'm not sure when it broke.) Fix by simply not accepting -V1. June 27 -- July ??, 2006 (just after ADAM-2006) MAJOR CHANGES, in 3 groups. Not everything is detailed here, so see the HTML manual. LADR: Change parsing/printing so that less space is required around prefix and postfix ops. The important difference is that prefix "-" and postfix "'" need not have space, e.g., "---p'''" will be parsed as unary operations. The downside: If you wish to use a new multicharacter "special symbol", you must give an "op" command that has quotes around the symbol, e.g., op(400, infix, "--->"). The "clear" parse type has been renamed "ordinary", and it can be given in an op command without the precedence argument, e.g., op(ordinary, "###"). LADR: "Formulas" can now have free variables, so Clauses are now formulas. Prover9 (also Mace4) decides which formulas are not clauses and clausifies them. clauses(...) is no longer accepted --- everything goes into formulas(...). Also, non-clausal and "goal" formulas appear in proofs. Prover9: The flags restrict_denials, reuse_denials, and auto_denials have changed. For Horn sets, when reuse_denials is clear, and when searching for multiple proofs: when a proof is found, the first negative clause in the proof, and all of its descendants, are disabled. This allows multiple proofs, without redundant proofs, when restrict_denials is clear. Less major changes. Prover9: new flag "bell", default set. LADR: Change start of block comment from %START to %BEGIN. Prover9: flag fof_reduction is gone. There is a new program fof-prover9. --------- LADR-June-2006C ---------- June 17, 2006 Prover9: change input list name terms(kb_weights) to terms(kbo_weights). Prover9: parameters true_part and false_part are now changable by actions. Also fix some of the other changable options. LADR: parsing routines accept comment-blocks, delimited by %START and END%. (Ok if there's no END%.) See the manual. Jun 16, 2006 Prover9: disable internal flag no_fapl. This is rarely used and I think it might cause some problems. Substantial changes to Prover9: Reorganized auto flags and introduced a few secondary auto flags: auto_denials and auto_process. (See the manual.) Auto_denials (default set): if a Horn set has more than one negative clause, max_proofs is set to the the number of negative clauses (which in turn sets restrict_denials). This is questionable, because restrict_denials can substantially alter the search. This will likely change after some more thought. --------- LADR-June-2006B---------- Jun 9, 2006 Prover9: add selection code (I,A,T,F), meaning (Input, Age, True, False) to printing of given clauses. Jun 5, 2006. LADR: Reorganized and changed names of some of the resolution and paramodulation options: ordered_inference and ordered_instance are replaced with separate options for resolution and paramodulation. --------- LADR-June-2006A---------- Jun 2, 2006. LADR bug from Veroff. Fatal error if more than 2^15 different function symbols. (It happens with prooftrans, because justifications are parsed as ordinary terms.) Overflow check was broken. Changed term structure to allow 2^31 different function symbols and fixed overflow check. May 30, 2006. Changed default eval_limit from 1000 to 1024. May 29, 2006. Two weighting bugs introduced in May 2 change: minus and depth. Fixed. --------- LADR-May-2006B---------- May 25, 2006. Change Demod_limit messages if there are a lot of them. May 25, 2006. Bugs found by Veroff. 1. "Fatal error: xx_simp2, bad literal." xproofs did not handle x!=c. 2. "Fatal error: expand step, result is not identical" Unit deletion failed to mark clause vars "nonnormal". 3. search.c: "if (Opt->dont_flip_input)" forgot flag(). This gets rid of "WARNING: orient_equalities, backward eq2:x = 1" and might change behavior, because lits now get flipped. 4. max_megs_exit caused longjmp fatal exit. Fixed. --------- LADR-May-2006A---------- May 24, 2006. May 20, 2006. Prover9: When new_constants introduced in the presence of interpretations, update interps. May 17, 2006. Prover9: new parms max_minutes, max_hours, max_days; these just change max_seconds. May 15, 2006. New option dependency: assign(max_proofs, n) -> set(restrict_denials). This is a highly questionable change, because (1) you get a proof with one goal, (2) you add a goal and set max_proofs=2, (3) now you might get NO PROOFS, because restrict_denials is now in effect. May 2, 2006. LADR: change weighting, making rules more verbose, with cleaner semantics. For example, Old rule: f(a,x) = x + 2. New rule: weight(f(a,x)) = weight(x) + 2. Apr 24, 2006. Prover9: fiddle with options fold/unfold. Apr 21, 2006. Prover9: Restrict clauses(goals) so that all must be positive units. Restrict formulas(goals) to at most one formula. Apr 17, 2006. Prover9: Make set(auto) the default (undo with clear(auto).) Remove command-line option -a (auto). Remove lrs_seconds. (Keep lrs_ticks.) Change limit parms so that -1 represents infinity. --------- LADR-Apr-2006A---------- Apr 17, 2006. LADR parsing bug (Veroff). If user has an op command for a symbol that has a built-in op declaration, the built-in should be disabled. Fixed. Apr 11, 2006. Prover9: Fix a few bugs that come up with clear(process_initial_sos). (1) $F in input or produced by predicate elimination; (2) p & - p didn't trigger any inference rules in auto_inference(). (There are so few cases in which clear(process_initial_sos) should be used that I would like to remove it. This would simplify things and allow more peace of mind.) Apr 5--10, 2006. Prooftrans: add ability to produce Ivy-style proof objects (which can be checked with Ivy). This took much longer than expected, but I think it is much more robust than Otter's build_proof_object2. Mar 29, 2006. Prover9: rename flag casc_2005 to auto2. Move set(fof_reduction) and assign(new_constants, 1) from auto to auto2. With these changes, auto2 should behave about the same as casc_2005 before these changes. (However, so many changes have been made to Prover9 since the CASC-2005 contest that even with auto2, the current version will probably behave differently on the 2005 contest problems.) Mar 23, 2006. Prover9: change default demod_size_limit from 500 to 1000. Mace4: change default to set(print_models_portable). Mar 20, 2006. Rewrite prooftrans and interpformat. Change Interp data structure to include comment term, and make the portable format like this: interpretation( size, list-of-comments, list-of-ops ). Mar 17, 2006. Reformat output files for Prover9 and Mace4. This separates the output files into well-defined sections (input, proof, model, statistics, etc.). Mar 13, 2006. apps.src/modelformat. Added xml option to output interpretations in xml. Added -f option. Mar 6, 2006. apps.src/prooftrans. Added xml option to output proofs in xml. Mar 3, 2007. Reorganize command-line options. Now accepted: -h help -a auto (like set(auto) as first line of input) -x casc_2005 (special-purpose auto) -t max_seconds (overrides ordinary input) -f files to read instead of stdin (clauses, etc.) More command-line options may be added, but the primary location for options will remain in the ordinary input. Feb 28, 2006. Bug in prooftrans (Veroff) reading justification with hyper xx. Fixed. --------- LADR-Feb-2006A---------- Feb 7, 2006. Changed the way dates and versions are included in source files. Changed names of parms (OK MK): weight1_part -> true_part, weight2_part -> false_part. (These, together with age_part, specify the given clause selection ratio, oldest : false-in-some-interp : true-in-interps.) Jan 23, 2006. Incompleteness bug from Ilya Mezhirov: input clause f(x) != f(a). does not give a refutation. Fixed simplify_literals2() in ladr/subsume.c so that it removes literals like that (if the instantiated vars do not occur elsewhere in the clause). Jan 12, 2006 Bug (fatal_error) in fof_reduction (reported by Ilya Mezhirov). Changed balanced_binary so that non-AND/OR is ok. Jan 6, 2006 Get rid of clauses(denials). Instead, introduce the flag set(restrict_denials). This flag says to move negative clauses from sos to the internal denials list. From then on, the behavior is the same as before. This change was made so that "goal" clauses can be "denials". The downside: it's an all-or-nothing option; before you could select which clauses go into "denials". Remove the dollar from Skolem constants and functions. I did this because we're using them more often (goals list), and the dollars are annoying to look at. Jan 4, 2006 Prover9 and Mace4: Changed "goals" list yet again. Goals can be either clauses or formulas. If clauses, they are made into formulas by universal closure. Each is then negated and clausified, and the clauses are appended to sos. For Prover9, this means that if ANY goal is proved, a proof is given. For Mace4, models must falsify ALL goals. Note that if there are multiple nonatomic goals, the semantics are nonintuitive and might not what you expect, because a proof can involve parts of different goals. If this is not clear, you can easily do without "goals" by putting an appropriate formula into formulas(sos). --------- LADR-Dec-2005A---------- Dec 16, 2005 Mace4: changed "verbose" flag so that it prints the clauses (once) and the cell selection order (for each domain size) before the search starts. Dec 13-14, 2005. Reorganize ladr/symbols.c (it's still a hodgepodge), especially the symbol precedence routines. Precedence for Prover9 should be the same as before, but it might be different for Mace4. In Mace4, the cell ordering can be different, giving different searches (compared to the old Mace4), but (so far), differences have been minor. Accept new input: skolem([a,b,f]), which declares symbols to be Skolem constants or functions, so that they behave like real Skolem constants/function w.r.t. options, etc.. The form is just like the lex command. This is in read_from_file, so it applies to both Prover9 and Mace4. Mace4: New flag set(skolems_last) does two things. (1) it changes the order in which cells are filled in (Skolems last), and (2) prevents multiple models in which only the Skolem functions change. I was hoping that this would reduce the number of isomorphic models (ignoring Skolems), but the experimental results are not good: It can reduce the number of isomorphic models, but it seems to take much longer to find models. Dec 8-19, 2005. Semantic guidance. Accept list of interpretations and use them to help select the given clause. Changed parms (weight_part, weight_neg_part) to (weight1_part,weight2_part). Weight1_part applies to clauses TRUE in all interps, weight2_part applies to clauses FALSE in at least one interp. If there are no interps, the default interp is "all atoms true". This is consistent with the old meanings of the parms (weight_part, weight_neg_part), because, with the default interp, nonnegative clauses are TRUE, and neg clauses are FALSE. New parm: eval_limit (default 1000). If the clause to be evaluated has V variables, and the largest interp has N variables, and if N^V > eval_limit, the evaluation is skipped, and the clause is given the value TRUE. December 1, 2005. Changed isofilter so that symbols starting with $ are ignored. These are assumed to be Skolem constants and functions. A new command-line options "include_skolems" causes the old behavior. November 22, 2005. Reorganized ladr/glist.c. Changed parameters for clause printing routines (see ladr/ioutil.h). Forked search: child sends symbol table updates to parent. This allows child to introduce new symbols. November 17-18, 2005. Prover9: removed options x_proofs, r_proofs, xr_proofs, xr_proofs, standard_proofs. Now, the only kind of proof produced is standard_proof. Various proof transformations will be done by separate programs, e.g., apps.src/prooftrans.c. November 11, 2005. Changed format of justifications so they can be parsed as terms. In demodulation justifications, included an integer giving the position of the rewritten term. This is so that proofs can be easily reconstructed without knowing the demodulation parameters (term ordering, etc). This is a substantial change. Old: [para (37 (a 1) 216 (a 1 1)) demod (136 (R) 272)] New: [para(37(a,1),216(a,1,1)),demod(136(4,R),272(2))]. The term 136(4,R) means demodulation from the right (R) side of demodulator 136 at position 4 (4th nonvariable subterm, left-to-right, bottom-up). Without the R means the demodulator is used in the ordinary way (from the left). Removed parm demod_limit. Introduced parm demod_step_limit (max steps per clause) Introduced parm demod_size_limit (maximum size of rewritten term) November 7, 2005. Minor Mace4 bug: with set(trace), terms are printed with variables instead of integers (e.g., f(x,y)=z instead of f(0,1)=2) during trace. Fixed. --------- LADR-Oct-2005A---------- October 20--31, 2005. Several small changes, mostly cosmetic. October 19, 2005. Removed Prover9 CASC heuristics: limit on number of heavy clauses of the same weight, and demod_limit size increase. These were ad hoc and should be thought out before re-introduction. October 10-11, 2005. (While working on SOBB-II.) Renamed "goals" list to "denials". Introduced new "goals_positive" lists (clauses and formulas), to which the following happens. Clauses: conjoin, universal closure, negate, clausify. Formulas: conjoin, negate, clausify. The resulting clauses are appended to sos. SOBB-II uses this version. --------- LADR-Sep-2005A---------- September 30, 2005. Change auto_kbo so that if there is a lex command, the special unary processing is done only if the unary op is greatest. September 27, 2005 A new app (in apps.src) to format Mace4 models in various ways. It reads a Mace4 output and formats all of the "portable" models as one of the following: portable, portable2, cooked, raw, tabular, tex. This can replace the script get_interps. September 23, 2005 Mace4 max_megs bug. Cannot be increased beyond the default of 200 megs. Fixed by disabling the check in ladr/memory.c (mace4 handles max_megs its own way, because it allocates substantial memory without going through ladr/memory.c). September 22, 2005 When compiling on AMD64 machines, there were a few compiler warnings about pointers and integers being different sizes. All but one were inconsequential and trivial to fix. The nontrivial on was in mace4.src/propagate.c, in which something tricky was done (handling integers as pointers). The code was fixed by introducing a union to force alignment (see mace4.src/ground.h), but the warning still occurs. September 7, 2005 Check that variables in answer literals also occur in ordinary literals. Fatal error if not. September 1, 2005 Changed auto_inference for paramodulation with Horn sets. If the user has set para_units_only or para_lit_limit, the para_lit_limit is no longer changed automatically. Updated utilities/proofs_to_hints so that duplicate clauses are omitted. (Previously, clauses with duplicate IDs were omitted.) --------- LADR-Aug-2005B---------- August 25, 2005. Updated actions: (1) accept only a subset of flags/parms; (2) if weight function or given clause selection is changed, reweigh sos clauses and reconstruct the sos index. August 24, 2005 Print "level" messages for breadth_first. Accept actions triggered by level, e.g., level=3 -> set(print_kept). When printing proof, print level as well as length. August 19-21, 2005 Reorganized cac_redundancy code. Reorganized literal simplification (tautology, x=x). Reorganized examples on Prover9 Website. --------- LADR-Aug-2005A---------- August 18, 2005 Changed fold_eq and unfold_eq so that they are ignored if there is a lex command. August 16, 2005. Bug from Branden Fitelson (on PowerBook). Forking_search() (fof_reduction) sending data from child to parent. Fixed fd_read_to_ibuf() ladr/ibuffer.c. August 8, 2005. The new flag lex_order_vars introduced (exposed?) a bug in AC redundancy checking that caused associativity (when demodulated by commutativity) to be deleted. Fixed. Added parm max_vars. (Same as max_distinct_vars in otter.) Bug in term weighting if variables on right side of equation. Fixed. August 3, 2005. Changed auto (auto1_inference) so that for Horn sets with equality, para_lit_limit is set to the maximum number of literals in an input clause. (Previously it was always set to 2.) July 29, 2005 fold_eq flag. When more than one symbol gets folded, make sure that the relative precedence of those symbols stays the same. (Behavior of fold_eq with KBO (unary symbol of weight 0) still needs to be thought out.) July 29, 2005 Minor bug related to goals list. You can get multiple proofs of a goal when clear(reuse_goals) (the default). Fixed. --------- LADR-July-2005D---------- July 18, 2005 Sutcliffe found that prolog_style_variables is broken in Mace4. Fixed read_from_file(). This should not affect Prover9. July 13, 2005 New flag lex_order_vars (default clear). Similar to Otter's. New weighting feature: term depth. These allow proof of Knuth ternary problem. --------- LADR-July-2005C ---------- July 7, 2005 Prover9 released at the Milehigh talk. Michael Kinyon reports that it doesn't compile with GCC 2.96. Fixed some variable declarations in apps.src. Also made a few changes to the makefiles. July 1, 2005 Geoff points out that it can't prove a really easy theorem. Fixed a completeness problem with predicate elimination and equality. LADR-July-2005B sent to Geoff for CASC. --------- LADR-July-2005 ---------- June 30, 2005 Sent to Geoff Sutcliffe for CASC: