[metis-users] Parameters and incompleteness

[Jasmin Blanchette]

Hi Joe,

I was wondering whether custom settings of the Metis parameters could lead to incompleteness. 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?

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.

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.

[1] https://docs.google.com/View?id=dcqg43v9_44d43x8ngj

Regards,

Jasmin