2020-03-24 18:4:42 (GMT)
Ok, let's move the discussion about HO Superposition here. As I mentioned in my email, the largest issue I've found so far concerns the -Elim rule, which is essentially this:
where is a fresh skolem symbol and are the free variables in .
The problem is that, on the ground level, the conclusion is not necessarily smaller than the premise.
Jasmin asked:
Why does the trick by Ganzinger & Stuber (namely, to make bound variables really big) not work for FOOL (or work for FOOL but not for HOL?)?
The reason that this is not in issue for Ganzinger and Stuber is that they work in FOL. So they have a distinction between terms and formulas and in particular variables cannot be bound inside terms. That makes it possible to create an order that makes bound variables larger than all terms. But in FOOL, we can have variables bound inside terms, which makes it impossible to make bound variables larger than all terms (because of the subterm property).
2020-03-24 18:6:5 (GMT)
My next question was: Why not have a trilogy in four parts? (With SUP-FOOL as part 3.) Alex's answer was that this would basically be more work, esp. at the nonground level (which he doesn't care about for lambda-SUP).
2020-03-24 18:8:7 (GMT)
My follow-up question was: What else needs to be adapted from part 2 to part 3 of the trilogy? Answer: Mostly the lifting from ground to nonground, which will require primitive substitution (enumeration/instantiation) for variables of type bool (and maybe partly appled vars etc. as well).
2020-03-24 18:9:3 (GMT)
I think that summarizes our 81 minute Skype call well.
2020-03-24 18:42:22 (GMT)
very naive question, but can you make _quantifiers_ very heavy in the ordering? (maybe with a coefficient?)
Here it's not just the bound variable, it's also about the quantifier itself.
2020-03-24 18:53:20 (GMT)
Very naive answer: Yes, sure.
2020-03-24 18:53:48 (GMT)
It still doesn't help you, because \bar y can be arbitrarily big.
2020-03-24 18:54:22 (GMT)
You can't predict how the \bar{y}'s will get instantiated. Maybe they'll contain lots of very heavy quantifiers.
2020-03-24 18:55:3 (GMT)
I guess it depends on what you have to instantiate [EDIT] free [END EDIT] variables wth. If there is no way to eliminate existential quantifiers eagerly, then unifications may instantiate free variables with terms containing existentials, and it seems that there is no way to stratify that.
2020-03-24 19:24:10 (GMT)
that makes sense indeed, if you want a complete calculus, you need to be able to instantiate with …
2020-03-24 21:5:35 (GMT)
I had a very complicated approach using basic superposition to solve this, but while writing it down for you, I realized that there is a much simpler way.
To understand the idea, you first need to know how my current definition of the TRS looks like. I make sure that has exactly two equivalence classes of type boolean, one whose normal form is and one whose normal form is . In particular, a term containing a forall- or exists-binder is never in normal form.
So if the term of the delta rule contains any forall- or exists-binders that are below variables of the corresponding nonground clause, these variables have been instantiated with a reducible term and we can apply the --trick.
2020-03-25 11:35:3 (GMT)
Yet another option could be to use a Hilbert choice binder (I think it's usually called ?) instead of the skolems:
If we treat similar to $$\lambda$$s, we would not need the subterm property for subterms inside -expressions (they would not be green). This would also mean that we cannot demodulate inside -expressions, but we could have similar tricks like DemodExt.
I think @Petar Vukmirovic told me that choice-terms like this perform better than skolems.
2020-03-25 11:45:34 (GMT)
Yes, this is all correct, but what is the difference with Skolems really?
2020-03-25 11:46:19 (GMT)
I mean, a skolem can really just be seen as a name for an \eps expression.
2020-03-25 11:46:31 (GMT)
You could treat skolems in the same way as the corresponding \eps.
2020-03-25 11:47:15 (GMT)
The main benefit of \eps IMO is that you can reason equationally (e.g. talk about soundness not equiv. preserv) and that you don't need to introduce fresh symbols.
2020-03-25 11:47:58 (GMT)
But we use Skolems elsewhere, and they make more sense than \eps terms (which get really big really quickly -- we have them in "metis" for example) in an implementation.
2020-03-25 11:48:35 (GMT)
Using would simplify the presentation because we would never need to talk about satisfiability-preservation.
2020-03-25 11:48:47 (GMT)
where else do we use Skolems?
2020-03-25 11:48:56 (GMT)
Right that's what I meant by "equiv. preserv".
2020-03-25 11:49:11 (GMT)
Well we use them a lot in "Extensions" of lambda-sup, don't we?
2020-03-25 11:49:33 (GMT)
Yes, but we could use choice there as well.
2020-03-25 11:49:48 (GMT)
Sure, but then we're farther away from an implem.
2020-03-25 11:50:2 (GMT)
With Pascal, we used \eps in one paper.
2020-03-25 11:50:11 (GMT)
It worked nicely.
2020-03-25 11:50:17 (GMT)
CADE 2017.
2020-03-25 11:50:19 (GMT)
I think @Petar Vukmirovic uses choice instead of skolems in the implementation already.
2020-03-25 11:50:27 (GMT)
Now JAR 2020.
2020-03-25 11:51:23 (GMT)
If so, I'm surprised the terms don't blow up. It was barely tolerable for metis; IIRC we had to introduce definitions.
2020-03-25 11:51:33 (GMT)
E.g. sko1 = \eps. ...
2020-03-25 11:51:34 (GMT)
Alex, skolems are used almost everywhere -- the only place where I used choice terms is in NegExt and it gave same or worse performance than using skolems
2020-03-25 11:51:43 (GMT)
so I use choice almost nowhere
2020-03-25 11:52:23 (GMT)
and for my lazy clausification I combine the best of using skolems and choice -- I maintain an index of formulas for which the skolems were introduced
2020-03-25 11:52:27 (GMT)
One way to think about the whole thing is indeed that a skolem is defined as "skoN = \eps ...." but that the equation is then forgotten.
2020-03-25 11:52:48 (GMT)
If you keep the equation around in theory, you can talk about soundness instead of sat.-preserv.
2020-03-25 11:53:3 (GMT)
when a generalization is found you can reuse the skolem -- this seems to be helpful as lazy cnf is working rather nicely (30+ problems improvement)
2020-03-25 11:53:20 (GMT)
Anyway, to summarize what I want to say:
2020-03-25 11:53:38 (GMT)
I think for the theory, Skolems and \eps are not so different.
2020-03-25 11:53:51 (GMT)
Right.
2020-03-25 11:54:3 (GMT)
\eps helped me a lot once because we wanted to use =
2020-03-25 11:54:12 (GMT)
and not some weaker relation
2020-03-25 11:54:20 (GMT)
(that would have complicated everything)
2020-03-25 11:54:51 (GMT)
One disadvantage for the theory is that this \eps would behave differently than the real \eps.
2020-03-25 11:55:5 (GMT)
Which is a constant and applied to a lambda: Eps (\lambda x. ...).
2020-03-25 11:55:13 (GMT)
A polymorphic constant of course.
2020-03-25 11:55:47 (GMT)
It's not a big disadvantage but every extra concept like this has a certain conceptual cost.
2020-03-25 11:56:22 (GMT)
End of summary/rambling. ;)
2020-03-25 12:4:11 (GMT)
Independently from eps vs sk, there is a decision whether superposition/demodulation should be allowed below the eps/sk.
2020-03-25 12:42:11 (GMT)
I thought it shouldn't -- otherwise you get trouble w/ the order. Or?
2020-03-25 12:56:21 (GMT)
I am not sure. The safest bet is certainly not to allow superposition/demodulation there. Then we can make as small as we want and the deltaElim rule is no big deal at all.
2020-03-25 12:58:36 (GMT)
But you think there might be an alternative, where e.g. the conclusion of delta-Elim is larger than the premise?
2020-03-25 13:1:43 (GMT)
There could be another way to make sure that the conclusion of delta-Elim is smaller than the premise for the relevant inferences. As I proposed above, we could use a variant of the theta-theta'-trick to make sure that the $$\bar{y}$$s are not instantiated with terms containing existential quantifiers.
EDIT: inserted a "not" above
2020-03-25 13:8:52 (GMT)
We have to make a similar decision for universal and existential quantifiers. Do we want superposition/demod below them or not?
Ganzinger and Stuber are not explicit about what their calculus does. I suppose the default would be to assume that they do superpose below the quantifiers. I have the impression that their proofs would work in both cases.
2020-03-25 13:10:42 (GMT)
Jasmin Blanchette: One disadvantage for the theory is that this \eps would behave differently than the real \eps.
Jasmin Blanchette: Which is a constant and applied to a lambda: Eps (\lambda x. ...).
Would you also prefer if forall and exists were constants and not quantifiers?
2020-03-25 13:12:14 (GMT)
OK, I can't find the "above" proposal (I must have missed it and/or cannot use Zulip search properly), but if that works indeed we'd have to choose between the basic-SUP-like approach and the theta-theta' approach (and I have no idea which one would be better).
2020-03-25 13:13:37 (GMT)
For the question of quantifiers: The way superposition works normally (as few inferences as possible), if we can avoid inferences below quantifiers, that seems preferable.
2020-03-25 13:14:1 (GMT)
Presumably some optional rules could take care of simplification or whatever else.
2020-03-25 13:14:7 (GMT)
The situation is analogous to lambdas.
2020-03-25 13:14:34 (GMT)
As for forall/exists as constants vs. quantifiers.
2020-03-25 13:14:46 (GMT)
In THF, they are actually constants.
2020-03-25 13:14:58 (GMT)
So are they in HOL/STT.
2020-03-25 13:15:25 (GMT)
It would be more standard thus to consider \forall x, ... as syntactic sugar and similarly for \exists.
2020-03-25 13:15:43 (GMT)
I'm guessing it wouldn't change things much
2020-03-25 13:16:22 (GMT)
Without constants, one has to write (\lambda p, \forall x, p x) to obtain the forall "constant".
2020-03-25 13:18:23 (GMT)
With a forall-constant, it would be much harder to distinguish between variables bound by a lambda and variables bound by a forall.
2020-03-25 13:26:58 (GMT)
Now I realized why we should go for superposition inferences below forall- and exists-binders and below skolems. If we don't, we will get more deep variables.
2020-03-25 13:34:16 (GMT)
He he.
2020-03-25 13:35:3 (GMT)
Of course, if you want to treat the two differently (and you probably want).
2020-03-25 13:35:28 (GMT)
Still, the two approaches are not so different.
2020-03-25 13:35:48 (GMT)
If \forall is applied, you're free to treat the \lambda differently.
2020-03-25 13:36:25 (GMT)
If it's not applied, you can treat it as if it were \lambda p, \forall ... (hm, eta-expansion).
2020-03-25 13:37:23 (GMT)
In short, I can't imagine the two approaches are that different, and one would give us a standard description of the logic.
2020-03-25 13:37:30 (GMT)
Jasmin Blanchette said:
If so, I'm surprised the terms don't blow up. It was barely tolerable for metis; IIRC we had to introduce definitions.
Hashconsing should make it a non problem, right? Assuming indexing/unification stop at the boundary.
2020-03-25 13:38:4 (GMT)
I can't talk for Zip, but in Isabelle both "hashconsing" and "assuming" are wrong. ;)
2020-03-25 13:38:36 (GMT)
Also, whenever you instantiate a variable, you have to instantiate it in those ugly terms.
2020-03-25 13:38:37 (GMT)
Well in Zipperposition hashconsing is a fundamental building block :-)
2020-03-25 13:38:57 (GMT)
So if by "nonproblem" you mean "much less of a problem", maybe.
2020-03-25 13:41:45 (GMT)
Also, I think that we will want to do superposition inferences below and hence indexing. I am convinced now that skolems are the better approach.
2020-03-25 13:41:53 (GMT)
I mean that the big term is already there (before instantiation of ), and multiple instances of the instantiated variables are not a problem because of hashconsing. The resulting term DAG is roughly the same size.
2020-03-25 13:42:18 (GMT)
but yeah, going under epsilons for unification is a bigger issue I think.
2020-03-25 13:44:38 (GMT)
The only thing I do not like about skolems is that we cannot claim that our rules are sound.
2020-03-25 13:52:7 (GMT)
Why care about soundness in a refutational prover?
2020-03-25 13:53:2 (GMT)
Good point :-)
2020-03-25 13:55:42 (GMT)
The saturation framework suggests that soundness is important by calling the consequence relation for soundness. Maybe it should be called the satisfiability preservation relation?
2020-03-25 13:59:23 (GMT)
But we will only consider HOL with choice, right? Otherwise skolemization would not be sat-preserving either, right?
2020-03-25 14:0:25 (GMT)
I think I will work out completeness on FOOL first (to keep my sanity), including nonground FOOL. My current favorite choices are:
2020-03-25 16:29:11 (GMT)
Concerning |\approx, all calculi that Uwe ever cares about happen to be sound. It's just since he's started working with us that he's facing calculi that are not sound. (Clausification is outside the calculus in his mind, and he never seemed to have cared much about Ganz. & Stuber.)
2020-03-25 16:30:0 (GMT)
Wasn't there an issue with |\approx as sat-preserv, which led Uwe to say we should take |\approx to be always true?
2020-03-25 16:30:44 (GMT)
Anyway, I'll rediscuss this with Uwe et al. I'm thinking we could remove |\approx from the prover architectures and instead add a sentence or two.
2020-03-25 16:32:48 (GMT)
As for HOL, yes sure with choice.
2020-03-25 16:33:5 (GMT)
But why wouldn't Skolem be sat preserving?
2020-03-25 16:33:36 (GMT)
Of course it is. As usual, you can see a skolem "sk1" as a definition "sk1 = eps ...".
2020-03-25 16:35:20 (GMT)
So either (1) you use "eps ..." right away (sound),
(2) you define "sk1 = eps ..." and use "sk1" (sat preserving), or
(3) you use "sk1" and forget "sk1 = eps ..." (weaker than (2) and hence sat preserving, a forteriori).
2020-03-25 16:37:4 (GMT)
Your favorite choices sound reasonable.
2020-03-25 16:37:44 (GMT)
To justify (2), you just need the usual trick (which you do at least twice in "part 2 of 3") of extending the model with a definition.
2020-03-25 16:38:2 (GMT)
From now on, we can refer to the three papers as 1/3, 2/3, and 3/3. ;)
2020-03-25 17:51:29 (GMT)
Jasmin Blanchette: But why wouldn't Skolem be sat preserving?
I meant it would not be sat-preserving if we do not have choice. Since we have Henkin semantics, the choice function would not need to be in the universe in HOL without choice. But you seem to be happy with having choice baked into the logic. Then all is fine!
2020-03-25 18:47:37 (GMT)
Alexander Bentkamp said:
The saturation framework suggests that soundness is important by calling the consequence relation for soundness. Maybe it should be called the satisfiability preservation relation?
The only reason for introducing was to highlight the point that it's independent of the consequence relation used in the redundancy criterion and in refutational completeness.. It's not really needed in the framework, but without it, readers might think that inferences must be sound w.r.t. , and that's not the case.
Jasmin Blanchette said:
Anyway, I'll rediscuss this with Uwe et al. I'm thinking we could remove |\approx from the prover architectures and instead add a sentence or two.
That's fine with me.
2020-03-25 21:25:51 (GMT)
I've given more thought to "forall- and exists quantifiers" (current favorite choice #2). I'm not convinced. This would basically uglify Section 2 to prettify Section 4.1 (of the report).
2020-03-25 21:27:13 (GMT)
Just think of e.g. Chris B. or Alex S. reading yet another nonstandard description of HOL in Sect. 2 and giving up reading there. :S
2020-03-25 21:28:36 (GMT)
I'm sure you can work with standard HOL and quantifiers as constants (or in fact just defined as \lambda p. p = (\lambda x. true)).
2020-03-25 21:28:56 (GMT)
Then for FOOL you have to choose: Either you see it as a subset of HOL or as it own thing.
2020-03-25 21:29:8 (GMT)
A fully applied subset, with no applied variables, etc.
2020-03-25 21:29:57 (GMT)
This kind of view might not be too frequent in the literature, but it's quite natural e.g. in Isabelle/HOL. Some tools define a predicate "is_first_order", or implement first-order matching, etc.
2020-03-25 21:30:44 (GMT)
"As its own thing" means you can have actual binders for \forall and \exists.
2020-03-25 21:36:4 (GMT)
What you are proposing is what I meant by "The F-encoding could translate forall-constants into forall-quantifiers if necessary". HOL would have a forall constant, FOOL would have a forall quantifier. The F-encoding would translate between them.
2020-03-25 21:37:52 (GMT)
I wasn't sure what you meant by "if necessary". But yes, if you go for "as is own thing", then that's what you'd do.
2020-03-25 21:38:11 (GMT)
If you go for "FOOL as a subset of HOL", you don't have to do anything there.
2020-03-25 21:39:47 (GMT)
I am still playing with the idea of having FOOL as a separate paper...
2020-03-25 21:40:3 (GMT)
Tempting.
2020-03-25 21:40:14 (GMT)
Maybe you could convince Petar and Visa to help you.
2020-03-25 21:40:32 (GMT)
Petar already implemented Ganz. & Stuber in Zipperposition, apparently.
2020-03-25 21:41:3 (GMT)
I mentioned this to Petar today and he freaked out at the thought of having to write the completeness proof.
2020-03-25 21:41:4 (GMT)
Jasmin Blanchette: Maybe you could convince Petar and Visa to help you.
Hehe, yeah, it would probably smart to team up for that.
2020-03-25 21:41:12 (GMT)
I said, relax!
2020-03-25 21:41:21 (GMT)
Alex will have proved the ground case anyway,
2020-03-25 21:41:34 (GMT)
and the lifting can't be so hard and you could ask Visa. ;)
2020-03-25 21:41:49 (GMT)
I mean, you saw their PAAR submission, right?
2020-03-25 21:42:21 (GMT)
It's eagerly clausifying instead of lazily, and no ref. completeness proof, but it's closely related.
2020-03-25 21:43:19 (GMT)
Yeah sounds good.
2020-03-25 21:44:2 (GMT)
I am mostly focussing on FOOL because all of HOL is just to much to think about at once. So it's a win win :)
2020-03-25 21:44:21 (GMT)
Right. You'd end up with a paper within a paper (or rather, report).
2020-03-25 21:44:25 (GMT)
That's too much.
2020-03-25 21:45:3 (GMT)
Petar could help design and tweak the nonground rules, evaluate, ...
2020-03-25 21:47:9 (GMT)
Ganzinger & Stuber isn't exactly the most cited paper (10 citations on Google Scholar), but you could subsume it.
2020-03-25 21:48:18 (GMT)
Doesn't mean it's not a good paper :slight_smile:
2020-03-25 21:48:52 (GMT)
BTW Simon, you must be happy: The chat is not dead!
2020-03-25 21:49:7 (GMT)
And we're now discussing new paper ideas in the open, like you dreamed all along.
2020-03-25 21:49:38 (GMT)
The Matryoshka grant proposal cites G&S. That makes 11 citations. ;)
2020-03-25 21:50:8 (GMT)
So much bullsh^H^H^H^H^Hforesight in that document. ;)
2020-03-25 21:50:51 (GMT)
Well, G&S say themselves that their work might be useful for HO Sup...
2020-03-25 21:51:2 (GMT)
Maybe I should read it at some point.
2020-03-25 21:51:24 (GMT)
I think I've thought that about 20 papers in the past 5 days. I have to make a list and reserve a day for reading ("Reading Friday")?
2020-03-25 21:51:34 (GMT)
)? -> ?)
2020-03-25 21:52:2 (GMT)
Should we try to be consistent with other descriptions of FOOL?
2020-03-25 21:52:18 (GMT)
Like the FOOL papers or with the TFX format?
2020-03-25 21:52:31 (GMT)
Funny, they write "That gap needs to be closed for any successful integration of automated provers into interactive ones".
2020-03-25 21:52:43 (GMT)
But in practice, encodings work surprisingly well.
2020-03-25 21:52:54 (GMT)
Yeah, this thing is completely matryoshka.
2020-03-25 21:53:2 (GMT)
Jasmin Blanchette said:
I think I've thought that about 20 papers in the past 5 days. I have to make a list and reserve a day for reading ("Reading Friday")?
Maybe we could all have an online reading group…
2020-03-25 21:53:15 (GMT)
Yes, I'm all in favor of reading group.
2020-03-25 21:53:29 (GMT)
They have that at MPI-SWS in Saarbrücken -- I get the emails in my spam folder.
2020-03-25 21:53:45 (GMT)
Always POPL or such papers, but we could do that for ATP and ITP.
2020-03-25 21:54:11 (GMT)
Should we start a new #readinggroup or #bookclub or whatever stream?
2020-03-25 21:55:40 (GMT)
Sure!
2020-03-25 21:56:3 (GMT)
BTW Michael Färber, who will join us in Sept., is a big fan of nonclausal reasoning.
2020-03-25 21:56:22 (GMT)
OK, who wants to be the stream master and pick the first paper?
2020-03-25 21:57:21 (GMT)
"Translating a conjecture into clause normal form before handing it over to the theorem prover is like shooting oneself into the foot before starting on a long hike", ha ha!
2020-03-25 21:57:36 (GMT)
From the Zipper man himself, G. Huet.
2020-03-25 21:58:17 (GMT)
Oh, the G&S paper is a Nancy-Saarbrücken collaboration. Totally Matryoshka.
2020-03-25 21:59:7 (GMT)
#bookclub is open!
2020-03-25 22:47:29 (GMT)
Hey - I didn't say much because I didn't want to interrupt your discussion but I'd be interested in the book club too, if you'd like to have me.
2020-03-26 15:20:23 (GMT)
@Alexander Bentkamp @Jasmin Blanchette Sorry that I am too late to join the party :)
2020-03-26 15:23:15 (GMT)
But I would be really happy if we were to extend bools PAAR paper with lazy clausification (already there) and completeness proof (scares the shit out of me as Jasmin mentioned :)
2020-03-26 15:27:22 (GMT)
But your paper is about HOL, right?
2020-03-26 15:27:56 (GMT)
I thought we could make a FOOL paper.
2020-03-26 15:44:34 (GMT)
yes yes of course
2020-03-26 15:44:40 (GMT)
sorry if I was confusing
2020-03-26 15:45:5 (GMT)
but completeness would be guaranteed for FOOL
2020-03-26 16:1:53 (GMT)
Shouldn't that be a separate paper then?
2020-03-26 16:2:23 (GMT)
I doubt that I can finish the proof for the PAAR deadline anyway.
2020-03-26 16:6:16 (GMT)
@Alexander Bentkamp I have good news for you! The PAAR submission deadline is (most likely, it's not on the website yet) going to be delayed by one month.
2020-03-26 16:6:36 (GMT)
wow, ok :D
2020-03-26 16:7:16 (GMT)
yay, more time to review papers! :tada:
2020-03-26 16:45:20 (GMT)
But still it feels like a bit too much for one paper...
2020-03-26 16:58:26 (GMT)
Alexander Bentkamp said:
I doubt that I can finish the proof for the PAAR deadline anyway.
Again I was unclear :)
2020-03-26 16:59:0 (GMT)
It should definitely be a separate paper and I think of too big scientific contribution to be published at any workshop
2020-03-26 16:59:33 (GMT)
ok, so is lazy clausification in the PAAR paper or did you mean it is already implemented in Zipperposition?
2020-03-26 17:0:3 (GMT)
it is only implemented, but not mentioned in PAAR
2020-03-26 17:0:30 (GMT)
okay, perfect. Then we have a clean separation.
2020-03-26 17:0:44 (GMT)
yeah sorry if I was unclear
2020-03-26 17:1:29 (GMT)
Let's make a FOOL topic here. This topic got a tiny bit out of hand.
2020-03-26 17:1:59 (GMT)
Or maybe I chose the title a bit too specific.