Prover9 Semantic Guidance

Using finite interpretations to help select the given clause.

How it Works

Include one or more interpretations in the input file.
They must be in in Mace4's default "standard" format.
When a clause is kept, it is evaluated in the interpretations. If it is false in all 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=4, true_part=4, meaning that for one iteration it selects the oldest, then for 4 iterations the lowest weight "false" clause, then for 4 iterations the lowest weight "true" clause; and so on.

Examples

Here are some examples of semantic guidance on difficult problems.

These Prover9 jobs use set(lex_order_vars), which is risky, because it can block all proofs. See the Prover9 manual for the description of lex_order_vars.

Lattice Theory Huntington Identities

Get guiding interpretation.

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

Job with guidance (1 seconds).

prover9 -f LT.in LT-interp.out > LT.out ; ### ( LT.out.xml )

Job without guidance (23 seconds).

prover9 -t 7200 -f LT.in > LT-base.out ; ### ( LT-base.out.xml )

Boolean Algebra 2-Basis

Get guiding interpretation.

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

Job with guidance (20 seconds).

prover9 -f BA2.in BA2-interp.out > BA2.out ; ### ( BA2.out.xml )

Job without guidance (46 seconds).

prover9 -f BA2.in > BA2-base.out ; ### ( BA2-base.out.xml )

Modular Ortholattice Single Axiom

The Prover9 jobs in this section use the flag set(lex_order_vars) (see the manual), which reduces redundancy, but it can easily block proofs. It works very well for these examples, both with and without semantic guidance.

Associativity Property

Get guiding interpretation.

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

Job with guidance (46 seconds).

prover9 -f MOL-A.in MOL-A-interp.out > MOL-A.out ; ### ( MOL-A.out.xml )

Modularity Property

Get guiding interpretation.

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

Job with guidance (649 seconds).

prover9 -f MOL-M.in MOL-M-interp.out > MOL-M.out ; ### ( MOL-M.out.xml )

Associativity and Modularity Properties Together, without Guidance

(Associativity 169 seconds, Modularity 2891 seconds.)

prover9 -f MOL-base.in > MOL-base.out ; ### ( MOL-base.out.xml )