Petar Vukmirovic
2020-01-24 21:39:36 (GMT)
Hello everyone!
I have recently implemented recognition of injectivity in E and got super good results (with only one strategy we solve something like 800+ problems).
However, I found a possible source of unsoundness...
Say we have an axiom ![X,Y,Z]: f @ X @ Y = f @ X @ Z ==> Y = Z.
This means that for a particular X f is injective in its second argument.
Now my question for you is Is it sound to state the following axiom:
![X]:?[F]:![Z]: F @ (f @ X @ Z) = Z
or after Skolemization we get sk_inv_f @ X @ (f @ X @ Z) = Z.
That is, it is crucial that we do not forget free variables other than Z (or Y).
@Jasmin Blanchette I think we made a mistake by forgetting this and this is why numbers for E are high
@Ahmed B how do you implement injectivity recognition? You said that it helped you a lot for SH problems.
Do you know how much? Is there something special that you do when you recognize it?
Cheers,
Petar.
Simon Cruanes
2020-01-24 21:56:50 (GMT)
![X]:?[F]:![Z]: F @ (f @ X @ Z) = Z
or after Skolemization we get sk_inv_f @ X @ (f @ X @ Z) = Z.
this seems indeed quite reasonable? The only trap I can think of is that you must ensure sk_inv_f(X) is always applied as such, and not deconstructed (the usual caveat when skolemizing HO formulas in the absence of choice).
Simon Cruanes
2020-01-24 22:0:28 (GMT)
Have you considered trying the prover on satisfiable problems (either some nitpick set of benchmarks, or mutations of unsatisfiable problems)?
Petar Vukmirovic
2020-01-24 22:13:19 (GMT)
I just realized this moments ago
Petar Vukmirovic
2020-01-24 22:13:25 (GMT)
And it is 23:13 in Amsterdam
Petar Vukmirovic
2020-01-24 22:13:40 (GMT)
So I will try it tomorrow
Ahmed B
2020-01-25 7:22:31 (GMT)
Ahmed B how do you implement injectivity recognition? You said that it helped you a lot for SH problems.
Do you know how much? Is there something special that you do when you recognize it?Cheers,
Petar.
I more or less lifted the rule from @Alex Steen's PhD thesis:
Ahmed B
2020-01-25 7:25:27 (GMT)
The one difference in the Vampire rule was that I allowed either literal to be the negative one. For example
f X Y != f X Z \/ Y = Z
Petar Vukmirovic
2020-01-25 9:34:21 (GMT)
Hi Ahmed :)
I am not sure I understand. The direction that Alex has is in his thesis is equality congruence.
That is Y = Z => f @ X @ Y = f @ X @ Z or in clausal form (Y != Z || f @ X @ Y = f @ X @ Z) comes from congurence.
Therefore, it does not hold that symbol sK23 is injective, right?
The other direction would be true. That is f @ X = f @ Y => X = Y or in clausal form f @ X != f @ Y || X = Y implies existence of an inverse.
Am I mistaken?
Ahmed B
2020-01-25 10:17:14 (GMT)
What you say makes sense... :)
Ahmed B
2020-01-25 10:38:56 (GMT)
Petar Vukmirovic
2020-01-25 10:41:11 (GMT)
Yeah, I have an implementation in Zip
and now I am working on an implementation in E
Petar Vukmirovic
2020-01-25 10:41:43 (GMT)
it is pretty rudimentary in Zip
and in E I am trying to do something smart but it seems I am leaking memory like crazy :)
Simon Cruanes
2020-01-25 18:56:22 (GMT)
Feels like you could have started the smart thing in Zipperposition :upside_down:
(a long time ago there was code for detecting AC symbols, I think, btw)