[metis-users] Parameters and incompleteness

[Jasmin Blanchette]

Hi Joe,

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

Well, at least there's now a mailing list and an archive, so some of the information is now stored somewhere. ;)

> "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).

Ah, I see. I also used ": type" for types, which seemed reasonable, but this was done in an unsystematic way (using some clever but legetimate tricks), where paramodulation into "variable : type" appears to be necessary.

> "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.]

OK. We're actually using "." the way it's intended to be used, so this never was a problem.

Thanks for the explanations!

Cheers,

Jasmin