Alexander Bentkamp
2020-03-26 21:50:34 (GMT)
What do you think would be the best definition of clauses for FOOL?
(1) clauses are multisets of terms:
(2) clauses are multisets of equations:
(3a) clauses are multisets of (dis)equations:
(3b) clauses are multisets of (dis)equations:
Alexander Bentkamp
2020-03-26 21:53:41 (GMT)
Ganzinger and Stuber use (2). I am not entirely sure why, but maybe it simplifies the definition of their term rewrite system. If that's the only reason, that does not concern us for FOOL.
Alexander Bentkamp
2020-03-26 21:54:36 (GMT)
I think Zipperposition used to have (1), then (3a), and now (3b).
Martin R
2020-03-26 22:32:13 (GMT)
wouldnt be the first literal in 3b ?
Alexander Bentkamp
2020-03-26 22:54:36 (GMT)
Hehe, that would be 3c :grinning_face_with_smiling_eyes:
Petar Vukmirovic
2020-03-27 9:36:43 (GMT)
Zipperposition now has 3b
Petar Vukmirovic
2020-03-27 9:37:31 (GMT)
This coincides with what E has and seems to be working quite nicely
we motivate our decisions in PAAR paper
Alexander Bentkamp
2020-03-27 10:17:21 (GMT)
Ok, I found where you explain what you do on page 4, but I didn't find any motivation for it. So why is it better?
Jasmin Blanchette
2020-03-27 10:18:5 (GMT)
3b has fewer positive equalities
Alexander Bentkamp
2020-03-27 10:19:33 (GMT)
because fewer positive equalities = fewer superposition inferences?
Jasmin Blanchette
2020-03-27 10:19:38 (GMT)
yep
Alexander Bentkamp
2020-03-27 10:19:59 (GMT)
Then (1) would be best, right?
Jasmin Blanchette
2020-03-27 10:20:14 (GMT)
urgl
Alexander Bentkamp
2020-03-27 10:25:4 (GMT)
Of course, theses are just representations, so no matter how our calculus will look like, we can make it work with any representation.
Jasmin Blanchette
2020-03-27 10:25:21 (GMT)
right
Alexander Bentkamp
2020-03-27 10:27:4 (GMT)
I don't think that (3b) will make a very elegant description of our calculus because either our calculus requires us to do superposition inferences with booleans or not. I don't expect that it will behave differently for positive or negative predicates.
Alexander Bentkamp
2020-03-27 10:32:24 (GMT)
I would rather try to go for one of the other representations and try to make a calulus that does not require superposition inferences with booleans. I think we only need a resolution rule for predicates, which could be interpreted as superposition inference with booleans at the top level in representations (2), (3a), and (3b).
Alexander Bentkamp
2020-03-27 10:33:22 (GMT)
What is so ugly about (1)? It is actually the most simplistic solution. There would be only one type of equality. In the other representations, we have a term equality and a clause equality.
Jasmin Blanchette
2020-03-27 10:34:36 (GMT)
Sorry, I thought for the implem.
Alexander Bentkamp
2020-03-27 10:43:38 (GMT)
Yeah, I was thinking about both the implementation and the proof because I thought they should match, but maybe they don't need to match. Maybe I'll try (1) then, and then we can decide how to handle this in the implementation once the calculus is clear.
Jasmin Blanchette
2020-03-27 10:48:18 (GMT)
If your calc works on (1) then it's OK if the implem works on (1) too.
Jasmin Blanchette
2020-03-27 10:49:9 (GMT)
"Urgl" was a knee-jerk reaction thinking you'd have to duplicate your calculus rules, but if you want/need to duplicate them anyway, then (1) is better.
Jasmin Blanchette
2020-03-27 10:49:14 (GMT)
BTW Visa is on board!
Petar Vukmirovic
2020-03-27 10:50:59 (GMT)
Petar Vukmirovic
2020-03-27 10:51:17 (GMT)
Here is the motivation later on in the paper
Petar Vukmirovic
2020-03-27 10:53:2 (GMT)
From the implementation perspecive 1 makes you duplicate sooo many things
Petar Vukmirovic
2020-03-27 10:53:20 (GMT)
E implements predicates as 3b)
Petar Vukmirovic
2020-03-27 10:55:3 (GMT)
But I completely agree that it is the best to theoretically settle with a calculus, see what you need and do not need to do and then have a discussion how to implement this
Jasmin Blanchette
2020-03-27 10:55:33 (GMT)
Well if the calculus duplicates things in theory, the implem is very likely to have to duplicate things in practice.
Jasmin Blanchette
2020-03-27 10:55:56 (GMT)
BTW I'm going to rename the thread if you don't mind.
Petar Vukmirovic
2020-03-27 10:57:3 (GMT)
Jasmin Blanchette said:
Well if the calculus duplicates things in theory, the implem is very likely to have to duplicate things in practice.
Well, it depends. Maybe the dupication is not deep and used only for easier presentation and then it is better to go with 3b) in implementation
Petar Vukmirovic
2020-03-27 10:57:44 (GMT)
But if it turns out that there is a deep difference between predicates and equations between booleans an T (F) then we will have to see
Jasmin Blanchette
2020-03-27 11:2:41 (GMT)
Sure, but if it's for easier presentation it will lead to uglier proofs. ;)
Jasmin Blanchette
2020-03-27 11:3:14 (GMT)
We already merge positive and negative superposition as an economy of concept. I'd expect Alex wouldn't duplicate things just for "easier presentation". ;)
Petar Vukmirovic
2020-03-27 11:17:25 (GMT)
I am all not for duplicating :)
But I do not want to influence the proof artist :)
Alexander Bentkamp
2020-03-27 12:4:40 (GMT)
Ok, I changed my mind. I thought we would not need Superpositions into proper boolean subterms because we have the Cases rule. But in fact, there is a choice we can make. And now I think that Sup would be preferable over Cases in some situations.
For Example:
Given are two clauses:C[p] (where p is not at the top level) and p = ⊤ ⋁ D
Option A: Restrict Sup not to do inferences into proper boolean subterms. But Cases produces: C[⊥] ⋁ p = ⊤ and C[⊤] ⋁ p = ⊥. Then Sup for top-level booleans (aka resolution) applies to C[⊤] ⋁ p = ⊥ and produces: C[⊤] ⋁ D.
Option B: Restrict Cases to do produce only the case ⊥ if the boolean subterm is a predicate: C[⊥] ⋁ p = ⊤. Sup into the proper boolean subterm of C[p] yields C[⊤] ⋁ D.
Option A produces 3 clauses; whereas Option B produces only 2 clauses. So I prefer Option B. For Option B, representation (3b) is better suited.
Petar Vukmirovic
2020-03-27 12:29:57 (GMT)
It sounds good to me :)
Petar Vukmirovic
2020-03-27 12:30:51 (GMT)
In Kotelnikov's work Cases (or Fool Paramodulation) is already restricted to case using only one polarity
Petar Vukmirovic
2020-03-27 12:31:15 (GMT)
Why would cases produce two clauses in the first option?
Alexander Bentkamp
2020-03-27 12:47:29 (GMT)
Good point. That's another thing where we can probably choose. So far I assumed that the logical quantifiers and connectives would be dealt with at the top level, as in G&S. But we could also consider dealing with them before Cases brings them to the top.
Alexander Bentkamp
2020-03-27 12:48:7 (GMT)
Then we could possibly restrict Cases to one polarity.
Petar Vukmirovic
2020-03-27 12:50:49 (GMT)
There is another idea
Petar Vukmirovic
2020-03-27 12:51:11 (GMT)
What if we do not need cases at all? What if Ext- rules with boolean subterms are enough?
Alexander Bentkamp
2020-03-27 12:52:40 (GMT)
How would that look like?
Petar Vukmirovic
2020-03-27 12:55:11 (GMT)
well consider this
you have p(a =>b) and ~p(~b => ~a) for example.
now, instead of casing the terms inside to reason about their logical properties
you say I perform normal generating inferences conditioned under proving that some formulas are equivalent
Petar Vukmirovic
2020-03-27 12:55:51 (GMT)
this has the advantage that you do not carry around terms like p(T) and p(F) with different polarities
Alexander Bentkamp
2020-03-27 13:28:55 (GMT)
No idea how we could prove such a thing complete...
Alexander Bentkamp
2020-03-27 13:51:27 (GMT)
I suspect that it is better to deal with the quantifiers and connectives only at the top level and have a Cases rule for both polarities.
Alexander Bentkamp
2020-03-27 13:59:18 (GMT)
For boolean subterms that are predicates (i.e., do not start with at quantifier or connective), we can restrict Cases to only one polarity (as described in Option B above). This is consistent with the FOOL paramodulation rule because boolean terms in FOOL are always predicates. The connectives and quantifiers are eliminated during preprocessing by FOOL, right?
Petar Vukmirovic
2020-03-27 14:25:42 (GMT)
Yes they are :)
Petar Vukmirovic
2020-03-27 14:25:47 (GMT)
But would we do the same
Petar Vukmirovic
2020-03-27 14:26:5 (GMT)
My evaluation shows it is better not to do so
Alexander Bentkamp
2020-03-27 14:50:14 (GMT)
So basically, you are suggesting to clausify as little as possible and treat connectives in place, right?
Alexander Bentkamp
2020-03-27 14:55:53 (GMT)
Oh, right because that's what you did in the PAAR paper :-)
Alexander Bentkamp
2020-03-27 15:2:39 (GMT)
Ok, let's try the in place treatment then. However, I do not think equality and forall-quanitifiers can be treated in place. They need to be taken out with a Cases rule for both polarities.
Alexander Bentkamp
2020-03-27 17:3:35 (GMT)
(deleted)
Petar Vukmirovic
2020-03-27 20:0:10 (GMT)
Sorry I did not see this message
What I am saying is that we should not preprocess
Petar Vukmirovic
2020-03-27 20:1:22 (GMT)
That is, we should not rename nested booleans, because that is very detrimental to the performance
And if we can case as little as possible and transform the problem so that it is more first-order we should do it
(as p(a => b) and ~p(~b => ~a) shows)
Petar Vukmirovic
2020-03-27 20:1:46 (GMT)
well not very detrimental but it has an effect of around 30 problems
Alexander Bentkamp
2020-04-02 10:0:53 (GMT)
In the PAAR paper, there is not much about and . I have an idea, but I am unsure whether this is satisfiability preserving. We could add a rule to BoolSimp that says: where is a fresh Skolem symbol and are the free variables in . For , we could rewrite into and do the same there. Does that make sense?
Petar Vukmirovic
2020-04-02 10:18:18 (GMT)
For the first part, this is what (lazy) clausification does
Petar Vukmirovic
2020-04-02 10:19:3 (GMT)
For the second part, lazy clausification will just give new fresh variables to
Petar Vukmirovic
2020-04-02 10:19:19 (GMT)
Why do you think using double negation to represent is better?
Alexander Bentkamp
2020-04-02 10:25:19 (GMT)
Just to be clear: I am talking about proper subterms here: So for example, .
Alexander Bentkamp
2020-04-02 10:26:56 (GMT)
So will become ?
Petar Vukmirovic
2020-04-02 10:29:40 (GMT)
Not really: first it will be bubbled to the top level and then CNF will take care of it
Alexander Bentkamp
2020-04-02 10:30:7 (GMT)
Ok, that's different. I am wondering if the same can be done in place.
Petar Vukmirovic
2020-04-02 10:30:29 (GMT)
And honestly, I do not think there is going to be large difference, because rarely do you prove something
about Booleans if you do not case it or if you do not apply boolean extensionality
Petar Vukmirovic
2020-04-02 10:31:11 (GMT)
But now that I think about it
Petar Vukmirovic
2020-04-02 10:32:29 (GMT)
you are right... Maybe superposition will be enugh to prove if we do what you described
Petar Vukmirovic
2020-04-02 10:33:1 (GMT)
except that we do not use double negation to represent forall -- then we are back to square one and have to use extensionality/casing
Petar Vukmirovic
2020-04-02 10:33:33 (GMT)
But are you sure such an extension is satisfiability-preserving
Alexander Bentkamp
2020-04-02 10:33:51 (GMT)
No, I am pretty sure it is not. But I don't know why :-D
Alexander Bentkamp
2020-04-02 10:34:33 (GMT)
If becomes , I do know why:
Alexander Bentkamp
2020-04-02 10:35:42 (GMT)
Let's say you also have
Then a satisfiable problem becomes unsat.
Petar Vukmirovic
2020-04-02 10:36:17 (GMT)
ok I see
Alexander Bentkamp
2020-04-02 10:38:0 (GMT)
But the approach with the double negation is also odd because both and would become
Petar Vukmirovic
2020-04-02 10:39:21 (GMT)
wait.. wouldn't they be different skolems
Alexander Bentkamp
2020-04-02 10:39:35 (GMT)
yes, different skolems. But still.
Petar Vukmirovic
2020-04-02 10:41:5 (GMT)
strange indeed
Alexander Bentkamp
2020-04-02 10:41:41 (GMT)
So maybe it is sat-preserving, but not complete if performed as a simplification.
Petar Vukmirovic
2020-04-02 10:42:18 (GMT)
Yeah.. And again, even if we simplify it like that, we will need to later on case it or do extensionality most likely
Petar Vukmirovic
2020-04-02 10:42:29 (GMT)
so I very much doubt that it will be a significant gain
Alexander Bentkamp
2020-04-02 10:43:56 (GMT)
I think it might make the difference whether we need to have both a - and a -Cases rule or only a -Cases rule. But I will look into this further.
Petar Vukmirovic
2020-04-02 10:44:21 (GMT)
ok ok
Petar Vukmirovic
2020-04-02 10:45:6 (GMT)
A rule that distibutes the quantifier out would be helpful, but that is definitely not sat-preserving
Visa
2020-04-06 8:21:3 (GMT)
Hi!
Actually making a compromise between casing and conditional unification (CU) seems well motivated.
Weakness of Boolean CU is that it postpones processing of large nested formulas. This is harmful to completeness and potentially in practise too. At the mean time weakness of naïve casing is that it blindly splits everything eligible resulting in unnecessary duplication. A compromise is now to case large but unify modulo small formulas. This turns out to look like a simple representation tweak in casing.
Here I take =,⊤,⊥ as primitives and ¬,≠ as derived. Simplification is eager: b≠⊥ means b=⊤ if b is symbol, or b if b is equation. Boolean variables range over {⊤,⊥} and flat v makes clauses.
C[b] ⊢ C[⊥] v b, C[⊤] v ¬b aka CasesSimp can be written
C[b] ⊢ C[z] v b≠z where z is variable (⊤ or ⊥).
Consider the case that b <C[z] is small (precisely: C[z] has term [in]equation larger than b and ¬b). We might encounter an inference like
C[z] v z≠b, ¬C[z] v z≠c ⊢ z≠b v z≠c where c is small too.
Compacter conclusion would be b≠c as per CU. Since b≠c < C[z] v z≠b by smallness, such larger conclusion b≠c suffices to decrease counterexamples in completeness proof. CasesSimp itself will be complete because it makes inferences with "z=⊤vz=⊥" unnecessary by deleting the original clause. Hence it should be OK to leave small nested formulas in place, order them as ⊤/⊥ and unify conditionally in usual SP rules, which would be augmented with ∀+∃-elimination and CasesSimp for non-small formulas.
Side note: Encoding ¬A as ⊥=A is handy because it gives right order to ≠vs.= and to simplify t≠t⇔A. However it doesn't recover the usual superposition (negative literals need merging too) and Petar measured this kind of setup to be suboptimal. We can probably fix this in implementation thanks to selection as in refinements of the ES calculus. Selecting A=⊥ fixes the available rules and effectively raises its order so that it may be replaced by (A=⊤)=⊥—or by A≠⊤ with primitive ≠. We can change nested formulas similarly because if A≠⊤ doesn't dominate, neither does A=⊥, and if A≠⊤ does dominate, then its order is reduced to that of ⊤/⊥ by CasesSimp. Details such as effect(lessness) of order change to redundancy remain to be checked.
Alexander Bentkamp
2020-04-06 9:15:43 (GMT)
So if b is small, we can choose between these two representations:
- C[b], i.e. leaving b in place and order it as ⊤/⊥
- C[z] ⋁ b≠z, where z is a special kind of variable representing ⊤ or ⊥
Their behavior is identical, right?
Visa
2020-04-06 12:39:2 (GMT)
In C[z] v z≠b the variable z is not special in any way: all Boolean variables range over just {⊤,⊥}.
Representing C[z] v z≠b with "b in place" as C[b] is for implementation. Theoretically what matters is exactly the slight behavioral difference:
C[z] v z≠b, ¬C[z] v z≠c ⊢ z≠b v z≠c
C[b], ¬C[c] ⊢ b≠c
Replacing z≠b v z≠c by the larger b≠c is not a simplification but it makes the first inference redundant (assuming smallness).
Alexander Bentkamp
2020-04-06 12:44:16 (GMT)
Visa said:
In C[z] v z≠b the variable z is not special in any way: all Boolean variables range over just {⊤,⊥}.
What about all of the other boolean terms? They might all normalize to ⊥ or ⊤, but they still need to be considered somehow. Maybe with basic superposition we could get rid of them in the completeness proof.
Visa
2020-04-06 12:48:42 (GMT)
The range of variables depends on semantics, not syntax.
Alexander Bentkamp
2020-04-06 13:0:51 (GMT)
Ok, I am not sure about that, but all in all the ideas look promising!
Alexander Bentkamp
2020-04-06 13:3:26 (GMT)
Concerning z≠b v z≠c vs b≠c: Wouldn't we have to apply CasesSimp tob≠c, yielding z≠b v z≠c?
Visa
2020-04-06 13:6:52 (GMT)
No if b≠c can be oriented, say b→¬c with b atomic. Otherwise yes. The same as in ES.
Alexander Bentkamp
2020-04-06 13:10:31 (GMT)
So do you have a plan how the completeness proof for this could look like?
Alexander Bentkamp
2020-04-06 14:0:46 (GMT)
I would guess that abstraction (aka purification) has to be applied at least in the completeness proof, even if the implementation does something else. This will be necessary to justify unification modulo booleans as you suggested in your email. Probably completeness of ground and nonground calculus would need to have the abstraction. Then you could try to justify afterwards why abstraction can be replaced by a combination of unification modulo booleans and CasesSimp.
Visa
2020-04-06 14:15:55 (GMT)
CU for small formulas is an afterthought: E.g. a (half ground) reflexivity inference
t[z]≠t[y] v z≠b v y≠c v C ⊢ z≠b v z≠c v C
is made redundant by its CU version
t[z]≠t[y] v z≠b v y≠c v C ⊢ b≠c v C
because latter conclusion entails the former and is smaller than the premise. Others likewise. Leaving purified formula in place is an implementation representation recommentation.
I already told how similar argument allows CasesSimp to replace superpositions with z=⊤vz=⊥.
I'm not sure how this interacts with your calculus. The lack of representation normalization puzzles me. (What is the relation between A=⊥ and A≠⊤? Why aren't clauses terms? Why → is mentioned but xor not?)
Alexander Bentkamp
2020-04-06 15:8:23 (GMT)
What is the relation between A=⊥ and A≠⊤
A≠⊤ can be simplified into A=⊥
Why aren't clauses terms?
Of course, in principle, clauses could be terms, but the ordering and the calculus rules must currently behave quite differently on the clauses and on terms. Ganzinger and Stuber do the same, but it is less visible because they use the same symbols for clauses and for terms.
Why → is mentioned but xor not?
We can also restrict ourselves to some minimal set of connectives or add xor. Again, Ganzinger and Stuber do the same. I just added ¬ because I thought it would be nice to have in there.
I am open to change the representations. I also don't like that there are so many ways to say the same thing, e.g. A≠⊤ and A=⊥. On the other hand, when we had a discussion at the beginning of this thread, most people prefered (3b), although (1) would have been the most simplistic approach. In some sense, I went for (3a) now.
Visa
2020-04-06 16:38:41 (GMT)
I think representation (2) is nicest for theory. When =,v have multiset RPO status, the order works out of the box for both clauses and terms. The only critical part I see is the relation of = and ≠ (where t≠s means t=s⇔⊥). Also the simplification A≠⊤ ⟶ A=⊥ shows that ⊥ is nicer primitive than ≠.
I agree that (3b) is to be implemented. It is a special case of (2)+selection (as in ES; see my first message).
Alexander Bentkamp
2020-04-06 18:58:48 (GMT)
I also prefer (2) for the theory because it would give us a couple of case distinctions less, but I doubt Petar will be happy if we restrict ourselves to RPO.
Jasmin Blanchette
2020-04-06 18:59:10 (GMT)
You could use WPO.
Jasmin Blanchette
2020-04-06 18:59:18 (GMT)
It's a combination of RPO and KBO.
Alexander Bentkamp
2020-04-06 18:59:27 (GMT)
Oh, right. That's nice.
Jasmin Blanchette
2020-04-06 19:0:10 (GMT)
I think it's a sandwich: first RPO, then to break ties, weights, then to break ties again, some lexicographic or other stuff.
Jasmin Blanchette
2020-04-06 19:0:28 (GMT)
It would have to be lifted to ground lambda-free HOL I guess, but that should be easy.
Alexander Bentkamp
2020-04-06 19:0:42 (GMT)
Can it be implemented efficiently?
Jasmin Blanchette
2020-04-06 20:0:31 (GMT)
I think so.
Jasmin Blanchette
2020-04-06 20:1:0 (GMT)
I mean RPO like efficient
Jasmin Blanchette
2020-04-06 20:9:12 (GMT)
TKBO?
Jasmin Blanchette
2020-04-06 20:26:4 (GMT)
Like Petar (presumably), I wouldn't be happy with RPO only. We're trying to be graceful w.r.t. FOL, and in particular FOL w/ KBO.
Jasmin Blanchette
2020-04-06 20:26:48 (GMT)
Uwe worked out / reinvented WPO for superposition once, but he didn't publish it once he discovered it was subsumed by WPO.
Jasmin Blanchette
2020-04-06 20:27:10 (GMT)
His write-up might be useful. (I don't have it.)
Jasmin Blanchette
2020-04-06 20:28:2 (GMT)
Forget all of that.
Jasmin Blanchette
2020-04-06 20:28:26 (GMT)
KBO also has status! You can use lambda-free KBO with multisets as well. No need for RPO.
Jasmin Blanchette
2020-04-06 20:29:33 (GMT)
See Becker et al.
Alexander Bentkamp
2020-04-06 20:44:40 (GMT)
That will not be enough. We need an order that has the property that if u > t and u > s and the symbol eq does not appear in u, then u > eq(s,t).
Visa
2020-04-07 6:57:3 (GMT)
Aren't ordinal weights for this kind of use cases? In any case all non-Boolean stuff may use any term order and then appear as atoms to RPO layer of =,v. Order of nested formulas hardly matters at all because casing will reduce them to ⊤/⊥.
Actually restricting inferences with =⊥ directly in rules—as Alex did—is cleaner than via selection. I also back off from reinterpreting order of =⊥ as that of ≠⊤. It doesn't pay off to avoid special casing that.
On a second thought CU may neither be worth its complexity. Definitions like {if(⊤,x,y)=x, if(⊥,x,y)=y} will force case split anyway.
Jasmin Blanchette
2020-04-07 7:56:29 (GMT)
To Alex: You could make all symbols except u be at least \omega, and you give a weight of 1 to u.
Jasmin Blanchette
2020-04-07 7:57:3 (GMT)
Replace u by eq. ;)
Jasmin Blanchette
2020-04-07 7:57:8 (GMT)
In fact, here's an easier trick.
Jasmin Blanchette
2020-04-07 7:57:23 (GMT)
You remember that KBO allows weights of 0 for one unary symbol.
Jasmin Blanchette
2020-04-07 7:57:39 (GMT)
What Voronkov made me aware of is that you can instead also have a binary symbol of weight -1.
Jasmin Blanchette
2020-04-07 7:57:49 (GMT)
Or a ternary symbol of weight -2.
Jasmin Blanchette
2020-04-07 7:58:3 (GMT)
More specifically, I should write -\epsilon and -2\epsilon.
Jasmin Blanchette
2020-04-07 7:59:1 (GMT)
In short, if you want, you can give a weight of 0 to "eq". We'd have to work out the exact conditions for this to work (it would probably have to be the minimum of the precedence), but since this eq is always fully applied, it shouldn't be hard.
Alexander Bentkamp
2020-04-07 8:10:29 (GMT)
I don't get it. The weight of eq(s,t) is w(eq) + w(s) + w(t), right?
Petar Vukmirovic
2020-04-07 8:14:41 (GMT)
Visa said:
On a second thought CU may neither be worth its complexity. Definitions like {if(⊤,x,y)=x, if(⊥,x,y)=y} will force case split anyway.
These definitions are common in practice.
Petar Vukmirovic
2020-04-07 8:16:29 (GMT)
@all: What is WPO?
Petar Vukmirovic
2020-04-07 8:16:36 (GMT)
Do you have a reference to that?
Alexander Bentkamp
2020-04-07 8:17:36 (GMT)
Petar Vukmirovic
2020-04-07 8:20:20 (GMT)
Thanks
Jasmin Blanchette
2020-04-07 8:56:10 (GMT)
Alex, you're right. I was thinking about KBO status to solve this, but of course this kicks in only to break ties.
Alexander Bentkamp
2020-04-07 8:59:44 (GMT)
WPO would do it. But is it worth it?
Alexander Bentkamp
2020-04-07 9:1:10 (GMT)
We could also just stick with allowing both positive and negative literals.
Petar Vukmirovic
2020-04-07 9:1:39 (GMT)
I haven't read the WPO paper. I will hopefully do this today.
Alexander Bentkamp
2020-04-07 9:1:46 (GMT)
Or, a third option (I think): We could use Merging Paramodulation instead of EqFact.
Petar Vukmirovic
2020-04-07 9:2:7 (GMT)
If we find a way to implement it in
Petar Vukmirovic
2020-04-07 9:2:12 (GMT)
maybe it is worth it
Alexander Bentkamp
2020-04-07 9:2:47 (GMT)
You mean O(size(s)*size(t)), right?
Alexander Bentkamp
2020-04-07 9:2:51 (GMT)
like RPO?
Alexander Bentkamp
2020-04-07 9:4:40 (GMT)
I guess that's possible, but the paper does not give a lot of details about the implementation. I don't know if there is another paper about the implementation somewhere?
Alexander Bentkamp
2020-04-07 9:7:59 (GMT)
Sophie
2020-04-07 9:9:29 (GMT)
For those that do not have a VU access:
https://link.springer.com/chapter/10.1007%2F978-3-319-96418-8_29
Sophie
2020-04-07 9:10:12 (GMT)
@Alexander Bentkamp By the way, what do you mean by merging paramodulation exactly?
Alexander Bentkamp
2020-04-07 9:13:3 (GMT)
Visa and I would like to use representation (2) from the beginning of this thread. But that may bring trouble with the order because the conclusion of EqFact may not be small enough. However, in the original Bachmair and Ganzinger paper, there is an alternative to EqFact, which is called Merging Paramodulation.
Alexander Bentkamp
2020-04-07 9:15:5 (GMT)
Alexander Bentkamp
2020-04-07 9:16:52 (GMT)
But now I see that there are actually two rules that are needed to replace EqFact. There is also this one:
Alexander Bentkamp
2020-04-07 9:17:2 (GMT)
Alexander Bentkamp
2020-04-07 9:17:41 (GMT)
So maybe this alternative is not so elegant either...
Jasmin Blanchette
2020-04-07 9:27:47 (GMT)
I don't think WPO would be that bad, if it works.
Jasmin Blanchette
2020-04-07 9:28:11 (GMT)
We're talking about one custom instantiation of WPO.
Jasmin Blanchette
2020-04-07 9:28:37 (GMT)
Otherwise, one could hack KBO and have "statues" also for weights, with sum and max being the two operators.
Jasmin Blanchette
2020-04-07 9:29:0 (GMT)
I'm confident this could work.
Alexander Bentkamp
2020-04-07 9:29:33 (GMT)
hack KBO? so you mean turn KBO into WPO?
Jasmin Blanchette
2020-04-07 9:29:44 (GMT)
On a small scale.
Alexander Bentkamp
2020-04-07 9:30:2 (GMT)
Ok, a simple version of WPO.
Jasmin Blanchette
2020-04-07 9:30:6 (GMT)
I don't think adding max/sum statuses to weights is enough to recover WPO.
Jasmin Blanchette
2020-04-07 9:31:12 (GMT)
Regardless, mathematically, we could end up with (more or less) the same result: An order that behaves like KBO except on "eq", where it would (almost) ignore "eq" and take the "max" of the two arguments.
Alexander Bentkamp
2020-04-07 9:32:11 (GMT)
But the implementations of KBO and RPO are quite different because of the subterm checks in RPO.
Jasmin Blanchette
2020-04-07 9:32:29 (GMT)
If the whole thing can be avoided, so much the better, but it would be sad if the calculus were to be needlessly inefficient just because of fears of the order. ;)
Jasmin Blanchette
2020-04-07 9:32:51 (GMT)
I'm thinking theory right now.
Jasmin Blanchette
2020-04-07 9:33:5 (GMT)
The subterm checks of RPO become redundant once you've compared weights.
Jasmin Blanchette
2020-04-07 9:33:18 (GMT)
That's the magic of KBO.
Jasmin Blanchette
2020-04-07 9:33:30 (GMT)
And my trick with "max" instead of "sum" preserves that.
Alexander Bentkamp
2020-04-07 9:33:54 (GMT)
oh, right. That sound nice.
Jasmin Blanchette
2020-04-07 9:34:10 (GMT)
Anyway, stuff to think about.
Alexander Bentkamp
2020-04-07 9:34:16 (GMT)
But I don't think efficiency of the calculus is at stake here.
Jasmin Blanchette
2020-04-07 9:34:30 (GMT)
More its elegance?
Alexander Bentkamp
2020-04-07 9:34:37 (GMT)
Yes
Jasmin Blanchette
2020-04-07 9:35:12 (GMT)
Then indeed it looks to me like there's no easy/elegant way to deal with the orders.
Jasmin Blanchette
2020-04-07 9:35:54 (GMT)
The cleanest is probably WPO.
Jasmin Blanchette
2020-04-07 9:36:29 (GMT)
But then we'd need to lift WPO to lambda-free (or at least ground lambda-free) in HOSup.
Jasmin Blanchette
2020-04-07 9:37:2 (GMT)
It's probably easy, now that we understand how these orders work, with a bit of hand-waving.
Jasmin Blanchette
2020-04-07 9:37:15 (GMT)
(No need for yet another paper!)
Jasmin Blanchette
2020-04-07 9:37:55 (GMT)
By "the cleanest is probably WPO", I mean among the order-based options.
Jasmin Blanchette
2020-04-07 9:38:15 (GMT)
The most elegant solution is probably special calculus rules, like you discuss.
Jasmin Blanchette
2020-04-07 9:38:27 (GMT)
OK, back to the lambda-free paper.
Petar Vukmirovic
2020-04-07 9:44:22 (GMT)
The version that Jasmin described (max for eq) could be implemented in linear time
Petar Vukmirovic
2020-04-07 9:45:44 (GMT)
so for the efficiency of the prover that would be the best
Petar Vukmirovic
2020-04-07 9:45:52 (GMT)
RPO can be used as is, right?
Alexander Bentkamp
2020-04-07 9:46:12 (GMT)
yes
Alexander Bentkamp
2020-04-07 9:49:30 (GMT)
(A) The advantages of using WPO/modified KBO/RPO would be:
- We could make all literals positive, i.e. less case distinctions. (we can still select literals of the form t ≈ ⊥)
- There is only one notation for "negative" literals, not "s≄t" and "(s ≈ t) ≄⊤" , but only "(s ≈ t) ≈⊥".
- We would not need EqRes any more. This would automatically be handled by BoolRw.
(B) But the alternative is not so bad either:
- There are multiple representations of negative literals, e.g., "s≄t" and "(s ≈ t) ≈⊥" and "(s ≈ t) ≄⊤" , but they all can be simplified to "s≄t"
- We would be closer to the implementation, unless we decide to get rid of disequations in the implementation, too.
- We do not restrict the order as much and we don't need to deal with WPO or modified KBO.
Alexander Bentkamp
2020-04-07 9:50:58 (GMT)
I think I have a tendency for (A) right now.
Petar Vukmirovic
2020-04-07 9:55:38 (GMT)
hm... B is also very appealing
Petar Vukmirovic
2020-04-07 9:55:49 (GMT)
What are the cons of it?
Alexander Bentkamp
2020-04-07 10:39:32 (GMT)
The cons of (B) are:
- We must consider a few more cases in the proofs because we have both negative literals and literals of the form
s ≈ ⊥, which also behave like negative literals (e.g. both can be selected) and because we have both positive and negative literals - We have both EqRes and the equality rule of BoolRw, which roughly do the same thing.
- It might be confusing to have so many different clauses that really say the same thing.
Alexander Bentkamp
2020-04-07 10:39:48 (GMT)
Hm, yeah, it is not that bad really.
Alexander Bentkamp
2020-04-07 10:40:4 (GMT)
I have a tendency for (B) now :-D
Petar Vukmirovic
2020-04-07 11:9:52 (GMT)
Ok, so the cons are mostly that the calculus/proof is more inelegant
But the point 3 is not a practical concern, because we will simplify literals to , so we will have only one representation
Jasmin Blanchette
2020-04-07 11:19:27 (GMT)
Of Alex's three cons, point 2 seems to be the most relevant one (inelegant calculus, which hint at the fact that something might be suboptimal). For point 3, I'm not sure what "confusing" means, and point 1 I'd say "ah well that's just the proof". I wouldn't mind ugly proofs as long as the theorems are beautiful. ;)
Alexander Bentkamp
2020-04-07 12:17:53 (GMT)
Ok, let me elaborate on point 2: The BoolRw rule for equality is essentially a superposition inference with the side premise (x ≈ x) ≈ ⊤. For example:
In option (A), the only way to say s ≉ t is (s ≈ t) ≈ ⊥. For clauses of the form C ⋁ (s ≈ t) ≈ ⊥, where s and t are unifiable, BoolRw derives C ⋁ ⊤ ≈ ⊥, which can be simplified into C. This is why we don't need EqRes as a separate rule in option (A).
In option (B), we have at least two ways to say that s is not equal t: s ≉ t and (s ≈ t) ≈ ⊥. The literal (s ≈ t) ≈ ⊥ can be simplified into s ≉ t. Since BoolRw does not work on s ≉ t, we need a separate rule EqRes. But in practice, we would not do any duplicate work because we can always simplify (s ≈ t) ≈ ⊥ into s ≉ t.
Alexander Bentkamp
2020-04-07 12:22:5 (GMT)
Point 3 was referring to Visa's comment: "The lack of representation normalization puzzles me." But maybe I misunderstood this comment. Maybe it just means that we need clear explanations what the standard way to state disequations is? It would not necessarily need to be the only way as long as they all can be simplified into one standard form.
Jasmin Blanchette
2020-04-07 12:24:12 (GMT)
Alex, to me the slight mismatch between theory and practice is puzzling. If you say you can always simplify, that means you don't need BoolRw to handle the case (s ≈ t) ≈ ⊥ in practice. Which means you don't need to handle it in theory either, right?
Jasmin Blanchette
2020-04-07 12:24:38 (GMT)
As long as you make the inference part of the simplification rule part of the calculus (Inf).
Jasmin Blanchette
2020-04-07 12:28:28 (GMT)
Standard superposition has a strict separation between mandatory generating rules and optional simplification rules, but it doesn't have to be like that.
Alexander Bentkamp
2020-04-07 12:29:45 (GMT)
Sure, we can also modify BoolRw to not do inferences on literals of the form (s ≈ t) ≈ ⊥, but that would just make the rule BoolRw more complicated to formulate.
Jasmin Blanchette
2020-04-07 12:32:32 (GMT)
Right.
Alexander Bentkamp
2020-04-07 12:33:7 (GMT)
I think we should separate inferences and simplification rules clearly. The core proof should not deal with simplifications. Our situation is very similar to Sup vs Demod.
Jasmin Blanchette
2020-04-07 12:33:10 (GMT)
But then I'd expect that what's true about the rule's formulation is true about the implementation.
Jasmin Blanchette
2020-04-07 12:33:43 (GMT)
OK.
Alexander Bentkamp
2020-04-07 12:35:26 (GMT)
The implementation can be done exactly as described in the rule. In principle, the implementation of BoolRw would do inferences on literals of the form (s ≈ t) ≈ ⊥, but this would never happen because those literals would be simplified before.
Jasmin Blanchette
2020-04-07 12:36:29 (GMT)
I see. Now I understand the difference between "in theory" and "in practice".
Jasmin Blanchette
2020-04-07 12:36:44 (GMT)
I mistook it for a difference between calculus and implementation, which worried me a bit.
Jasmin Blanchette
2020-04-07 12:37:18 (GMT)
The strict distinction between core calculus and simp rules makes sense here.
Alexander Bentkamp
2020-04-07 12:38:13 (GMT)
Ok, I think I will continue using (B) then.
Petar Vukmirovic
2020-04-07 12:50:55 (GMT)
So to conclude, going for (B) means we use RPO/KBO as they are
Petar Vukmirovic
2020-04-07 12:51:40 (GMT)
and in implementation perform eager simplification of the disequations disguised as equations
Alexander Bentkamp
2020-04-07 13:8:7 (GMT)
Yes, I just added a note on this to the extensions section.
Alexander Bentkamp
2020-04-07 13:12:52 (GMT)
I also saw "Demodulation with negative equations" there. That won't be necessary because s ≉ ⊤ should be simplified into s ≈ ⊥. Then s ≈ ⊥ can be used for Demodulation, but doesn't need to be used for superposition (as all literals of the form s ≈ ⊥).
Petar Vukmirovic
2020-04-07 13:14:13 (GMT)
Ok.. so our criterion for something to be negative is that it is equal to
Alexander Bentkamp
2020-04-07 13:17:6 (GMT)
Yes, both literals of the form s ≉ t and literals of the form s ≈ ⊥ behave like negative literals. But I think we are better of calling only s ≉ t negative. Maybe we need another word that includes negative literals and those of the form s ≈ ⊥.
Alexander Bentkamp
2020-04-07 13:17:16 (GMT)
Yes, both literals of the form s ≉ t and literals of the form s ≈ ⊥ behave like negative literals. But I think we are better of calling only s ≉ t negative. Maybe we need another word that includes negative literals and those of the form s ≈ ⊥.
Alexander Bentkamp
2020-04-07 13:18:12 (GMT)
Maybe "pessimistic"? But maybe we don't need a word for that at all.
Jasmin Blanchette
2020-04-07 13:24:29 (GMT)
Negativoid. ;)
Jasmin Blanchette
2020-04-07 13:28:11 (GMT)
Subpositive.
Jasmin Blanchette
2020-04-07 13:29:35 (GMT)
I agree with Alex that it's better not to call s ≈ ⊥ negative. If you call that negative and s ≈ ⊤ positive, what would you call ⊥ ≈ ⊤? And its negation? ;)
Simon Cruanes
2020-04-07 13:33:10 (GMT)
wow, zulip has become too verbose for me to follow all the details, that's great.
So will y'all write a bit of summary about what the FO+bool calculus will look like? :)
And: since lfHOL and FOL are more or less the same thing but with the former being more convenient, would it make sense to target lfHOL+bool? If one was to write a new superposition prover I'd argue it could be the perfect logic to target.
Petar Vukmirovic
2020-04-07 13:40:29 (GMT)
all of this is more or less implementable in E
maybe it is th perfect logic that Sledgehammer can target?
Simon Cruanes
2020-04-07 13:45:40 (GMT)
I agree, it also nicely matches UF in smtlib (which does have first-class booleans), and you can go a long way with lfHOL otherwise. At least the simply-sorted version.
If I were to write a new prover I'd probably pick that fragment and one of these modern low-level languages (rust, D, nim…)
Michael Färber
2020-04-22 8:5:27 (GMT)
Simon Cruanes said:
If I were to write a new prover I'd probably pick that fragment and one of these modern low-level languages (rust, D, nim…)
I completely agree with Simon here. I have implemented a proof checker in Rust, and it feels great. I have made the experience that the language tends to encourage very clean designs.