2020-10-06 16:33:46 (GMT)
Heyo, I would like to rename some proof rules before we freeze everything in carbonite for at least a year. Here my suggestions:
lia_generic -> tmp_lia
It's a bad rule and should go away at some point
tautologic_clause -> tautology
duplicated_literals -> contraction
this is she standard name for this
tmp_AC_simp -> tmp_ac_simp
nothing is capitalized otherwise
quantifier_simplify -> qnt_simplify
tmp_quantifier_cnf -> tmp_qnt_cnf
qnt is currently more often used
qnt_simplify -> onepoint
overlap, and it's unclear what it does; _simplify is used for the
rules coming from connect_equiv
Any opinions? /cc @Mathias Fleury @Haniel Barbosa @Pascal Fontaine
2020-10-06 16:37:38 (GMT)
I am not a fan of the tmp_ prefix. Even if it is supposed to disappear, I only believe that when it happens (like tmp_skolemize: it did not disappear either)
2020-10-06 16:39:28 (GMT)
hm right, but then there is a different quality between those rules and other, more well defined rules I think
2020-10-06 16:39:57 (GMT)
from a user point of view, who cares?
2020-10-06 16:40:11 (GMT)
I also always found tmp_ weird.
2020-10-06 16:41:13 (GMT)
@Mathias Fleury so you would be in favor of just keeping it the way it is until it's hopefully gone at some point?
2020-10-06 16:42:5 (GMT)
It's a bit like introducing someone as your new temporary {girl,boy}friend. ;)
2020-10-06 16:42:30 (GMT)
Pascal probably has an opinion about the tmp_ prefix.
2020-10-06 16:43:7 (GMT)
But I doubt the prefix is enough to help with any forward or backward compatibility, really.
2020-10-06 16:44:53 (GMT)
the typical ewiges provisorium
2020-10-06 16:45:6 (GMT)
I would simply drop the tmp_ part
2020-10-06 16:46:43 (GMT)
my intention here is purely cosmetics. versioning and compatibility is a much bigger discussion I think
2020-10-06 16:47:49 (GMT)
Dropping the tmp is purely cosmetic :-)
2020-10-06 16:50:30 (GMT)
@Mathias Fleury I agree. My sentence was related to Jasmins remark. I'm fine with removing tmp_ except for tmp_skolemize. Because this rule is really just a placeholder for a half-implemented feature and only gets emitted when an option marked as experimental is active and skolemize suggest much bigger importance.
2020-10-06 16:50:57 (GMT)
deep_skolemize?
2020-10-06 17:37:36 (GMT)
I also think we should drop tmp_. It looks bad. It's fine to have whatever name that conveys a general rule
2020-10-06 17:37:57 (GMT)
I don't like contraction. In the context of resolution we should use factoring, I'd say
2020-10-06 17:38:46 (GMT)
I like changing qnt_simplify to onepoint
2020-10-06 17:41:34 (GMT)
regarding factoring how strongly does this imply self-unification?
2020-10-06 17:42:1 (GMT)
I guess as strong as contraction
2020-10-06 17:42:20 (GMT)
I can't really say though.
2020-10-07 7:16:57 (GMT)
According to Wikipedia, the two terms are synonyms. I wasn't aware that contraction unifies but apparently it does (or can): https://en.wikipedia.org/wiki/Structural_rule
2020-10-07 7:17:52 (GMT)
I'm pretty sure it didn't unify in Nederpelt & Geuvers's book, but I don't have the book with me. Thus, I'd tend to use contraction for equality and factoring for unification. I don't know which one you have in veriT.
2020-10-07 7:43:40 (GMT)
It's syntactical equality. The rule is somewhat of a macro rule: It doesn't just eliminate one repeated literal, but all.
2020-10-07 7:46:44 (GMT)
I'd go for contraction then.
2020-10-07 11:18:46 (GMT)
Hi All,
the tmp_ was meant to be something that I do not like and that I want to see gone. Haniel contributed a lot to improve the situation. I am not happy that there are still some tmp_ rules there nowadays, and I would see as an achievement that no bad rule is ever used. _generic is not very nice either, but it tells that a pure LIA decision procedure is enough to generate a proof for this. I do not feel strongly about rule names besides this.
Thanks!