LADR Updates, ADAM-2009

Contents

Bugs and Such

See the Changelog file.

Floating-point Values for Weighting

The following weighting parameters accept floating-point values (as well as integers).
max_weight, variable_weight, constant_weight, not_weight, or_weight, sk_constant_weight, prop_atom_weight, nest_penalty, depth_penalty, var_penalty, default_weight, complexity.
Floating-point values must be enclosed in double quotes, for example, 
assign(max_weight, "13.5").
Weighting rules accept floating-point values (as well as integers), for example, 
list(weights).

  weight(a) = "3.2".
  weight(f(a,x)) = "5.6" * weight(x).
  weight(f(a,_)) = "-1.1".

end_of_list.

Complexity for Given Clause Selection

Adjust weights of clauses based on the number of repeated subexpressions.
0 ≤ complexity(C) < 1.
Lower values mean more complex (better??).

Usage: 

assign(complexity, n).       % default 0
means that n * complexity(C) is added to the weight of each clause C.

Conditional Demodulation: set(eval_rewrite)

Currently separate from ordinary demodulation: use one or the other.

Equational rules: rewrite terms. 

  alpha = beta.                % unconditional
  condition -> alpha = beta.
  alpha = beta <- condition.

Equivalence rules: rewrite atomic formulas. 

  alpha <-> beta.                % unconditional
  condition -> (alpha <-> beta).
  (alpha <-> beta) <- condition.
The Prover9 manual lists the evaluable operations that can be used with eval_rewrite.

Production Mode

set(production).
    % set(production) -> set(raw).
    % set(produtcion) -> set(hyper_resolution).
    % set(produtcion) -> set(eval_rewrite).
    % set(produtcion) -> clear(back_subsume).
Antecedents in production rules are either resolvable or evaluable. An evaluable antecedent is either built-in or defined (by an equivalence rule).

See the examples in the Prover9 manual.

Arithmetic for Mace4

Example: solve constraint-satisfaction puzzles involving integer arithmetic.

See the examples in the Prover9 manual.

Fast Generation of Terms

Say you wish to generate all well-formed terms containing exactly