Semantic Guidance in Prover9

Using finite interpretations (models, algebras) to guide the search for a proof.

Evaluating a Clause in an Interpretation

• If all the symbols in the clause are interpreted, the clause evaluates to TRUE or to FALSE.
• It can be expensive: If the interpretation has n elements, and the clause has v variables, there are n^v instances to consider.

Semantic Restrictions on Inference Rules

(old method)

• Example: one parent must be false in the interpretation.
• Problems:
  • blocks very useful clauses
  • frequently incompatible with simplification strategies

---

Semantic Guidance

• Use interpretations to help select the given clause.
• Example.

---

Non-standard Uses of Semantic Guidance

• Generate a lot of FALSE identities as candidates to replace a quasi-identity (Kinyon).