Comment by sva_

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.