# 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 nv 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).