2020-10-19 16:5:55 (GMT)
Hello everyone, esp. superposition people :)
A bit an open ended question related to term orders.
One problem we have with the proofs generated by veriT is the order of the arguments of equality i.e. veriT implicitly assures that for $t_1 = t_2$ the term $t_1$ has a lower index than $t_2$ in the term table. Now sometimes we do some prepossessing on $t_1$ which results in a fresh term and hence a flip of the equality without a proof.
I wondered if we could use a term order during printing to avoid this problem. During printing we would just print $t_1 = t_2$ such that $t_1 > t_2$. Now to avoid the problem described above we need that if $f$ is the preprocessing function and $t_1 > t_2$ then $f(t_1) > t_2$. So I guess I'm looking for a as-weak-as-possible property on $f$ to ensure this holds. I guess monotonicity is such property.
Any ideas or pointers?
2020-10-19 16:18:12 (GMT)
Would the printing be robust to the equality rules that rely on the equality orders, like congruence, transitivity...?
2020-10-19 16:25:56 (GMT)
sadly not :( I also think the the instantiation rule can be tackled by this: if we have you don't know much about the potential instances.
2020-10-19 18:4:5 (GMT)
I don't really understand the context, but here's what I think about the property:
Monotonicity means "if then ". It doesn't imply "if then ".
I guess the property you are looking for is . This would imply "if then " if the order is transitive.
What kind of preprocessing operations are we talking about here?
2020-10-20 18:19:37 (GMT)
Oh right. I think the way forward for me would be to have a bit of an ontology of possible rewrite steps.
If I'm not mistaken, compatibility under -operations gives me what I need in some cases.
2020-10-20 18:31:38 (GMT)
Right, if the preprocessing consists of applying rewrite rules, you'll need an order that orients all of your rules and that has compatibility under -operations. Are the terms ground?
2020-10-20 19:29:50 (GMT)
most preprocessing steps can be expressed as rewrite steps, but not all. Terms are also, unfortunately, not necessary ground. It's sadly all quite messy (otherwise it would be easier to fix ^^)
2020-10-20 19:31:20 (GMT)
I'm guessing some preprocessing steps would make terms smaller. But the measure f swings the other way: it would have to become larger. Together with the requirement that f returns a nonnegative number, I believe this is overconstrained already: You can't have arbitrarily large terms be arbitrarily small.
2020-10-22 15:32:13 (GMT)
If I understand this correctly, Hans-Jörg means that is the application of preprocessing. So it's a function from terms to terms, not a measure.
2020-10-22 15:34:7 (GMT)
But I agree that writing < instead of > would be the more natural way to describe the problem.