Prover9 Weighting

  terms(weights).

     a = -3.
     f(x,x) = 1000.
     f(x,y) = (2*x) + (3*y).   % wt(f(x,y)) = 2*wt(x) + 3*wt(y).
     h(_,_) = 0.               % anonymous variables match variables only
     x + y = x + y.            % wt(x+y) = wt(x) + wt(y)

  end_of_list.

• anonymous variable " _ " matches any variable and only variable
• can be clauses as well as literals and terms.

Right side of weighting equation: how to calculate weight

• Operations for integer arithmetic: +, -, *, /, max, min, depth.
• Otherwise recursively weigh subterms.

   assign(constant_weight, 0).    % applies to all constants
   assign(variable_weight, 2).    % applies to all variables
   assign(not_weight, 3).         % applies to netated literals
   assign(or_weight, 4).          % applies to multiliteral clauses
   assign(sk_constant_weight, 5). % applies to all Skolem constnats
   assign(prop_atom_weight, 6).   % applies to propositional atoms

   assign(skolem_penalty, 7).     % weight penalty for skolem functions
   assign(nest_penalty, 8).       % weight penalty for nested functions