| ▲ | PaulHoule an hour ago | |
Well... One approach to symbolic AI is that it is about putting together logic and databases and another is that it is about SMT solving and constraint satisfaction and such. Lisp was a revolutionary language not because of the parens or even macros or that people used it to implement "expert systems" but because it had a garbage collector, hashtables and such. (e.g. most of the examples in famous Lisp programming books by Graham and Norvig can be coded up just fine in Python for pedagogical purposes) You can make a superhuman chess engine by alpha-beta search, etc. One of many great applications of neurosymbolics right now is using an A.I. to translate a program or proof or informal description of such a thing into inputs for a theorem prover. If math learns anything about A.I. it will be that they won't let you submit a proof to a journal if you can't write it up formally. Like it turns out that the ability of A.I.(s) to do "translation" (e.g. something that sorta requires understanding but doesn't quite) and handle tedious tasks unlocks the ability to use formal methods. | ||