Интерактивная математическая система доказательства
Вот подход dplyr:
library(dplyr)
df %>%
group_by(userID) %>%
mutate(date = as.Date(date),
l45 = lead(between(c(0, diff.Date(date)), 320, 410), default = FALSE))
# A tibble: 10 x 4
# Groups: userID [4]
loginID userID date l45
<int> <fct> <date> <lgl>
1 1 a 2017-01-03 TRUE
2 2 b 2017-01-12 TRUE
3 3 c 2017-01-14 TRUE
4 4 d 2017-01-19 FALSE
5 5 d 2017-10-18 FALSE
6 6 a 2017-11-30 FALSE
7 7 b 2017-12-09 FALSE
8 8 c 2017-12-17 FALSE
9 9 a 2017-12-30 FALSE
10 10 b 2018-01-15 FALSE
4 ответа
ACL2 is notorious -- we used to say it was an expert system, and so could only be used by experts, who had to learn from Warren Hunt, J Moore, or Bob Boyer. The thing you need to do in ACL2 is really really understand how the proof system itself works; then you can "hint" it in directions that reduce the search space.
There are several other systems that can help with this kind of thing, though, depending on what you're trying to do.
If you want to work with continuous math or number theory, the ideal is Mathematica. Problem is you can buy a used car for the same amount of money (unless you can qualify for an academic license, a far better deal.)
Something similar, and free, is Open Maxima, which is an extension of Macsyma. That page also points to several others like Axiom, that I've got no experience with.
For mathematical logic operations, there's PVS from SRI. They've got some other cool stuff like model-checking in the same framework.
В дополнение к ссылкам Чарли Мартина, вы также можете захотеть Проверьте Клен . Мой опыт работы с таким программным обеспечением составляет около 5 лет, но я вспоминаю, что в то время Maple был гораздо более интуитивным, чем Mathematica.
There's ongoing research in this area, it's called "Theorem proving in computer algebra".
People are trying to merge the ease of use and power of computer algebra systems like Mathematica, Maple, ... with the logical rigor of proof systems. The problems are:
Computer algebra systems are not rigorous. They tend to forget side conditions such as that a divisor must not be 0.
The proof systems are hard and tedious to use (as you have discovered).
Старая и не обслуживаемая система - «Ontic»:
http://www.cs.cmu.edu/afs/cs/project/ai-repository/ai/areas/kr/systems/ontic/0.html