Email Gateway (Aug 22 2022 at 11:49): Email Gateway (Aug 22 2022 at 11:49):From: Daniel Raggi <danielraggi@gmail.com>
In my extensive use of the transfer package I have found that there are
many logical transfer rules that are not included in the original package.
For example, I think only the first one of the following rules is included:
"(op = ===> op = ===> op -->) op /\ op /\"
"(op --> ===> op --> ===> op -->) op /\ op /\"
"(op --> ===> op = ===> op -->) op /\ op /\"
"(op = ===> op --> ===> op -->) op /\ op /\"
In general, for all logical operators, only a very small fraction of all
the combinations of equivalence, implication and reverse implication are
included.
I first noticed this because I have some transformation not going through,
so I added what I needed. After a closer analysis of all the similar
missing rules I've added >20. However, after using transfer' with the
extended set of rules I've realised that there might be a good reason why
they were left out. With complex goal statements, the number of possible
transformations using transfer' method becomes very large. After adding
these rules, the tactics I've been working on (which have to deal with a
lot of transformations and choose a specific one according to heuristics)
have become understandably slow to go through.
So my main questions are:
1) is it known that these transfer rules were left out?
2) if so, where they deliberately left out?
I would appreciate any other comments related to this.
Best,
Daniel
Last updated: Apr 18 2024 at 08:19 UTC