2020-06-15 19:14:36 (GMT)
Does anyone know if there is a name for the simplification rule that simplifies C[t] ⋁ t ≉ s into C[s] ⋁ t ≉ s if t > s? Is there any prover that implements it or is it not worth the effort?
@Stephan Schulz @Giles @Ahmed B @Uwe Waldmann
2020-06-15 19:34:37 (GMT)
I don't know if it has a name. I've thought something like that in the context of semantic tautology detection (which E does implement), but I've never done the coding. It should not be to difficult to hack - I'm putting it onto my todo-list....
2020-06-15 20:48:6 (GMT)
That's one particular case of contextual rewriting. (Note, however, that there are many simplification rules in the literature that are called "contextual rewriting".)
2020-06-15 21:51:2 (GMT)
We have the rule implemented in Vampire and it's called 'inner rewriting' there, from the options
--inner_rewriting (-irw)
[experimental]
C[t_1] | t1 != t2 ==> C[t_2] | t1 != t2 when t1>t2
default: off
2020-06-16 3:47:51 (GMT)
Hi @Giles, how useful is it in Vampire?
2020-06-16 8:50:43 (GMT)
There are some things that can be solved with it that we cannot solve as easily without it. Given the data I have that's as specific as I can be! Martin Suda implemented it and probably did some tests back in 2015. When we included it in some strategy learning process it was selected to be included in some schedules... whatever that means.
2020-06-16 8:56:10 (GMT)
That sounds good enough to give it a try. Thanks!
2020-06-16 9:5:3 (GMT)
The marketing name for this feature should be "deep rewriting". :slight_smile: