FVIndexing will not work that well for _very_ large signatures (in fact, it does not deal nicely with growing signatures now. But we can _group_ function symbols and count/position them (easiest done using modulo on the FunCode!) and use them. I've changed the rewrite system and eliminated the use for TPRestricted. Detection of rewritable processed clauses now takes the restriction into account, however, actual rewriting does not, i.e. the first rewrite will always win, even if it is a non-intantiated top level step. This is of course sound - is it also complete? It _should_ be, by the same argument that unrestricted rewriting of unprocessed clauses is ok...think & test! * In this context: Clean up the mess by removing dead code! -> No, it didn't, but I've now fixed it. Index for backwards-rewriting: Two separate indices, one for restricted terms, one for unrestricted ones. Data structure: (key->(term, clause*)) - position is not needed for this (or is it? Check current code if RW-link is always added). Abstract interface: Index returns candidate. One implementation: Return _all_ term/clause* pairs (i.e. no indexing), second: Use top-level hashing, third: use more advances path indexing. Index for unification: Store all candidate terms. Data structure: (key->(term, (clause, position)*))*. See above. Detect definitions and make defined symbols large in the precedence (instead of automatic unfolding). Beautify the handling of FVIndexing somehow (the trouble is that the index can only be computed when the preprocessed clause set is there...hmmm). Evaluate --inherit-conjecture-pm-literals. Purity. For the equational case, use non-E-unifiability as the criterion (approximate it with universal equality). Condensing. Flattening of ground terms (anti-unfolding ;-), useful for termination in many theories, and maybe in general. Contextual rewriting Use plain back propagation MLP for classification (n out of m multiplexer, error measure: Difference from wanted result (-1 for bad, 1 for giid heuristics). For input of discrete features use individual neurons. Can e.g. finally encode the UEQ <= HEQ <= GEQ (if that makes sense...). Do a Python prototype soon! Rippling-like annotated terms for E. Split only if clause has multiple inference literals. -> See below, stupid! Precedences giving different weights to frequencies in positive and negative literals (positive more seems better). Geoff's Idea: Goal-Directed heuristics, using similarity measures on frequency vectors. Alternatively: Giving bonus for smaller features. Simpler: Use frequency of symbols in goals to compute weights (symbols in goals are preferred). -> Simple version now done. Waldmeister-Style MixWeight: |max(s,t)| * (|s|+|t|+1) + |s| + |t| Caching term orderings: - Key: Only three kinds of instantiations (Never, Always, Once) -> allows caching for each value - Cache in OCB (no additional arguments to pass) - Cache is of term cells affected - Term stores its cache entry in multi-function field (reuse rewrite_hack). Invariant: Field is NULL unless used (side effect: eliminate TPIsReplaced, use field instead) - Cache entry: For KBO array of weighs, for LPO array of trees of other terms with comparison (key: (term, instatiation)). - After comparisons for a given instantiation are done, call "ClearCache": Pop stack, delete cache entry for term, until stack is empty. Replace VarHash with simple PDArrays if time critical. As variables idents are small in practice, should work with little memory overhead, but much faster. Perhaps put outputlevel and stream into proofstate? Allows for more customization. Again perhaps: Give names to proofstates and termbanks and prefix output about operations on a state with the name? Improve distribute_eprover.awk: Insert included files at the correct place in the command line, store logfile with job -> We can run multiple test runs in one call of the script, and do not have to wait for late jobs before starting the next parameter set. Generate Term Orderings: a) Try to orient axioms (perhaps try to orient pos-units from larger to smaller terms, all other literals smaller to larger terms?) - partially done, without preferred orientations. b) Run prover for n steps, take ordering which resulted in least amount of new clauses c) For non-unit clauses: Only (or primarily) take positive literals (=potential rewrite rules) into account. New Idea: Use "Trigger equations" with weight and ordering constraints! Dynamically addjustable pick-given-ratio (test with Scheme first --> test done, successful) Syntax: n@m[+-*/]k - initial value n - every m processed clauses modify n by adding/subtracting/multiplying with or dividing by k - Perhaps add limits?[a..b]? Rethink Simweight...return something based on the comparison of equal and unequal parts! gettermweight() is somewhat inefficient. If we don't need the weight multiplier, we can perhaps speed it up with a simple stack-based algorithm -> Ask Joachim! Consider unions to make term cells smaller Sort clauses (ordering on term numbers or pointers?) and unoriented equations, compare clauses, change clauseset to clause trees and keep only one copy of identical clauses --- will be difficult and perhaps unnecessary... (Probably won't do it -> now implemented for static clauses and called at intervalls) Extend index for literal subsumption? (Seems to be unnecessary) Implement Vampire-like pseudo-KBO: Weight, Vars, Word-Lexicographic Literal selection with P-Functions seems to work by inducing a fixed order on negative condition processing. If this is the case, perhaps we should not do selection for the case that there is only one negative literal, or the fact that a unique negative literal is maximal. On the other hand, perhaps we should use selection of positive literals for the case of a single negative literal even if we usually don't (yes, I do need to unify and rewrite all of the selection module at some time. Thanks for reminding me!) SelectComplexExceptRRHorn -> Check if the maximal literal is orientable, check if rule is range restricted with respect to this maximal term... Select DiffNeg orientable literal Select always unless UniqMaxPosOrientable (Waiting for results from the above to decide on base selection strategy) Select literals with variables not bound in any positive literal. Alternatively, select maximal negative literal if it exists (might have similar effect) Rework literal selection. Three parameters: Do I select, which negative one do I select, which positive one do I select (currently thats either none or all). Perhaps even better: 4 Parameters - decide on negative and positive selection individually. Do we want to select positive literals for paramodulation into other clauses as well? New selection concept? Use index for paramodulation from processed clauses into new ones - only needs maximal terms from maximal positive literals in clauses without selection If I need to touch all of this anyways: Get rid of the literal selection hack (selected literals are somewhat maximal) and cleanly separate these. Implement weight function that uses different penalties for unorientability of positive and negative literals -> Done, needs more testing For orientable rewrite-rules, give a higher weight to minimal sides than to maximal ones (prefer rules that decrease term size). For split clauses, give the split literal the (default) weight of the split off literals. Requires quite some work, as it touches most evaluation functions, but should be worth it. -> Done for some evaluation functions, thrown out again. To complex, doesn't seem to help. Always select positive split literals if we select at all! Then negative units can resolve against them...or we'd rather need a special simplifying inference for that kind of situation. -> We need this, and in general. It is complete (the resulting clause alone implies the parent, and is smaller). On the third hand, see Vampire paper in Proc. IJCAR for the different strategies implementable with splitting. Also think about contextual rewriting! -> Done for the simplification inference. Also read Alexandre's and Andrei's Paper! Use ordering constraints on clauses generated from unorientable literals or literals which are not uniquely maximal in the clause. If we use a unit with contraints for rewriting and the constraints to not evaluate to the trivial true case, we might need to drop constraints. Make some more measurements about relation of EqnCells to TermCells. If we really need less than one TermCell per EqnCell for hard problems, we should move the TermBank-Pointer from the EqnCell into the TermCell. This also would make many debugging operations simpler, because we have access to the signature from any shared term! Sharing factor used introspectively! Search for non-equational equivalences, add them as rewrite rules. Can we generalize this to equational literals? Does it make sense there or is it somehow subsumed by rewriting? Try to select (or unselect?) sort predicates of the form -p(X) for some p. On the plus side, may only instantiate X to terms of the correct sort. On the down side, perhap we can only prove sort for very specific instances and enumerate them. -> Done, never selecting them is (usually) good! For eground: Implement a special clause type taking up less memory. Implement the incomplete grounder by just taking the ungrounded system, instantiating everything to some constant (the most frequent constant?) and copying the set. (partially done) Literal sharing (with external sign?)! We can share lots of operations: - Unit subsumption and Simplify-Reflect - Select the same literal throughout the proof state (we can have local selection as well!). Problem: What happens if multiple literals are selected then? Possible answer: Then prefer only clauses with exactly one selected literal - if we solve this literal (at least in the Horn case), it should vanish everywhere! Or: Process only positive clauses and clauses with exactly one selected literal. For eground: - Move to explicit constraints _stored with the clause_ - Compute constraints before grounding, propagate to split clauses - Use unification constraints in clauses as they are generated! I.e. use constraints from both clauses (might be more expensive, but probably worth it). - Split only clauses with more than one inference literal -- nope, if it can be split at all, then there are at least two maximal literals! - New output levels: 0 - Nothing 1 - As currently 2 - Just the proof (don't know how...) 3 - A subset of all steps 4 - All inferences 5 - Additional information like subsumption, evaluation,... - Agressive split! -> Done - Agressive destructive resolution -> Done - Literal cut-off - Use the better data structure control we have thanks to the new rewriting to keep better track of ordering comparisons in literals and clauses. - Found and fixed a bug in the implementation of SoS. Redo the corresponding test runs! Fix another bug: If a SoS clause is used in simplification, then the child is SoS! Fix for E 0.71!