>>On Jan 20, 2008 2:34 PM, Jim Bromer <[EMAIL PROTECTED]> wrote: >> I am disappointed because the question of how a polynomial time solution of > >logical satisfiability might affect agi is very important to me.
Ben Wrote: Well, feel free to start a new thread on that topic, then ;-) In fact, I will do so: I will post a message on SAT, SMT and AGI I would rephrase the question as: How would a pragmatically useful polynomial time solution of logical satisfiability affect AGI? ----------------------------------- I really appreciate that. I was surprised when I thought you were quashing the discussion before it even got started in the direction that I wanted it to go in, and I was ready to take my marbles and go elsewhere. Since my SAT theory is a big deal, I was not interested in going into any details about how it works before I finish it, but I do want to examine the question of whether a general polytime SAT would be useful to AI. ----------------------------------- Ben Went On: In fact, it's interesting to talk about how existing SAT and SMT solvers http://en.wikipedia.org/wiki/Satisfiability_modulo_theories -- which are often quite effective on surprisingly large real-world problems, in spite of being exponential time in the worst case -- affect AGI. SMT in particular seems to have deep potential applicability. It would seem to me that a practical SMT solver handling quantifier logic would be a more useful research goal than proving P=NP. ----------------------------------- I am not so sure about that. SMT seems interesting but it does not seem somehow more strongly related to AGI than more general systems of logical reference. ----------------------------------- Ben went on: In AGI, we don't care that much about worst-case complexity, nor even necessarily about average-case complexity for very large N. We care mainly about average-case complexity for realistic N and for the specific probability distribution of problem-cases confronted in embodied experience. -------------------------------------------------------- My SAT solver will allow us to examine logic in some novel ways. And this is why it may be important to AGI. Although the contemporary work in SAT solvers is impressive and it could be used as is, it is algorithmically all over the place, and it makes integration with experimental methods very difficult. My SAT algorithms will not be novice friendly, but once they are learned, I think it will be possible to apply them to general problems of intelligence with only a little work. I have to qualify my comments by repeating that I am not certain that my algorithms will work. But I would like to write more about my thinking about the impact that this new theory will have on AGI in a few days. Jim Bromer ____________________________________________________________________________________ Looking for last minute shopping deals? Find them fast with Yahoo! Search. http://tools.search.yahoo.com/newsearch/category.php?category=shopping ----- 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=88251719-799f0d
