HN Books @HNBooksMonth

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.

⬐ sva_

> There has been big progress in automated theorem proving lately

It doesn't seem like there has been much progress for anything but FOL?

⬐ PaulHoule

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.

⬐ thwayunion

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.

Vol 4A was published in 2011: https://www.amazon.com/Art-Computer-Programming-Combinatoria...

Vol 4B was partially published in fascicles: https://www.amazon.com/Art-Computer-Programming-Fascicle-Pre... and https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat...

Instead of the ultimate edition of vols 1-3, so far we've got a "patch" by Martin Ruckert who coordinated the volunteers: https://www.amazon.com/MMIX-Supplement-Computer-Programming-...

⬐ hvidgaard

Thanks for the pointers.

This https://cs.stanford.edu/~uno/taocp.html seems up to date.

Donald Knuth recently released the latest chapter of 'The Art of Computer Programming' and decided to tackle the topic of Satisfiability & SAT solvers ( @ https://www.amazon.com/Art-Computer-Programming-Fascicle-Sat... ). Although he refers to algorithms in an vague way (using words like "Algorithm A" or "Algorithm J") and makes a determined effort to convey all information in the most mathematically precise way possible, I'm of the view that it's the finest work of it's kind on this topic. Having a section on something like 'random restarts' is great, but if you are already deep enough to have an interest in a paper like this, you are deep enough to learn about Luby sequences.

⬐ bloodorange

referrer link?