Prover9 Semantic Guidance

How it Works

• Include one or more interpretations in the input file.
• They must be in in Mace4's default "portable" format.
• When a clause is kept, it is evaluated in the interpretations. If it is false in any of the interpretations, it is given the attribute "label(false)". You will see this label when the clause is printed to the output file.
• If there are no interpretations in the input file, Prover9 uses a default interpretation in which positive literals are true and negative literals are false; that is, a clause gets the label "false" iff all literals are negative.
• If a clause contains a symbol that is not in the interpretations, or if evaluation would take too long (see parameter eval_limit), it is given the value "true".
• The "false" attribute is not considered when calculating the weight of a clause, and it is not used when deciding whether to discard a clause. It is used only when selecting the given clause.
• When selecting the given clause, Prover9 cycles through three methods, in a ratio determined by the parameters
  • age_part: clause with lowest ID (the oldest clause)
  • false_part: false clause with lowest weight
  • true_part: true clause with lowest weight
  The default ratio is age_part=1, false_part=2, true_part=2, meaning that for one iteration it selects the oldest, then for 2 iterations the lowest weight "false" clause, then for 2 iterations the lowest weight "true" clause; and so on.

  Anomalies:

  • If one of false_part, true_part is 0 and the other is not, the false/true distinction disappears, and selection for that part is simply by weight.
  • If it is time to selet a "false" clause, and none is available, a "true" clause is selected instead (and vice versa). That is, we don't skip the selection of the "false" clause; we substitute a "true" one.

Examples

Lattice Theory Huntington Identities

mace4 -N12 -f LT-interp.in | get_interps | isofilter ignore_constants wrap > LT-interp.out

prover9 -f LT.in LT-interp.out > LT.out

prover9 -t 7200 -f LT.in > LT-base.out

Boolean Algebra 2-Basis

mace4 -n6 -m -1 -f BA2-interp.in | get_interps | isofilter ignore_constants wrap > BA2-interp.out

prover9 -f BA2.in BA2-interp.out > BA2.out

prover9 -f BA2.in > BA2-base.out

Modular Ortholattice Single Axiom

Associativity Property

mace4 -n8 -m -1 -f MOL-A-interp.in | get_interps | isofilter ignore_constants wrap > MOL-A-interp.out

prover9 -f MOL-A.in MOL-A-interp.out > MOL-A.out

prover9 -f MOL-A.in > MOL-A-base.out

Modularity Property

mace4 -n10 -m -1 -f MOL-M-interp.in | get_interps | isofilter ignore_constants wrap > MOL-M-interp.out

prover9 -f MOL-M.in MOL-M-interp.out > MOL-M.out