LADR/Prover9/Mace4 Updates (since ADAM-2006)

William McCune

This page was written for an informal presentation at ADAM-2007.


See the


Syntax (all LADR programs)

Clauses and Formulas

Big change: "clauses" are now "formulas".
formulas(assumptions).   % "assumption" is a synonym for "sos"

  p(x) & p(i(x,y)) -> p(y)  # label(condensed_detachment).

  subset(x,y) <-> (all z (member(z,x) -> member(z,y))  # label(subset_def).

end_of_list.
Example:
prover9 -f subset_trans.in > subset_trans.out

Symbols

The Infamous "op" command.

TPTP Translators

TPTP problem file -> LADR (Prover9 or Mace4) input file.
tptp_to_ladr < PUZ031-1.p > PUZ031-1.in
prover9 -f PUZ031-1.in > PUZ031-1.out
If you prefer, those two processes can be piped together:
tptp_to_ladr < PUZ031-1.p | prover9 > PUZ031-1.out2
(Not all TPTP language features are supported.)

LADR to TPTP.

A Problem: TPTP accepts a smaller class of function/predicate symbols.
A Solution: Translator introduces new symbols when necessary.

ladr_to_tptp < RBA-2.in > RBA-2.p

Prover9

Selecting the Given Clause (always a work in progress)

A cycle of size 6:

% These are the default values
assign(age_part,    1).           % oldest clause
assign(weight_part, 0).           % lightest clause 
assign(true_part,   4).           % lightest "true" clause 
assign(false_part,  4).           % lightest "false" clause 
assign(random_part, 0).           % random clause
assign(hints_part,  2147483647).  % lightest clause that matches a hint
If a clause for the current "part" is not available, that part is skipped.

FUTURE: A more general and flexible method is on the way (McCune, Kinyon, Veroff).

Hints

Relational Definitions

Non-Horn Problems

Inference rules for non-unit (especially non-Horn) clauses have overhauled.

Term Ordering

Weighting (and related things)

New parameters:
assign(max_depth, n).      % analogous to max_weight

assign(depth_penalty, n).  % weight of clause C is increased by n * depth(C)

assign(var_penalty, n).    % weight of clause C is increased by n * number_of_vars(C)

Prover9 Miscellany


Prooftrans


IVY Proof Checker


Mace4


Isofilter