2020-04-14 15:15:3 (GMT)
Here (and in matryoshka/papers/2021-fboolsup) is a sketchy demonstration how to avoid distinguishing clauses from terms.
terms ⊇ clauses.pdf
Inference rules are off the shelf. I preferred symmetric Cases(Simp) over asymmetric because:
– both take 1 formula and leave 2
– only symmetric triggers further simplifications in both left
– both derive "C[⊤]vC[⊥]" in combination to superposition (necessary to transfer cases axiom to type X along a surjection 𝟚↠X)
– only asymmetric needs superpositions into sub-Booleans (proof: previous and the sketch)
– symmetric leaves space for optimizations (unify/𝟚, see thread: Superposition for FOL with interpreted Booleans)
These rules don't wish to challence FOOL preprocessing theorywise in modularity, simplicity or search space size.
2020-04-14 15:37:22 (GMT)
I like it! There are so many things I'd like to discuss, but maybe we should start with Cases, as you've already started.
Somehow I thought that asymmetric might be better, but you make very good points for the symmetric one. This is very much related to the "top-down" and "bottom-up" approaches we talked about in the "Calculus proposal" thread:
top-down = symmetric
bottom-up = asymmetric
Maybe @Petar Vukmirovic can say something about what his experiments say about this if he has tried it.
2020-04-14 15:41:2 (GMT)
Visa's symetric rules are simplifications
2020-04-14 15:41:29 (GMT)
Yes, that is the crucial advantage of the symmetric Cases.
2020-04-14 15:41:37 (GMT)
if you look at PAAR submission, best behaving Cases is the one that simplifies
2020-04-14 15:43:37 (GMT)
Ok, I wasn't aware of this. Then let's do that of course!
2020-04-14 15:45:27 (GMT)
but the difference is not huge
and there is one passage about order that worries me
2020-04-14 15:45:56 (GMT)
Yeah, but I hope that we can fix that :-)
2020-04-14 15:47:17 (GMT)
I think it is quite modular. We just have combine the best of mine with the best of Visa's. But first we need to figure out what the best parts of each are...
2020-04-14 15:50:52 (GMT)
What is super cool about Visa's approach is that he cases only subterms that have arguments
2020-04-14 15:51:15 (GMT)
this seems like a reasonable restriction
2020-04-14 15:55:16 (GMT)
really? where is that mentioned?
2020-04-14 15:56:47 (GMT)
ohh .. I mixed it up
2020-04-14 15:56:59 (GMT)
term must be basic to superpose from, but not to superpose into
2020-04-14 15:57:22 (GMT)
I guess both options are possible in principle. We can start casing innermost first or outermost first.
2020-04-14 15:58:0 (GMT)
In Visa's initial post here, it sounds like he wants to go for outermost first:
– only asymmetric needs superpositions into sub-Booleans (proof: previous and the sketch)
2020-04-14 15:58:23 (GMT)
Let me see the numebrs from PAAR to let you know which one was better
2020-04-14 15:59:17 (GMT)
outermost and all were best.
2020-04-14 15:59:23 (GMT)
indeed
2020-04-14 15:59:39 (GMT)
all is a bit surprising...
2020-04-14 16:0:17 (GMT)
there are some strange cases
weher all is needed
2020-04-14 16:0:28 (GMT)
liek f(f(f(a))) = a or something like that
2020-04-14 16:0:35 (GMT)
where f is a bool fun
2020-04-14 16:2:14 (GMT)
If you have a counter-example where outermost does not work, we need to know! I have a completeness proof in mind, but if you have a counter-example, that means it is flawed!
2020-04-14 16:6:12 (GMT)
maybe f(f(f(a)))!=f(a)? That's something Visa mentioned to me once.
2020-04-14 16:7:28 (GMT)
Oh, that's a higher-order example, I guess!
2020-04-14 16:11:31 (GMT)
there was a different counterexample
let me look in the raw data
2020-04-14 16:18:41 (GMT)
but bear in mind that those counterexamples were with my ad-hoc calculus
maybe something you do takes care of it
2020-04-14 16:19:49 (GMT)
Alex, why is f(f(f(a))) != f(a) HO? I looks very FOOLish to me.
2020-04-14 16:25:1 (GMT)
Ok I realized something
for my PAAR evaluation extensionality rules were on
those rules will take care of some incomplteness that is present in my approach
I will reevaluate different versions of simplification rule, with different modes for boolean subterm seelection
and let you know
2020-04-14 16:25:13 (GMT)
StarExec should evaluate in in ~1h
2020-04-14 16:34:58 (GMT)
Right, it's foolish.
2020-04-14 16:44:11 (GMT)
It is running, I will get back to you :slight_smile:
2020-04-14 17:15:3 (GMT)
This approach with the symmetric Cases is very close to FOOL now.
Visa wrote:
These rules don't wish to challence FOOL preprocessing theorywise in modularity, simplicity or search space size.
So how do we challenge FOOL? The idea was to be lazy, right?
2020-04-14 17:20:47 (GMT)
That is true... I have to admit that the document was not the easiest to follow
2020-04-14 17:21:19 (GMT)
I did not understand if he would aggressively simplify equations of the kind
2020-04-14 17:21:28 (GMT)
to
2020-04-14 17:27:19 (GMT)
Yes, the proof mentions this as a simp rule, which might be missing above.
2020-04-14 17:29:24 (GMT)
Of course, these simp rules do not need to be applied aggressively. We just must not forget about them completely. I don't know if that's a good strategy though.
2020-04-14 17:32:13 (GMT)
It was meant to be part of simplifying formula with ≤1 unknown p to ⊤, ⊥, p or ¬p. Explicitely
⊤≈p ⟶ p
⊥≈p = ¬p
p≈p ⟶ ⊤
p≈¬p ⟶ ⊥
and similarly for v. For example p := s≈t.
2020-04-14 17:35:55 (GMT)
Was my document difficult to read because it was not explicit enough?
2020-04-14 17:42:20 (GMT)
Visa said:
Was my document difficult to read because it was not explicit enough?
Don't worry about it. Maybe it was only me.
2020-04-14 17:42:43 (GMT)
It is still an early phase, so do not spend to much time on spelling it out
If I do not get something I will ask here
2020-04-14 17:54:3 (GMT)
There is one thing that Visa and me implemented ages ago and that is non-agressive simplification
In particular, when CasesSimp is applied, if it is applied in a loop, it will result in the maximally simplified set of clauses
2020-04-14 17:54:31 (GMT)
To mitigate this, we take out all (or only one, based on selection) boolean subterm and then stop
2020-04-14 18:49:2 (GMT)
@Alexander Bentkamp I found a counterexample: SYO040^1.p
2020-04-14 18:49:14 (GMT)
It might be because of the way bool simp is implemented
2020-04-14 19:3:25 (GMT)
cmd line that gives up:
./zipperposition.exe ~/Documents/TPTP-v7.3.0/Problems/SYO/SYO040^1.p --mode=ho-pragmatic --max-inferences=7 --ho-max-app-projections=1 --ho-max-elims=0 --ho-max-rigid-imitations=2 --ho-max-identifications=0 --ho-unif-max-depth=2 --boolean-reasoning=cases-simpl --bool-subterm-selection=M --ext-rules=off --kbo-weight-fun=lambda-def-invdocc --ho-prim-enum=none --ho-prim-max=2 --tptp-def-as-rewrite --rewrite-before-cnf=true --ho-unif-level=pragmatic-framework -q "1|const|conjecture-relative-var(1,s,f)" -q "1|prefer-processed|pnrefined(1,1,1,2,2,2,0.5)" -q "1|prefer-sos|staggered(1)" -q "2|prefer-fo|default" -q "2|defer-sos|staggered(2)" --ho-fixpoint-decider=true --ho-pattern-decider=true --ho-solid-decider=true --select=e-selection9 --solve-formulas=true --sup-at-vars=true --sup-at-var-headed=true --dupsup=true --lambdasup=2 --sine=50 --sine-tolerance=1.3 --sine-depth-max=3 --sine-depth-min=1
2020-04-14 19:3:40 (GMT)
change bool-subterm-selection to A for any
2020-04-14 19:4:27 (GMT)
Both outermost and all fail?
2020-04-14 19:4:37 (GMT)
no no
2020-04-14 19:4:50 (GMT)
any (A) suceeds
2020-04-14 19:4:58 (GMT)
outermost (L) fails
2020-04-14 19:5:3 (GMT)
innermost (M) also fails
2020-04-14 19:9:2 (GMT)
OK. It is because of the way it is implemented.
2020-04-14 19:9:32 (GMT)
This is the debug output of Zip:
0.003[zip.saturate]
given (before simplification):
[h (f (f (f x))) ≠ h (f x)*]/id:3/depth:0
0.003[zip.saturate]
all_simplify([h (f (f (f x))) ≠ h (f x)*]/id:3/depth:0)=
0.003[zip.saturate]
[x ∨ h (f (f (f false))) ≠ h (f false)*]/id:4/depth:0,
[¬x ∨ h (f (f (f true))) ≠ h (f true)*]/id:5/depth:0
0.003[zip.saturate] ### step 0 ###
0.003[zip.saturate]
given (0 steps, penalty 1):
[x ∨ h (f (f (f false))) ≠ h (f false)*]/id:4/depth:0
0.004[zip.saturate] inferred new clauses: []
2020-04-14 19:10:0 (GMT)
Original clause id:3 will get simplified into id:4 and id:5
2020-04-14 19:10:14 (GMT)
then id:4 gets chosen
2020-04-14 19:10:22 (GMT)
nothing gets inferred
2020-04-14 19:10:39 (GMT)
and no subterms are ever simplified again in id:4
2020-04-14 19:11:6 (GMT)
this is because of the mechanism I explained above that Visa and me implemented
2020-04-14 19:12:30 (GMT)
Ok, good, that means that our completeness proofs do have a chance to hold :-)
2020-04-14 19:13:52 (GMT)
But it is still true that we should be careful how we simplify
and in general, I think what Visa and me implemented was a good idea
2020-04-14 19:13:55 (GMT)
Order of simplifications—including CasesSimp—is irrelevant, isn't it. That is another difference to asymmetric version, see (5).
About examples (eligible underlined):
(1:cycle) Refuting f(f(fa))≠fa (f∈𝟚→𝟚) is nice by unification mod Booleans.
(2:fyi) Refuting Pa v b̲=a, P̲b̲, ¬Pa v ¬̲P̲a̲ (Pa<b∈𝟚) is impossible by unification mod Booleans (without simplification—blockable by obfuscating example). Here superposition into sub-Booleans is disallowed and intermediate conclusion after 2 steps deleted as tautology.
(3:no𝟚sup) Fact C[a⇔b], ¬avb̲, av¬̲b̲ ⊨ C[T] seems to show that superposition into subformulas never truly helps completeness.
(4:surjection) f̲(̲b̲x̲)̲=x, t≠s≠r≠t (f∈𝟚↠T, t∈T, x variable) shows that "C[p] ⊢ C[⊤]vC[⊥]" is necessary:
f̲(̲b̲x̲)̲=x (=:α) ⊢ f⊥=x v b̲x̲=⊤ (=:τ), f⊤=x v ¬̲b̲x̲ (=:φ) none of which can superpose with t≠s.
CasesSimp: sup. of τ and φ gives f̲⊥̲=x̲ v f⊤=x.
Cases: sup. of τ and α gives f̲⊥̲=x̲ v f⊤=x.
(5:cases↯max) Modification f̲(̲¬̲b̲x̲)̲=x, t≠s≠r≠t shows that asymmetric Cases restricted to maximal subformulas is incomplete. The "τ" here simplifies to f⊥=x v ¬̲b̲x̲ which is assumed not to rewrite conditionally (otherwise it isn't extension of standard superposition). Not casing bx is the source of incompleteness.
2020-04-14 19:16:9 (GMT)
So problem with non-aggressive simplification is that it stops if generative inferences run out even though simplification itself could create more of them. Did I understood corretly?
2020-04-14 19:16:47 (GMT)
Visa said:
So problem with non-aggressive simplification is that it stops if generative inferences run out even though simplification itself could create more of them. Did I understood corretly?
Well, it stops because it did a single step of simplification (which is just casing the minimal subterm)
2020-04-14 19:16:55 (GMT)
minimal as in innermost leftmost
2020-04-14 19:17:24 (GMT)
it is the single-step-simplify kind of rules that we have implemented just for this purpose if you remember
2020-04-14 19:17:39 (GMT)
if it was not single-step then everything would get maximally simplified
2020-04-14 19:17:58 (GMT)
and basically selection function (innermost or outermost) would not matter
2020-04-14 19:22:47 (GMT)
I see. So that is incomplete. Why not delete the original clause as part of a generational inference?
2020-04-14 19:24:35 (GMT)
In this case the original clause is deleted
2020-04-14 19:24:39 (GMT)
that is the cause of the problem
2020-04-14 19:24:51 (GMT)
it is CasesSimp, not Cases
2020-04-14 19:40:15 (GMT)
My main worry is now that we are just reinventing FOOL here... Even if we do the simplifications a bit slower than normally, does this really make a difference?
2020-04-14 19:42:13 (GMT)
When you say this what do you mean
2020-04-14 19:42:21 (GMT)
In short, we are _very_ different than FOOL
2020-04-14 19:42:35 (GMT)
to begin with in our laziness and in the fact that we do not preprocess anything
2020-04-14 19:47:32 (GMT)
But if we apply symmetric Cases aggressively in the beginning, that would amount to FOOL, or not?
2020-04-14 19:49:48 (GMT)
that is true
2020-04-14 19:49:58 (GMT)
but we do not want to do that :slight_smile:
2020-04-14 19:51:12 (GMT)
Can we come up with any examples where FOOL is horrible and lazyness would pay off?
2020-04-14 19:54:11 (GMT)
I think you had some TPTP examples where Satallax really benefited from not using CNF, right?
2020-04-14 20:17:39 (GMT)
Maybe something like h(p = q) != h(q = p) where p : bool, q : bool, h: bool -> i. Equivalences are bad for CNF, right?
2020-04-14 20:50:16 (GMT)
true
2020-04-14 20:51:27 (GMT)
and also unrolling that is done in FOOL is exponential in size of terms
2020-04-14 20:51:45 (GMT)
if we are able to control that explosion then we really gain something
2020-04-14 20:52:1 (GMT)
for example if you have p(FOOL_TERM1) & p(FOOL_TERM2)
2020-04-14 20:52:30 (GMT)
FOOL_TERM1 and FOOL_TERM2 will be unrolled independent of each other
2020-04-14 20:52:49 (GMT)
if oyu have further nesting inside FOOL_TERMi then you could really benefit from our approach
2020-04-15 8:1:44 (GMT)
Actually, concerning symmetric vs asymmetric Cases, we can have both: If we require only the asymmetric Cases as an inference rule, the symmetric Cases can still be a simplification rule. Then a heuristic could decide which one to use. If symmetric Cases is applied, the original clause becomes redundant and hence asymmetric Cases would no longer be needed for that clause.
2020-04-15 8:10:50 (GMT)
This is what we have right now in Zip, minus the heuristic that decides whether to simplify or infer
2020-04-15 8:11:26 (GMT)
Are you now convinced that our approach is significantly different than FOOL? :slight_smile:
2020-04-15 8:19:43 (GMT)
Having the option to use either symmetric or asymmetric Cases is definitely different from FOOL.
2020-04-15 8:31:26 (GMT)
True. If we managed to have simplification with some selection functions + casing only non-logical terms that would already be an improvement
2020-04-15 8:35:15 (GMT)
To be honest, my approach does apply Cases not only to uninterpreted predicates: ≈Elim, ∀Elim, and ∃Elim are also casing rules.
2020-04-15 8:38:36 (GMT)
But from my point of view, it is not clear whether symmetric or asymmetric Cases is better. Symmetric has many advantages as listed in Visa's first post here. The advantages of asymmetric are:
f(p,q)=c will eventually result in f(⊥,⊥)=c, f(⊥,⊤)=c, f(⊤,⊥)=c, f(⊤,⊤)=c with symmetric Cases, but in f(⊥,⊥)=c, f(⊥,q)=c, f(p,q)=cwith asymmetric Cases if we use the idea of "selecting" boolean subterms.2020-04-15 8:39:44 (GMT)
@Visa Do you think it makes sense to try to support both symmetric Cases and asymmetric Cases?
2020-04-15 8:42:18 (GMT)
Alexander Bentkamp said:
To be honest, my approach does apply Cases not only to uninterpreted predicates: ≈Elim, ∀Elim, and ∃Elim are also casing rules.
But that is already better than casing all formulas, right?
2020-04-15 9:19:37 (GMT)
I guess, but symmetric Cases also has its benefits. I think we should try to support both theoretically and then evaluate to see which one is better. Since your PAAR results were really close to each other, I think evaluating this again under different parameters and benchmarks might give different results.
2020-04-15 10:2:44 (GMT)
I see.
2020-04-15 14:46:58 (GMT)
I lack context, is this building on FOL or lfHOL?
2020-04-15 14:49:25 (GMT)
FOL
2020-04-15 14:50:14 (GMT)
The idea, Simon, is that the lambda-free will be built on top of that.
2020-04-15 14:51:57 (GMT)
If you look at the JAR submission linked below, Alex wants to replace FOL in Section 4.2 with FOOL. Then the HO stuff comes in 4.3 like before, and the nonground HO stuff in 4.4.
2020-04-15 14:52:10 (GMT)
Oh. I thought I saw a and that it was curried application.
2020-04-15 14:52:47 (GMT)
But in any case, the goal is to get a merge of FOOL with delayed clausification, in a nutshell?
2020-04-15 14:53:34 (GMT)
FOOL can mean many things. I use it to mean "FOL with interpreted Booleans".
2020-04-15 14:54:47 (GMT)
As I see it, the goal is to get a generalization of Bachmair & Stuber to support interpreted Bools.
2020-04-15 14:54:55 (GMT)
I meant the original "the vampire and the fool" paper.
2020-04-15 14:55:11 (GMT)
Yes, but even in that paper FOOL can mean many things.
2020-04-15 14:55:20 (GMT)
Yes but it also involves delayed clausification? Or is it still a generalization since B&S assumes a clausified input?
2020-04-15 14:55:41 (GMT)
I haven't read it closely, but there's a translation, there's a rule in there.
2020-04-15 14:56:2 (GMT)
The FOOL paper perform preprocessing.
2020-04-15 14:56:19 (GMT)
Oops, I meant G&S, not B&S.
2020-04-15 14:56:53 (GMT)
No, the whole point of G&S is to perform nonclausal reasoning.
2020-04-15 14:56:59 (GMT)
Which is good.
2020-04-15 14:57:15 (GMT)
Ah that makes more sense. (the G&S for delayed CNF)
2020-04-15 14:57:15 (GMT)
G&S is "superposition for nonclausal FOL".
2020-04-15 14:57:39 (GMT)
Now the goal is to go "FOOL" (the logic, not the translation or whatever else is in that FOOL paper).
2020-04-15 14:58:26 (GMT)
Still, to clarify:
Is it accurate to state that the new calculus would be able to deal with formulas that have booleans subterms, boolean formulas, etc. without requiring preprocessing? A truly complete calculus that goes end-to-end? :)
2020-04-15 14:58:34 (GMT)
I'm doing the marketing, while Alex, Sophie, Visa et al. do the actual work. ;)
2020-04-15 14:58:45 (GMT)
Yes, that's exactly that.
2020-04-15 14:59:23 (GMT)
To go HOL, we just need the ground calculus.
2020-04-15 14:59:25 (GMT)
That's very interesting. It would also be very nice for outputting proofs, I imagine, since there would be one calculus with fixed rules.
2020-04-15 14:59:38 (GMT)
But since it's interesting in its own right, it ended up becoming its own project/paper.
2020-04-15 14:59:58 (GMT)
Proofs of clausifications, indeed.
2020-04-15 15:1:33 (GMT)
That's very exciting, thanks for the clarifications. Sounds to me like that would help integration with proof assistants (besides the part where it handles better set problems and similar things where you don't want eager clausification).
So @Petar Vukmirovic has already implemented that?
2020-04-15 15:22:1 (GMT)
Kind of. Petar and Visa will be submitting a paper at PAAR about this kind of stuff -- but without completeness.
2020-04-15 15:22:20 (GMT)
Haven't you read it yet? It's in the Matryoshka repository somewhere.
2020-04-15 15:23:5 (GMT)
I've been a bit swamped by y'all's talk here!! Which is a good thing. I'll take a look, I also looked at the .pdf at the beginning of the thread.
2020-04-15 16:8:19 (GMT)
Answer to Alex: Restricting casing by the term order (not substructure relation as I thought) is great idea. That erases my earlier marginal preference.
However the goal is to get conclusions, not just a swamp of possibilities! I'm almost sure that doubling the casing techiques nowhere near doubles the benefits. Even if asymmetric completeness easily implies symmetric, it is very likely that there's more useful topics (e.g. examples) to discuss within the limited space.
2020-04-15 16:16:13 (GMT)
It might not double the benefits, but we also do not know which one is better. So we have to evaluate that, don't we?
2020-04-15 16:17:25 (GMT)
Or do you think there are more important choices to evaluate?
2020-04-15 16:19:33 (GMT)
If we reach any conclusion today, we can systemize it and I can implement and evaluate whatever we systemized
2020-04-15 16:41:22 (GMT)
Yes: evaluate both, create theory for the better one. Though it sounded like the evaluation might end up "statistically" inconclusive.
2020-04-15 16:46:38 (GMT)
Ok do we have very clear descriptions of opposing approaches
2020-04-15 16:46:48 (GMT)
Do we have benchmarks on which to evaluate?
2020-04-15 16:47:15 (GMT)
The logic is quite exotic and getting enough benchmarks to make conclusions is going to be hard
2020-04-15 16:53:45 (GMT)
Well currently we have Alex' and my proposals only.
2020-04-15 16:54:9 (GMT)
UF in smtlib? It's big benchmarks though typically.
And you need to deal with let and ite, but that's also part of the original FOOL paper.
2020-04-15 16:56:9 (GMT)
Well, let and ite are out of our scope.
2020-04-15 16:57:1 (GMT)
We can just axiomatize them or unfold them
2020-04-15 16:57:12 (GMT)
You can still preprocess them away! :)
Note that imho ite is a central part of having first-class booleans, and will be in a lot of real use cases (including benchmarks from proof assistants, program verification, etc.).
2020-04-15 17:3:31 (GMT)
Oke, you are right.. we can probably preprocess them
2020-04-15 17:3:46 (GMT)
Does Zip parse SMT?
2020-04-15 17:4:31 (GMT)
It parses tip, but it would be doable to parse smt2.6 instead using Dolmen (which is why we discussed it earlier with @Guillaume Bury !)
2020-04-15 17:13:19 (GMT)
Ok thanks!
I will take a look at this
2020-04-15 17:32:40 (GMT)
@Visa Your calculus seems to be able to omit some Cases inferences that mine needs. For example, in a clause p ≈ q where p > q, you do not apply Cases, right? I do need to do that because p might be reduced by a rule p → ⊥ that stems from the additional part of the rewriting system that is not produced by clauses. How do you handle this?
2020-04-15 17:34:31 (GMT)
@Alexander Bentkamp what is the status on simplifying literals that have equations on the top level
2020-04-15 17:35:5 (GMT)
can we normalize them all to and
2020-04-15 17:36:6 (GMT)
and for top-level predicates and
2020-04-15 18:24:16 (GMT)
No, I would like to normalize to and , but this is only for the order. For selection and superposition, can behave like a negative literal.
2020-04-15 18:34:31 (GMT)
Ok, ok..
Proposal: we apply view function when we pass the terms to order, and view views negative literals as
and in the implemenetation we have a single representation for both your and Visa's calculus
2020-04-15 18:51:28 (GMT)
Ok, wait. We have only spoken about Cases so far. There are plenty of other differences between Visa's proposal and mine:
(1) clauses are terms / clauses are multisets of literals
(2) order is WPO / multiset order on clauses and literals, KBO or RPO on terms
(3) equality and disjunction are commutative and associative / term-equality and term-disjunction behave like other symbols
I don't think we need to evaluate these differences. We should first try to agree on one option for each of these.
2020-04-15 18:53:28 (GMT)
(4) all literals are equations / literals can be a disequation
2020-04-15 18:53:50 (GMT)
Sure... we still need to systemize things clearly
2020-04-15 18:54:24 (GMT)
I was just thinking about this one things which theoretically might not seem important, but is in practice it is
2020-04-15 19:6:55 (GMT)
I like Visa's variants of (1) and (4). They are more elegant and purely representational. In the implementation we can make different decisions if Petar prefers.
We need to talk about (2) and (3).
Concerning (2), I think that it should be possible to use the multiset order on clauses and literals, also in Visa's calculus, even though clauses are considered terms. If it is possible, then I think we can agree that it would be better to keep the traditional approach to the clause order and to avoid WPO.
Concerning (3), I think it is just inconvenient to have associative connectives inside terms for the implementation. The term order would need to respect the associativity somehow.
2020-04-15 19:12:11 (GMT)
I think it is pretty clear that we should not represent clauses as terms in implementation
2020-04-15 19:12:42 (GMT)
As for WPO, I am all for avoiding it
2020-04-15 19:12:59 (GMT)
but if it need be, we can see how to efficiently implement it
2020-04-15 19:13:30 (GMT)
The problem is that to make further decisions we need to evaluate the approaches
2020-04-15 19:13:48 (GMT)
But that is quite hard to do when we do not have all those details worked out
2020-04-15 19:14:20 (GMT)
I was also unaware that in Visa's approach clauses are terms.
Word clause does not even appear in the doc :slight_smile:
2020-04-15 19:16:43 (GMT)
It's the title of this thread :smiley:. Clauses are not mentioned because if clauses are terms, we can just call them terms :smiley: .
2020-04-15 19:18:36 (GMT)
yeah, that I did not read :slight_smile:
2020-04-15 19:19:20 (GMT)
I probably know it because I exchanged some emails with Visa before.
2020-04-15 19:21:15 (GMT)
But how do you propose we continue?
2020-04-15 19:22:4 (GMT)
What are the things that you want to evaluate?
I can also do the the following: find the way to parse SMTs to get more problems
and then reevaluate PAAR on them
2020-04-15 19:22:29 (GMT)
this can tell us more about CasesSimp vs Cases
2020-04-15 19:22:37 (GMT)
and which approach is better in that way
2020-04-15 19:22:46 (GMT)
I can also experiment with Boolean selection functions
2020-04-15 19:23:9 (GMT)
Concerning asymmetric Cases vs symmetric Cases, I would suggest to go for the approach which allows for both. It is not much more complicated than what I already have in my proposal.
2020-04-15 19:24:59 (GMT)
Then we can do the evaluation as part of our paper. If we evaluate now and then go for one of the two approaches, we will have difficulties to report on the results of our initial evaluation. And if we don't report about it, then it's not really useful, right?
2020-04-15 19:28:34 (GMT)
If both approaches make sense and it's not obvious which one is better on paper, it makes sense to report both if that's not too much work. (I wouldn't worry about space because you can have a tech report / journal article with all the details.) If nothing else, it will save others from redoing the work.
2020-04-15 19:29:54 (GMT)
Ok..
2020-04-15 19:29:55 (GMT)
A lovely example is Alex (et al.)'s IJCAR 2018 paper, about -free superposition. He defined four calculi: intensional vs. extensional, nonpurifying vs. purifying.
2020-04-15 19:30:17 (GMT)
So we will ahve a single calculus with two approaches to casing
2020-04-15 19:30:30 (GMT)
Like B&G and merging paramodulation / equality factoring?
2020-04-15 19:30:33 (GMT)
Since full HOL is extensional, we had a hunch this would be the winner, but for nonpurifying vs. purifying we had to evaluate.
2020-04-15 19:31:34 (GMT)
The winner ended up being extensional nonpurifying in our CADE 2019 paper.
2020-04-15 19:31:54 (GMT)
What I initially understood is that we will have two quite different calculi with different representation of primitivies / orders / etc.
2020-04-15 19:32:4 (GMT)
Now I completely agree with you that we should have both
2020-04-15 19:32:5 (GMT)
But now, at IJCAR 2020, there's a paper by Ahmed Bhayat and Giles Reger that's based on the intensional nonpurifying calculus. That was unexpected, but it's quite satisfying.
2020-04-15 19:45:31 (GMT)
Petar Vukmirovic: Like B&G and merging paramodulation / equality factoring?
I think it's even better than that: It's just using a simplification rule or not.
2020-04-16 11:18:23 (GMT)
I'm flattened how miserably I failed to communicate my main points. There was just one (1) thing I wanted to demonstrate. Namely, clauses can be terms without sad drawbacks (so far).
I'm not interested in the theory per se so every major suggestion—including clauses⊆terms—is supposed to be a practical advantage. (I found the distinction a hindrance when coding Cases.)
WPO was for completeness proof only. I'll make that and the corresponding implementation strategy explicit in the sketch.
2020-04-16 11:44:18 (GMT)
Yeah, our communication is not going well right now. Of course, if we were all in one office, this would be much easier. Maybe we should try Skype meetings? Maybe once every day?
2020-04-16 11:46:42 (GMT)
Would 11 am be ok for you?
2020-04-16 12:28:17 (GMT)
For me that idea is perfect! :slight_smile:
2020-04-16 12:33:14 (GMT)
Yes.
2020-04-16 12:34:51 (GMT)
Visa said:
I'm not interested in the theory per se so every major suggestion—including clauses⊆terms—is supposed to be a practical advantage. (I found the distinction a hindrance when coding Cases.)
I think that practically representing clauses as terms is going to be a huge development effort -- basically all the basic inferences now work on clausal structure, and all of them would have to change.
Also, why do you think this was a problem while coding Cases?
2020-04-16 12:34:55 (GMT)
Doesn't 11 AM collide with Petar's breakfast? ;)
2020-04-16 12:35:4 (GMT)
It's much earlier :slight_smile:
2020-04-16 12:43:20 (GMT)
Especially mistaking the 2 equalities as the same lead initially to easy completeness bugs. Different clauses, literals and terms imply different iteration interfaces imply more learning.
2020-04-16 12:44:59 (GMT)
Conceptually clause interface will be subsumed by term interface. But I don't know if that it feasible in Zipperposition.
2020-04-16 12:49:22 (GMT)
What do you mean mean with mistaking 2 equalities the same?
What I think is the biggest problem here is that to support the new rule, we need to change how all the other ones work.
Instead, I think it is better to make the current architecture work with the new rule than to change the prover architecture to fit the new calculus
2020-04-16 13:28:31 (GMT)
I think Visa means abolishing the distinction between in literals and "bold " in terms of type Bool.
2020-04-16 13:28:41 (GMT)
2020-04-16 13:28:59 (GMT)
Hm, \pmb (poor man's bold) doesn't work so well here. ;)
2020-04-16 13:31:18 (GMT)
BuiltIn.Eq is not equation literal. There was some function, say mk_prop, that made true propositional atom. But mk_prop(Term.App(BuiltIn.Eq, [t,s])) didn't make literal t≈s because the equalities differ.
We can implement what is most convenient to us. The duplication of =,v is easiest being already present but ideally there would not be such duplication, right? If so, theory should not force it.
2020-04-16 13:44:33 (GMT)
Ahhh. Ok...
The way it is currently dealt with is that everything is normalized to an equation literal if it can be
2020-04-16 13:46:7 (GMT)
We can discuss different ways to normalize things, as Alex and I mentioned previously
2020-04-16 13:58:32 (GMT)
Just ignore my post if it makes no sense, but from my point of view the duplication of and is difficult to avoid, esp. in the implementation but also in theory. For example, the inner, bold versions are not commutative and (for ) associative, whereas the outer ones are. Generalizing orders (KBO etc.), data structures, and so on to support associative-commutative operators is quite difficult in the context of superposition. That's the reason why it's not usually done.
2020-04-16 13:59:4 (GMT)
(E exploits commutativity and perhaps associativity when it detects it, in its redundancy criterion, but that's it.)
2020-04-16 13:59:28 (GMT)
Jasmin Blanchette said:
(E exploits commutativity and perhaps associativity when it detects it, in its redundancy criterion, but that's it.)
Indeed, in the exact same way that iProver does
2020-04-16 13:59:32 (GMT)
SMT stuff
2020-04-16 13:59:51 (GMT)
Keeping the two separate makes it easier to remain graceful.
2020-04-16 14:0:13 (GMT)
Jasmin Blanchette said:
Keeping the two separate makes it easier to remain graceful.
That was also my feeling
2020-04-16 14:0:49 (GMT)
(On the other hand, if the two layers can be merged gracefully, and it can be implented, I'm not against.)