# Meta-Prover Design¶

## Intro¶

The meta-prover is a software component that is responsible for reasoning about properties of logic symbols, but not for solving the actual problem at hand. It deals with the higher-level structure of a problem, more at the level of meta-data than the raw axioms given by the user. See [BurelCruanes2013] for more details.

## Structure¶

The meta-prover has two main tasks to carry out:

1. Scannings
for patterns in clauses it is given (from a running resolution or superposition prover, or from an input file...). A successful scan may add facts about the problem (presence of a given axiom instance).
2. Reasoning
over known facts and structures (theories, lemmas, etc.), using both a known knowledge base (definition of theories, known lemmas) and the results of scanning.

## Implementation¶

The logic representation of the meta-prover is a form of `HOTerm`, ie. first-order terms with currying, no quantifiers. The relevant variants (a `Lambda` variant is omitted) are:

• `Var : int -> term`

a universal variable, typed, used for abstracted symbols, and for Horn clauses

• `RigidVar : int -> term`

a universal variable, typed, used for problem-level quantification. This can only by matched with another rigid variable (for alpha renaming).

• `TyAt : type * term -> term`

curried application of a term to a type (for polymorphism)

• `At : term * term -> term`

curried application of a term to another term

• `Multiset : term list -> term`

multiset of terms, very handy for representing clauses. Unification of multiset is not AC-unification, but instead unifies subterms pairwise. All terms must have the same type `tau`, in which case the multiset has type `multiset(tau)`. This is used both for equational literals, with `eq_lit {| a, b |}` representing `a = b` (resp. `neq_lit`) and clauses (multisets of literals).

• `Record : (string*term) list * term option -> term`

record value, with a list of `field : term` pairs (with pairwise distinct fields) and an optional “remainder” part that must be a variable of type `record(T)` (with `T` some type). The type of the record is given by the typing rules for records. The remainder part is used for unification, for instance

```{x:X, y:2 | R} == {x:1, y:Y, color: red}
```

succeeds and yields

```X=1, Y=2, R = {color:red}
```

applying the substitution to the first record yields

```{x:1, Y:2, color:red}bound
```

The typing rules for records are the following

```t_1:tau_1 ....                        t_n : tau_n
-------------------------------------------------
{f_1:t_1, ..., f_n:t_n} :             {f_i:tau_i}

t_i : tau_i                             y : tau_y
-------------------------------------------------
{f_1:t_1, ..., f_n:t_n | y} : {f_i:tau_i | tau_y}
```

### Scanning¶

We need a specific mix of matching and alpha-equivalence checking for scanning concrete clauses so as to find instances of patterns. A pattern is just a term in which all salient function symbols (which occur in some structure at the meta-level) as abstracted into variables. The meta-prover must remember which variables are regular universal variables, and which ones are abstracted functions.

The scanning operation must bind abstracted variables to concrete terms (the matching part) but cannot bind universal variables to anything else than other universal variables (the alpha-equivalence part). Binding type variables is ok.

For instance, if a pattern for commutativity is `F X Y = F Y X` with abstracted variable `F`, then scanning the concrete clause `g a X Y = g a Y X` succeeds by binding `F` to the concrete term `g a`, and binding universal variables `X` and `Y` to other universal variables.

Scanning is actually done by encoding the problem clauses, in a shallow way, using `Multiset` constructors and `RigidVar`. For a clause `c` let `c'` be its encoding; we then add `holds c' <- .` to the clauses of the reasoner so that it can match axiom definitions. Axioms are described by `axiom foo <- holds c.` where `c` is the clause that describes the axiom.

The encoding of clauses is done by:

1. currying applications
2. replacing free variables by `RigidVar` instances (in order to force
unification to be only alpha-equivalence on those)
3. replacing equational literals `a = b` by `eq_lit [a, b]`
and `a != b` by `neq_lit [a, b]`
4. replacing the clause by `[l1, l2, ..., ln]` where the `li` are
the encoded literals.
5. adding `holds c.` to the meta-prover where `c` is the encoded clause.

### Reasoning¶

As all rules are Horn clauses, of the shape `A <- B_1, ..., B_n`, or simple atoms that we call facts. Since we embed universal variables, or type variables, it actually isn’t always true that atoms are ground.

The idea is simply to use a term index, and regular unification, to perform unit resolution. Roughly, the rule is

```A <- B_1, B_2, ..., B_n        B
--------------------------------
sigma(A <- B_2, ..., B_n)

if sigma(B_1) = sigma(B)
```

### Indexing¶

It is important to have some form of indexing. See the page about Higher-Order indexing.