back to root

back to Matryoshka

Full HOL sup

• Petar Vukmirovic

  2020-04-22 11:45:52 (GMT)

  Now that I am fixing regression bugs, I found one rule that i have implemented that is really (@Jasmin Blanchette ) important

• Petar Vukmirovic

  2020-04-22 11:46:22 (GMT)

  It is a modification to EqFact that takes into account subtle interference of booleans and app-vars

• Petar Vukmirovic

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

  (This might be interesting for both @Alexander Bentkamp and @Sophie )

• Petar Vukmirovic

  2020-04-22 11:47:53 (GMT)

  Namely, when you have a literal $P \, \overline{s}$ and a literal $\neg (\textsf{p} \, \overline{t})$ normally you cannot perform EqFact on them

• Petar Vukmirovic

  2020-04-22 11:48:58 (GMT)

  (because the first one is encoded as positive eq $P \, \overline{s}$ and the second one as $\textsf{p} \, \overline{t}$

• Petar Vukmirovic

  2020-04-22 11:50:22 (GMT)

  However, if we pretend the second one is $\neg(\textsf{p} \, \overline{t}) \approx \top$ (where $\neg$ is a real logical connective, not some meta-notation)

• Petar Vukmirovic

  2020-04-22 11:50:36 (GMT)

  The we can perform EqFact

• Petar Vukmirovic

  2020-04-22 11:51:12 (GMT)

  Note that this is different than first doing primitive enumeration with negation, since $P$ might appear in $\overline{t}$

• Petar Vukmirovic

  2020-04-22 11:51:36 (GMT)

  Similar tricks can be performed for all 4 combinations of app var has sign $s_1$ and prediate has the sign $s_2$

• Petar Vukmirovic

  2020-04-22 11:52:18 (GMT)

  This is very useful, and Visa and I discovered it while trying to solve some set theory problems in TPTP ( there are a lot of them )

• Petar Vukmirovic

  2020-04-22 11:53:10 (GMT)

  please reload, I edited latex several times

• Jasmin Blanchette

  2020-04-22 11:53:34 (GMT)

  Is our rule described in your PAAR submission?

• Petar Vukmirovic

  2020-04-22 11:54:16 (GMT)

  No, I just remembered it exists while finding out that in 1 of those 4 cases there was a bug

• Petar Vukmirovic

  2020-04-22 11:54:26 (GMT)

  Though I have no more space in PAAR :frown:

• Jasmin Blanchette

  2020-04-22 11:54:43 (GMT)

  Well if the rule is important, you can perhaps shorten something else?

• Petar Vukmirovic

  2020-04-22 11:55:19 (GMT)

  True... And maybe it is 15pg + ref (or maybe I can kindly ask for it to be :slight_smile:

• Jasmin Blanchette

  2020-04-22 11:55:25 (GMT)

  What surprises me is that EqFact has the reputation of being this rarely-useful-only-there-for-completeness rule.

• Jasmin Blanchette

  2020-04-22 11:55:41 (GMT)

  Right, just ask. I doubt they'll deny you that.

• Jasmin Blanchette

  2020-04-22 11:58:16 (GMT)

  What I do sometimes with the EasyChair template is to switch to Times New Roman. ;)

• Jasmin Blanchette

  2020-04-22 11:58:22 (GMT)

  That saves, like, half a page.

• Petar Vukmirovic

  2020-04-22 11:59:10 (GMT)

  We discovered it while solving Cantor's surjective theorem (there are more subsets than the elements of a set) that if we do not include it we cannot solve the problem
  so the reason I started this discussion is that it might be necessary for completeness?

• Jasmin Blanchette

  2020-04-22 12:0:15 (GMT)

  I'll let Alex et al. answer that one. ;)

• Jasmin Blanchette

  2020-04-22 12:1:40 (GMT)

  BTW Petar, in the PAAR paper, you have waay too much space between your tables and the captions. I guess you must be using \begin{center}...\end{center}. Try \centerline{...} instead.

• Jasmin Blanchette

  2020-04-22 12:2:8 (GMT)

  I can suggest more shortenings during our call at 16:00.

• Petar Vukmirovic

  2020-04-22 12:8:57 (GMT)

  ok ok sure :slight_smile:

• Jasmin Blanchette

  2020-04-22 12:12:58 (GMT)

  By "PAAR paper", I mean "PAAR submission" of course. ;)

• Alexander Bentkamp

  2020-04-22 12:30:55 (GMT)

  I don't think it's necessary for completness in our current approach, but it's still useful to understand why it helps.

• Alexander Bentkamp

  2020-04-22 12:31:39 (GMT)

  Petar Vukmirovic said:

  Note that this is different than first doing primitive enumeration with negation, since $P$ might appear in $\overline{t}$

  Why does it matter that $P$ might appear in $\overline{t}$?

• Alexander Bentkamp

  2020-04-22 12:37:51 (GMT)

  If $P$ did appear in $\overline{t}$, I don't think the unifier necessary for EqFact exists...

• Petar Vukmirovic

  2020-04-22 13:54:50 (GMT)

  Alexander Bentkamp said:

  If $P$ did appear in $\overline{t}$, I don't think the unifier necessary for EqFact exists...

  Remember that this is HO unification... This is an excerpt from the proof:
  image.png

  

• Petar Vukmirovic

  2020-04-22 13:55:1 (GMT)

  The unifier is complex, but it still exists...

• Alexander Bentkamp

  2020-04-22 13:55:24 (GMT)

  I was thinking of the fixpoint rule we mention in our HoUnif paper

• Petar Vukmirovic

  2020-04-22 13:56:5 (GMT)

  fixpoint cannot (should not) catch this since $F_0$ is applied

• Alexander Bentkamp

  2020-04-22 13:58:37 (GMT)

  oh, I see.

• Petar Vukmirovic

  2020-04-22 13:59:38 (GMT)

  and if you would apply primitive enumeration first, you would not get this unifier

• Petar Vukmirovic

  2020-04-22 14:0:21 (GMT)

  (this early at least)

• Alexander Bentkamp

  2020-04-22 14:1:8 (GMT)

  Ok, but this screenshot is different from what you said earlier. In the screenshot the variable-headed term is the negative literal. Above, the variable-headed term was the negative one.

• Petar Vukmirovic

  2020-04-22 14:12:44 (GMT)

  yeah it is one of the polarities

• Alexander Bentkamp

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

  With the polarities in the screenshot, our current calculus requires an EqFact inference, but I am not sure whether it is the one you mean:

  $\frac{C \lor p\>\bar{t}\approx\top \lor P\>\bar{s} \approx \bot}{(C\lor \bot\not\approx \top\lor P\>\bar{s}\approx\top)\sigma}EqFact$

  where $\sigma \in \text{csu}(P\>\bar{s}, p\>\bar{t})$

• Petar Vukmirovic

  2020-04-22 15:3:32 (GMT)

  this is ecatly what you want to avoid because this clause is a tautology

• Petar Vukmirovic

  2020-04-22 15:3:59 (GMT)

  $\bot \not\approx\top$ is simplified to $\top$

• Petar Vukmirovic

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

  and you are done

• Petar Vukmirovic

  2020-04-22 15:4:45 (GMT)

  if you pretend that $p \, \overline{t} \approx \top$ is $\neg (p \, \overline{t}) \approx \bot$

• Petar Vukmirovic

  2020-04-22 15:5:19 (GMT)

  than you get $\bot \approx \bot$ literal which can be removed

• Petar Vukmirovic

  2020-04-22 15:49:52 (GMT)

  Here is the proof the theorem which helped me and @Visa discover this rule: image.png

  

• Alexander Bentkamp

  2020-04-22 17:48:47 (GMT)

  This is a very cool example.

• Petar Vukmirovic

  2020-04-22 17:51:45 (GMT)

  Now that I am looking at it more deeply, I think you can get it with primitive enumeration, but that step is going to increase the penalty of already expensive clause (a lot of HO variables) and you will never find the proof

• Alexander Bentkamp

  2020-04-22 17:54:0 (GMT)

  But I think that you could do a similar trick with EqRes. When you have an equality of booleans t ≈ s (like you have in the forth box from the bottom), try to apply EqRes on ¬ t ≉ s. That gives you the empty clause directly without splitting in two branches as you do currently.

• Alexander Bentkamp

  2020-04-22 17:55:34 (GMT)

  Yeah, I don't think this is needed for completeness, but it's very useful anyway.

• Petar Vukmirovic

  2020-04-22 17:59:24 (GMT)

  @Jasmin Blanchette : Germans use very as well!

• Petar Vukmirovic

  2020-04-22 17:59:41 (GMT)

  BTW, you are right. I am going to implement that

• Petar Vukmirovic

  2020-04-23 9:38:16 (GMT)

  Here is the output after applying your fix:
  image.png

  

• Petar Vukmirovic

  2020-04-23 9:38:20 (GMT)

  Even cooler proof :slight_smile:

• Alexander Bentkamp

  2020-04-23 9:40:34 (GMT)

  Do you have other examples where the EqFact variant helped? Does the EqRes variant help there too?

• Petar Vukmirovic

  2020-04-23 9:49:58 (GMT)

  Currently, I am looking into them..

• Petar Vukmirovic

  2020-04-23 10:23:9 (GMT)

  Ok for this proof I previously needed primitive enumeration but with lazy clausification and solve formulas inference it is solved in 0.008s : image.png

  

• Jasmin Blanchette

  2020-04-23 10:27:35 (GMT)

  Wow, that's amazing!! You should put this proof in appendix to your PAAR submission, Petar!

• Petar Vukmirovic

  2020-04-23 10:31:46 (GMT)

  Yeah, for that I need to describe lazy clausification... I hope I will have the space for that :frown:

• Jasmin Blanchette

  2020-04-23 10:33:16 (GMT)

  You should use Times New Roman. I can give you my LaTeX setup from PxTP 2013. ;)

• Jasmin Blanchette

  2020-04-23 10:36:46 (GMT)

  Or forget PAAR and just send your work straight to J. Applied Logic for example.

• Simon Cruanes

  2020-04-23 13:38:57 (GMT)

  That's so cool. If you look in examples/ho/ I think there are some similar problems that used to not be solved (precisely because HO+bools is hard) :slight_smile:

• Ahmed B

  2020-05-11 17:59:54 (GMT)

  Petar Vukmirovic said:

  Here is the output after applying your fix:
  image.png

  This is a very interesting problem and proof. I can see no way to achieve the proof using the combinatory calculus at all.

• Petar Vukmirovic

  2020-05-12 9:19:6 (GMT)

  I think that the key to solving problem like this is delaying clausification.

• Petar Vukmirovic

  2020-05-12 9:19:26 (GMT)

  Maybe you can reuse VCNF machinery for that

• Alexander Bentkamp

  2020-05-12 9:24:10 (GMT)

  Another key is a strong unification algorithm. @Petar Vukmirovic You planned to design a new combinatory unification algorithm, right?

• Ahmed B

  2020-05-12 9:55:3 (GMT)

  Alexander Bentkamp said:

  Another key is a strong unification algorithm. Petar Vukmirovic You planned to design a new combinatory unification algorithm, right?

  The idea behind the combinatory calculus is lazy unguided unification as part of the calculus. For some problems it may be a good way to go, but for problems like this one it is disastrous.

• Alexander Bentkamp

  2020-05-12 10:0:14 (GMT)

  Oh, right. I was still thinking of the older approach with RCU.

• Petar Vukmirovic

  2020-05-12 12:4:31 (GMT)

  You are both right :slight_smile:

  Maybe you can see how lazy clausification works with combinators

• Ahmed B

  2020-05-12 12:34:14 (GMT)

  That is certainly something to investigate, but I doubt that it would help with problem SET557^1 in particular.

  The negated conjecture after ArgCong is:

  sk_1 (sk_2 x_0) x_1 \not\equal x_0 x_1

  Using the trick of negating one side and then doing an equality resolution only leads to a quick proof when higher-order unification is available.

• Alexander Bentkamp

  2020-05-12 12:59:34 (GMT)

  It's nice to see that Petar's unification algorithm can crack these TPTP problems, but we shouldn't get too obsessed with these small, tricky HO problems. This won't help on real life Sledgehammer problems. Of course, Petar is obsessed with them now because he wants to win the competition :grinning: