[metis-users] Parameters and incompleteness

[Joe Hurd]

Hi Jasmine,

> I was wondering whether custom settings of the Metis parameters could lead to incompleteness.

Yes indeed, I would describe parameter setting as a minefield.

> More specifically, Isabelle has so far operated with
>
>  val waiting_params =
>    {symbolsWeight = 1.0,
>     variablesWeight = 0.0,
>     literalsWeight = 0.0,
>     models = []}
>
> and I've found examples that seem to loop forever (who knows really), but that are solved very quickly with "variablesWeight = 0.5". Should "variablesWeight" and "literalsWeight" be nonzero?

The waiting_params control the order that clauses are removed from the
empty set. The way that Metis implements this is that there is a
default FIFO-ish weight (the "distance" of a clause from the initial
clauses), and the parameters in the waiting_params structure modify
the default weight. I *believe* that this procedure will eventually
remove every clause from the waiting set, and so is complete (but
proving this is rather subtle and depends on the whole loop).

> Vampire is not a model of documentation, but they nonetheless documented which values of which options are incomplete [1]. This could be an idea for Metis as well.

I think that would be a good idea, but would take significant time to
do a good job (so may not happen).

> While I'm mentioning documentation issue, I've been bitten by assuming that ":" and "." (like all the other pretty-printed operators) were uninterpreted -- but there is special support for those in Metis, and incompleteness seem to rear its ugly head if these are not used in the intended way.

Yes, it would be safest to regard these as reserved words and avoid
these. They are interpreted to solve specific problems that came up in
practice:

"variable : type" terms were unifying with all possible
paramodulations "s : type = t : type", but it's complete to skip
paramodulations into variables. Metis interprets "variable : type"
terms as variables for this purpose to block paramodulation (since ":"
is morally just an annotation).

"function . argument" terms encode higher order function applications,
and Metis interprets them this way for the purpose of weighting
clauses using finite models. [Isabelle doesn't use this heuristic, so
this shouldn't matter.]

Hope that helps to clarify things.

Cheers,

Joe