back to root

back to IJCAR 2020

Redundancy of clauses and inferences

• Uwe Waldmann

  2020-07-01 14:36:20 (GMT)

  Martin Suda asked what is the point of considering redundant inferences in addition to redundant clauses. Here's an example:
  Let $a > b > c > d$, then there is a superposition inference

  $\displaystyle{\frac{a = c \qquad a = b \lor a = d}{c = b \lor a = d}}$

  We would like to rewrite the conclusion to $c = b \lor c = d$ using the first premise.
  The conclusion does not become redundant in this way: It follows from $c = b \lor c = d$ and $a = c$, but the
  latter clause is larger than the conclusion.
  However, the original inference becomes redundant, since the clause
  $a = c$ is smaller than the larger premise of the inference, and that's
  sufficient.

• Jasmin Blanchette

  2020-07-01 14:48:45 (GMT)

  (@Martin Suda see Uwe's comment above.)

• Jasmin Blanchette

  2020-07-01 15:33:43 (GMT)

  @Uwe Waldmann I've added your example to our manuscript (jour.tex).