Comment by PaulHoule
4 years ago
There has been big progress in automated theorem proving lately
https://en.wikipedia.org/wiki/Automated_theorem_proving
you just don't hear about it much because the technology is not so fashionable today. Also it is more clear what the limits are, I mean, Turing, Godel, Tarski and all of those apply to neural networks as well any other formal system but people mostly forget it.
Knuth wrote a really fun volume of The Art of Computer Programming about advances in SAT solvers which are the foundation for theorem provers
https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat...
Everybody is aware that neural network techniques have improved drastically in performance, it's much more obscure that the toolbox of symbolic A.I. has improved greatly. Back in the 1980s production rules engines struggled to handle 10,000 rules, now Drools can handle 1,000,000+ rules with no problems.
> There has been big progress in automated theorem proving lately
It doesn't seem like there has been much progress for anything but FOL?
The wiki article on automated theorem proving is quite bad as an overview of the active field; it's more a historical article about the mid to late 20th century. Most of the interesting things in automated reasoning have happened since the naughts, and that article kind of stops in the 90s
SMT solvers have gotten quite good over the past couple decades, there are tons of domain-specific tools (eg in software and hardware verification), tons of niche applied decidable or semi-decidable theories (eg various modal and description logics), a lot of progress on the proof assistant ("non-fully-automated theorem proving") paradigm, and so on.
It's clear that commonsense reasoning needs to deal with modals, counterfactuals, defaults, temporal logic, etc.
It's not hard to add some extensions to logic for a particular application but a very hard problem to develop a general purpose extended logic.
I look at the logic-adjacent production rules systems which never really standardized some of the commonly necessary things such as agendas, priorities, defaults, etc.