back to root

back to Matryoshka

FluidCases

• Alexander Bentkamp

  2020-04-16 15:50:34 (GMT)

  I'd like to make you familiar with the ugly sides of my plan for HOSup. Let's discuss if you think that this is something that we have to accept or if you think that we have to do better than that.

  Although we are not completely sure yet how the calculus for FOL with booleans will look like, we will definitely have a Cases rule that needs to be lifted to the nonground HO layer for our higher-order superposition calculus. For Cases inferences in fluid terms, the resulting rule looks very much like FluidSup. Here is an example that also resembles one of our FluidSup examples a lot:

  $a \not\approx c \quad\quad h\>(Y\>b)\>(Y\>a) \not\approx h\>(g\>(b \approx c))\>(g\>\bot)$

  This is unsatisfiable, as you can see by instatiating $Y := (\lambda u.\>g\>(u \approx c))$. Now FluidCases would produce the following from the second clause:

  $h\>(H\>(G\>b)\>b)\>(H\>\bot\>a) \not\approx h\>(g\>(b \approx c))\>(g\>\bot) \lor G\> a \approx \top$

  This is essentially DupSup/FluidSup with the imaginary clause $X\approx \bot \lor X \approx \top$. Now EqRes applies and we get:

  $(a \approx c) \approx \top$

  which yields a contradiction with the first clause, if our calculus works properly on FOL with booleans.

  I put the tentative FluidSup rule in its general form into the 2020-hosup document if you are interested.

• Petar Vukmirovic

  2020-04-16 16:23:2 (GMT)

  IMO, you spent a lot of time in designing a complete way to paramodulate into app-vars and after a year I am totally convinced FluidSup-like rule cannot be avoided for predicate-free HOL

• Petar Vukmirovic

  2020-04-16 16:23:11 (GMT)

  it is only worse when you go higher

• Petar Vukmirovic

  2020-04-16 16:23:47 (GMT)

  But I think this is perfect place to identify fragments which are well behaved

• Petar Vukmirovic

  2020-04-16 16:24:43 (GMT)

  And one more thing.. Maybe primitive enumeration is better (more contrallable in practice) than this approach

• Petar Vukmirovic

  2020-04-16 16:25:47 (GMT)

  (i.e., you will instantiate $Y$ with $\lambda x. Z_1 x \approx Z_2 x$)

• Petar Vukmirovic

  2020-04-16 16:26:12 (GMT)

  on which you can then perform eqres

• Alexander Bentkamp

  2020-04-16 17:9:40 (GMT)

  Primitive enumeration is a separate issue and does not help in this example. If you instantiate $Y$ with $\lambda x. Z_1 x \approx Z_2 x$, you can't squeeze in the $g$ any more.

• Petar Vukmirovic

  2020-04-16 17:20:13 (GMT)

  ooh.. I see. I dropped $g$ .

• Petar Vukmirovic

  2020-04-16 17:20:49 (GMT)

  One thing that I can tell you that I learned from PAAR submission is that $x \approx \top \lor x \approx \bot$ is horrible if it is in the proof state

• Alexander Bentkamp

  2020-04-16 17:22:5 (GMT)

  Yes, we should definitely not put it into the proof state. I just mentioned it to explain what's going on.

• Giles

  2020-04-16 20:58:57 (GMT)

  Petar Vukmirovic said:

  One thing that I can tell you that I learned from PAAR submission is that $x \approx \top \lor x \approx \bot$ is horrible if it is in the proof state

  I'm not actually following the conversation but occasionally take a look out of interest. It may already be obvious but the horribleness of this axiom was the sole motivation for the FOOL Paramodulation rule in Vampire.

• Alexander Bentkamp

  2020-04-17 6:24:55 (GMT)

  Yes, what we call Cases is essentially FOOL Paramodulation.

• Jasmin Blanchette

  2020-04-17 6:45:19 (GMT)

  If the axiom somehow does emerge, can it be picked up by the redundancy criterion?

• Jasmin Blanchette

  2020-04-17 6:45:52 (GMT)

  (Obviously, if it's in the original problem, it could -- and probably should -- be filtered out.)

• Jasmin Blanchette

  2020-04-17 6:50:36 (GMT)

  I'm not shocked by FluidCases and am guessing it can't be avoided. But I'd be curious in how the fluid rules behave in the second-order case: (1) Is DupSup complete then? (2) Does FluidSup coincide with DupSup then -- theoretically and in terms of Zip performance?

• Jasmin Blanchette

  2020-04-17 6:51:10 (GMT)

  These are open questions (at least in my mind) which we carry over from the $\lambda$-sup paper and which become relevant again with Cases.

• Alexander Bentkamp

  2020-04-17 7:22:4 (GMT)

  Jasmin Blanchette: If the axiom somehow does emerge, can it be picked up by the redundancy criterion?

  Yes, the GF layer (aka floor layer) will be FOL with interpreted booleans. So redundancy will be defined w.r.t. the entailment relation of that logic. Therefore $x \approx \top \lor x \approx \bot$ will be redundant.

• Alexander Bentkamp

  2020-04-17 7:36:15 (GMT)

  These are open questions (at least in my mind) which we carry over from the \lambdaλ-sup paper and which become relevant again with Cases.

  I think what you are suggesting is a good approach:

  • Accept that FluidSup and friends cannot be avoided
  • Look into ways to make FluidSup more performant:
    • Look into second-order logic and DupSup
    • Look into constraints for flex-flex pairs

• Petar Vukmirovic

  2020-04-17 7:40:48 (GMT)

  Alexander Bentkamp said:

  These are open questions (at least in my mind) which we carry over from the \lambdaλ-sup paper and which become relevant again with Cases.

  I think what you are suggesting is a good approach:

  • Accept that FluidSup and friends cannot be avoided
  • Look into ways to make FluidSup more performant:
    • Look into second-order logic and DupSup
    • Look into constraints for flex-flex pairs

  Exactly my thoughts when I said we should find well-behaved fragments