> SMT in particular seems to have deep potential applicability. To add a little background, SMT is under heavy developement at Microsoft and it is planned to be applied a lot. The basic progress is that the new version of Z3 is an order of magnitude faster than the last one, and is even a competitive SAT-solver in addition to doing SMT. It is used in (at least) two projects: one is C code verification with the aim to fully verify a hypervisor written in C (Verisoft XT done in Saarbruecken), the other is parametrized unit tests integration in Visual Studio called Pex (http://research.microsoft.com/Pex/).
As far as I know there is little or no work done yet to integrate probabilistic reasoning with these solvers and it will probably not be easy to do it and keep things efficient. Integrating these solvers directly into AGI will probably be quite hard as well - possibly as hard as just integrating DPLL with clause learning directly (the basic method for most SAT solvers and I guess SMT solvers as well). But even if there is no easy way to directly integrate or extend the solvers for AGI, there are numerous ways in which these can speed up AGI developement. It looks like Microsoft is generating demand for formal verification which never hurts. In addition, you can try to use Pex for your .Net coding projects - parametrized unit tests are really really nice, almost like specification, just try and see your bugs die! ;). - lk ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=8660244&id_secret=88126441-aa01a5
