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

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

See the

Syntax (all LADR programs)

Clauses and Formulas

• Non-clausal formulas are recognized and translated to clauses (by universal closure and clausification).
• Labels on non-clausal formulas are inherited by the resulting clauses.
• Non-clausal input formulas are shown in proofs.

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.

prover9 -f subset_trans.in > subset_trans.out

Symbols

• Less space is required around symbols.

  Previously:	x' ' ' ' = x
  Now:	x'''' = x

• Multicharacter operator declarations require quotes:

  op(400, infix, "--->").
  

• Different parse types of the same precedence are not allowed (including built-in declarations).

  op(333, postfix, @).
  op(333, prefix, ~).    # not allowed, given the preceding declaration
  

  This restriction avoids ambiguous strings, e.g., (~ x @).

TPTP Translators

tptp_to_ladr < PUZ031-1.p > PUZ031-1.in
prover9 -f PUZ031-1.in > PUZ031-1.out

tptp_to_ladr < PUZ031-1.p | prover9 > PUZ031-1.out2

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

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

Hints

• New selection method.
• Clauses that match hints receive ordinary clause weights.
• Hints are now back demodulated.
• New flag set(breadth_first_hints).

Relational Definitions

• Option to expand with relational definitions. Example:

  prover9 -f subset_trans_expand.in > subset_trans_expand.out
  

• A more interesting example:

  prover9 -f t2_23.in > t2_23.out  (XML-formatted proof)
  

• Note that definitions must include all quantifiers.
• FUTURE: user marks definitions to be expanded.

Non-Horn Problems

• Ordered resolution/paramodulation with literal selection.
• More complete and more effective.
• New flag para_from_vars (default set).

Term Ordering

• Split "lex" command into "function_order" and "predicate_order" commands.
• ("lex" is still accepted as a synonym for "function_order".)
• The default predicate_order has "=" smallest instead of largest.

Weighting (and related things)

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

• Semantic guidance with multiple interpretations: Clause is "false" if it is false in all (previously some) interps.
• New command-line option: -p (fully parenthesize all terms, for testing op declarations)

Prooftrans

• Option to remove labels from clauses.
• Option to not attatch new labels to clauses.

IVY Proof Checker

• It's now trivial to double-check your Prover9 proofs.
• Give it a Prover9 output containing some proofs:

  prover9 -f subset_trans.in > subset_trans.out
  

• Or run "prooftrans ivy" and give it the IVY proof object:

  prooftrans ivy -f subset_trans.out > subset_trans.ivy
  

Mace4

• No substantial changes.
• New HTML documentation, part of Prover9 manual.

Isofilter

• Option to check for isomorphism on specified subset of the operations.