2020-01-14 14:7:19 (GMT)
Simon asked me privately what I was doing. I'm working on the saturation framework with Uwe, Sophie, and Simon R. The goal is to replace Section 4 of Bachmair & Ganzinger's Handbook Chapter by a more modular and powerful framework that makes it easy to transfer static completeness of a calculus to dynamic completeness of a given clause prover. We target IJCAR 2020. This will, I hope, also be the basis for a future paper on a splitting framework (think AVATAR).
2020-02-07 15:22:47 (GMT)
By the way, for anyone interested, these are the drafts:
http://matryoshka.gforge.inria.fr/pubs/saturate_paper.pdf (short conference version)
http://matryoshka.gforge.inria.fr/pubs/saturate_report.pdf (longer report version)
2020-02-07 15:26:26 (GMT)
The examples in the paper are great, but maybe it would be useful to have separate documents elaborating some of the instances of this framework, e.g. of resolution and of superposition, including all the details of the completeness proofs? This would probably make it easier to understand how the framework can be used.
2020-02-07 15:36:52 (GMT)
For a second I was hoping it was an analysis of the old Saturate prover from Bachmair and Ganzinger (I think). The one with non-clausal superposition :slight_smile:
2020-02-07 15:37:57 (GMT)
The plan is that we integrate these two calculi (resolution and superposition) to the isabelle framework and then we will write a paper that details their integration. Sorry, you will have to wait a bit @Alexander Bentkamp
2020-02-07 15:46:38 (GMT)
Simon Robillard is already working on the integration of the superposition (but he needs to formalize superposition from scratch in isabelle, including the proof of ground completeness and that is a lot of work) and as soon as I am done with the end of the framework itself, I will complete the integration of the resolution calculus from @Anders Schlichtkrull to the framework, that I started some months ago but had to stop because the framework needed some generalization.
2020-02-07 19:39:1 (GMT)
Just an advice: don't put git URLs that point to master at the end. Point to an URL that has a given hash that will not break in the future if you move the directory elsewhere.
2020-04-09 10:5:26 (GMT)
@Sophie: I'm guessing you don't need the red diffs anymore in the report?
2020-04-09 10:58:20 (GMT)
No, indeed
2020-04-29 16:43:27 (GMT)
@Uwe Waldmann @Sophie Urgent problem. In the paper and report, in Sect. 4.1, we write C ·≻ D implies Gq(C) ⊆ Gq(D). However, typically this requirement won't be met. Consider C = p(a) \/ q(a) and D = p(X). Then Gq(C) = {p(a) \/ q(a)} and Gq(D) = {p(a), p(b), ....
I say "urgent" because I believe it's not too late to update the camera-ready PDF -- according to EasyChair, we can still upload it, and the chairs haven't checked it yet.
2020-04-29 16:45:28 (GMT)
Maybe it's enough to write something like Gq(C) ⊆ Gq(D) \union Red(Gq(D))?
2020-04-29 17:10:1 (GMT)
Oh, I see. The solution is to use the weird same-length subsumption ordering, which is described in an earlier example.
2020-04-29 17:10:9 (GMT)
That's the reason why I want only "term-rewriting subsumption" (i.e., ), not "propositional subsumption" (i.e., ).
.
2020-04-29 17:10:18 (GMT)
Right.
2020-04-29 17:10:27 (GMT)
I just read your mind.
2020-04-29 17:10:57 (GMT)
That's a relief. :) Is there a way we can make this clearer in the paper? E.g. by giving it a name?
2020-04-29 17:11:38 (GMT)
Also, we have a mixture of "subsumption order" and "subsumption quasi-order". Since the latter is more accurate, I'm going to replace all occurrences, unless someone stops me.
2020-04-29 17:11:47 (GMT)
"Preorder" would be fine as well of course.
2020-04-29 17:12:49 (GMT)
As long as we're talking about $\geq$, "quasi-order" is fine; $>$ is an order, though.
2020-04-29 17:14:40 (GMT)
In fact we could have been more liberal in the preliminaries of Sect. 4.1 (in order to admit propositional subsumption), but then the conditions in Lemma 59 get more complicated.
2020-04-29 17:22:0 (GMT)
Jasmin Blanchette said:
That's a relief. :) Is there a way we can make this clearer in the paper? E.g. by giving it a name?
We could either refer back to Ex. 41 and footnote 4 or repeat what has been said there. The ordering $$\cdor>$$ is a tiebreaker; if it is able to compare formulas where there is no tie (which means, they don't have shared ground instances), then we cannot make use of it anyhow. In order to simplify the notation, we assume that compares only formulas where the ground instances are in the subset relation.
2020-04-29 17:42:39 (GMT)
About quasi-ordering: of course. That's why I left it alone before. ;) My memory is bad.
I really wish we had a name other than just "subsumption". We already had one reviewer surprised by the definition and my brain always parses "subsumption" as meaning "propositional subsumption"...
2020-04-29 17:47:4 (GMT)
Anyway, I've now added a reference "(Example 41)", which will help. :)
2020-04-29 20:32:25 (GMT)
It's a bit annoying that we have no guarantee that standard redundancy covers propositional subsumption. Of course, for every redundancy criterion used in practice, makes redundant, but this doesn't follow from (R1)--(R4).
2020-04-30 5:4:28 (GMT)
What bothers me more right now are Examples 63 and 64.
2020-04-30 5:5:4 (GMT)
In Example 63, we can apply forward and backward deletion only to same-length subsumed clauses. This is not a real Otter architecture.
2020-04-30 5:5:29 (GMT)
And Example 64, about RP, uses "subsumption" to mean "propositional subsumption". As does our introduction.
2020-04-30 5:5:58 (GMT)
I am really not happy about using the word "subsumption" to mean two different things. This confuses our readers, but this also confuses us.
2020-04-30 5:8:18 (GMT)
When I have two terms such that , I say that generalizes or that is an instance of . This is very standard I believe -- in any case, I have a paper with Stephan Schulz where we use that terminology (TACAS 2019).
Why not do the same with clauses? The term-rewriting subsumption becomes "generalization", and the propositional subsumption is "subsumption". Then we discuss the relation between the two a bit more.
2020-04-30 5:10:53 (GMT)
I should also add that the Isabelle code for RP already
To come back to @Uwe Waldmann's last comment: it wouldn't bother me. (R1)--(R4) are abstract nonsense. They don't even know anything about the clausal structure.
I'm going to prepare a patch for "generalization"
2020-04-30 5:17:31 (GMT)
OK, I am slightly bothered too, like Uwe. A claim like
First, any redundancy criterion that is obtained by lifting a ground criterion can be extended to a redundancy criterion that supports subsumption without affecting static refutational completeness (\Sect~\ref{sec:lifting}).
in the intro is actually slightly too strong. I'll change "any" to "a".
2020-04-30 6:34:25 (GMT)
I have made my changes in rep_inst.tex. Please have a look and let me know what you think.
2020-04-30 6:35:51 (GMT)
I'm now talking about the "instantiation (quasi-)ordering(s)". I've gone through everywhere and made sure we use the words instance/generalize/subsume in (I belive) the right way.
2020-04-30 7:56:25 (GMT)
Jasmin Blanchette said:
In Example 63, we can apply forward and backward deletion only to same-length subsumed clauses. This is not a real Otter architecture.
No, we apply it to "term-rewriting" subsumed and to redundant clauses. With a reasonable definition of redundancy, that covers alll "propositionlly" subsumed clauses.
2020-04-30 8:10:16 (GMT)
Sorry, you're right. But Example 64 still suffered from the flaw.
2020-04-30 8:18:52 (GMT)
Anyway, please have a look at my change. It's not very drastic. Saying that "f(b) = a" is an instance of "f(X) = a" isn't exactly radical.