Comment by PaulHoule

It's what we used to call AI back in the 1970s and 1980s which has advanced a whole lot with little awareness. That is, people thought 10,000 rules was a lot of rules in 1998 and now you can work with 10,000,000 rules. And theorem provers, SAT and SMT all got vastly better.