back to root

back to Matryoshka

Superposition and EqFact conditions

• Alexander Bentkamp

  2020-04-29 14:53:29 (GMT)

  Visa noticed that some of the conditions in my fboolsup draft are not necessary and this also affects our previous papers:

  • $u'\not\preceq v'$ in EqFact follows from the other conditions.
  • $D\sigma \not\succeq C\sigma$ in Sup follows mostly from the other conditions and when it doesn't, the inference is clearly redundant because there is a corresponding inference with C and D swapped.

  Should I remove these conditions from our two journal paper drafts?

• Alexander Bentkamp

  2020-04-30 10:40:56 (GMT)

  Looking a bit closer at EqFact, the condition $u' \not\preceq v'$ doesn't actually follow from the others. Here is an example:

  $\frac{a \approx f(a) \lor a \approx X}{X\not\approx f(a) \lor a \approx f(a)}EqFact?$

  All standard side conditions are fulfilled, but $u' \not\preceq v'$ is not: The literal $a \approx X$ is strictly maximal, and $a \not\preceq X$. But $u' \not\preceq v'$ does not hold because $a\prec f(a)$.

• Jasmin Blanchette

  2020-04-30 10:57:37 (GMT)

  Ah!!

• Alexander Bentkamp

  2020-04-30 11:44:46 (GMT)

  Probably there are similar examples for the condition on Sup. Actually, the condition on Sup is also in Bachmair and Ganzinger '94. So I will leave these conditions in there.

• Alexander Bentkamp

  2020-06-09 13:49:24 (GMT)

  Here is an example where the Sup side condition $D\sigma \not\succeq C\sigma$ is violated, but none of the other side conditions.

  $\frac{f(X) \approx g(Y) \lor h(f(X)) \not\approx c \lor h(g(Y)) \not\approx c \quad\quad f(X) \not\approx c}{g(Y) \not\approx c \lor h(f(X)) \not\approx c \lor h(g(Y)) \not\approx c}Sup$

  One could argue that this example exists not because $D\sigma \not\succeq C\sigma$ is a useful side condition, but rather because the other side conditions are too weak. For example, the literal $f(X) \approx g(Y)$ is maximal in the sense that there is no larger literal in the clause, but still, it would not be maximal under any grounding substitution. This would mean that we should instead define all conditions semantically in terms of the grounding.

  If we define all side condition semantically (i.e. "There exists a grounding substitution such that this or that is maximal"), the conditions in question here are really unnecessary. However, I assume that these conditions have been added because the semantic conditions are not efficiently computable.

• Jasmin Blanchette

  2020-06-09 13:57:34 (GMT)

  Interesting observations. My impression is that the calculus designing people have a mixture of computable and noncomputable conditions. The tension between being general and being close to the implementation is always there.

  The solution, naturally, is called refinement. The abstract calculus would use semantic side conditions and the concrete one would use computable conditions. But somehow refinement (beyond "here's my calculus and here's my prover") is rarely applied when it comes to calculus design. Calculus designers don't want to be bothered with designing more than one calculus, I guess.

• Jasmin Blanchette

  2020-06-09 13:58:25 (GMT)

  Our current situation is somewhat inconsistent, with the semantic condition e.g. in Sup (for which it would be impossible to give a syntactic criterion without knowing the term order).

• Jasmin Blanchette

  2020-06-09 13:59:55 (GMT)

  We could in principle go for fully semantics and add Remarks that point out potential syntactic criteria, but I'm not sure it's worth it, especially for core calculus rules. We also don't cover parallel superposition, for example. Maybe some of the superposition experts have an opinion?