Jim Bromer wrote:
I am going to try to summarize what I have said.
With God's help, I may have discovered a path toward a method to
achieve a polynomial time solution to Logical Satisfiability, and so
from this vantage point I have started to ask the question of whether
or not a feasible SAT solver would actually be useful in advancing
general AI.
I think that most knowledgeable people would assume that it would be.
However, there has been some doubt about this so I came up with a
logical model that might show how such a situation could make a
critical difference to general AI programming. Or at least AI
programming that emphasizes the use of rational methods.
My feeling right now, is that if my solver actually works it would
take at least n^3 or n^4 steps. This means, for all practical
purposes, that it would stretch the range of general solvers from
logical formulas of 20 distinct variables or so to formulas of
hundreds or even thousands of characters long. I believe that this
would be a major advancement, both in general computing and in AI
programming.
But would it make any difference in general AI programming, what this
group calls AGI?
Jim,
The problem is that even if your solution (which sounds not so much like
a solution as a vague, God-inspired possibility that you may have found
a path toward a method that might conceivably yield a solution.....)
actually did what you claim it might do, that would still beg so many
questions about what it means to build an AGI, that it has almost no
relevance.
There are only some kinds of AI that might benefit, and there are some
people who would claim that, in fact, the types of AI that could benefit
are dead in the water anyway (will never lead to an actual AGI).
So when that is added to your religious references and open admission
that you only think you may have a solution, all kinds of red flags go up.
Richard Loosemore
Imagining a system that used logical or rational methods that might
initially be expressed in fairly simple logical terms, but which could
have hundreds of variants and hundreds of interconnections with the
other logical formulas of the system I have come up with a case where
n^4 SAT might be critical. The formulas of the system that I have in
mind would be speculative and derived from an inductive logical system
that was designed to be capable of learning. I then pointed out that
some of the formulas produced by an automated system might have only a
few valid cases, meaning that a trial and error method of searching
for logical satisfiability would be very unlikely to work for those
formulas. In this case the n^4 SAT solver would be very useful. But
why would this be useful to AGI?
Remember, our programs are supposed to be adaptive and capable of
general learning. If a fully automated AI program was truly learning
from the IO data environment, it would tend to create numerous
conjectures about it. Such a program would tend to create
insignificant conjectures that was founded on a great deal of trivial
evidence which could then be used to 'confirm' the conjecture. Even
worse, it might (and will) produce meaningless garbage that was based
on methods like those that mush rational and non-rational responses or
made extensive use of over-generalization. On the other hand a few
coincidences or over-generalizations could turn out to be very
meaningful. So my theory is this. If the program produced logical
theories of relations between events that occurred in the IO data
environment, then those theories that had only a few valid solutions
might be instrumental. A complicated theory that only has a few valid
cases would, under certain conditions, be easier to prove or disprove
than a theory that can be 'verified' by tens of thousands of
combinations of trivial coincidences. This is similar to Popper's
falsifiability theory in that it supposes that some theories have to
be strongly testable in order to advance science. I do not mean to
suggest that falsifiability is absolute in an inductive system, just
that some key theories that are narrowly testable may be very
significant in the advancement of learning. The rational-based
conjectures that only have a few solutions would therefore be better
for critical testing (as long as the solutions involved some kind of
observable event that was likely to occur under some conditions.) And
a better general SAT solver would represent a major advancment in
discovering the conditions under which confirmatory or disconfirmatory
evidence for those kinds of theories could be found.
Perhaps people have objected to my messages about this because I
mentioned God, or perhaps they have objected to my question because
they believe a polynomial time solution to the SAT problem is
impossible. On the other hand, there may be another objection to the
question simply because the answer is so blatantly obviousness. Of
course a polynomial time solution to SAT would be significant in the
advancement AI programming.
Jim Bromer
On Sun, Mar 30, 2008 at 11:47 AM, Jim Bromer <[EMAIL PROTECTED]> wrote:
The issue that I am still trying to develop is whether or not a general SAT
solver would be useful for AGI. I believe it would be. So I am going to go on
with my theory about bounded logical networks.
A bounded logical network is a network where simple logical theories, that is
logical speculations about the input output environment and about its own
'thinking', could be constructed with hundreds or thousands of variants and
interconnections to other bounded logical theories. These theories would not
be fully integrated by strong taxonomic logic, so they could be used with
inductive learning. Such a system would produce some inconsistencies, but any
inductive system can produce inconsistencies. I believe that interconnected
logically bounded theories could show both the intuition of network theories,
the subtleties and nuances of complex integrated theories, and the strong
logical-analytical potential of logical-rational programs. People should also
realize that the bounded interconnected logical model could be used with a
variety of rational reasoning methods, not just ideative logic. But my
personal theories do center around rational ideative reasoning that would
, be capable (I believe) of using and learning general reasoning.
Now there is one criticism to my opinion about the usefulness of a general SAT
solver in this model. That is, since an interconnected bounded logical network
model is not a pure fully integrated logical model, then approximations could
be used effectively in the model. For instance, if the system was capable of
creating bounded logical theories with thousands of interconnections, even if a
solution wasn't known, the program could try millions of guesses about the
logical relations to see if any worked. These guesses would be
simplifications, which would tend toward over-generalization, but whats the
problem? The system I have in mind is not purely logical, it is a bounded
logical system which could and would contain many inconsistencies anyway. My
contention here is that is just the problem that we are faced with today in
rational based AGI. They can get so far, but only so far.
A theory, with thousands of subtle variations and connections with other
theories, that only had one or a few correct solutions would be useful in
critical reasoning because these special theories would be critically
significant. They would exhibit strong correlations with simple or constrained
relations that would be more like experiments that isolated significant factors
that can be tested. And these related theories could be examined more
effectively using abstraction as well. (There could still be problems with the
critical theory since it could contain inconsistencies, but you are going to
have that problem with any inductive system.) If you are going to be using a
rational-based AGI method, then you are going to want some theories that
exhibit critical reasoning. These kinds of theories might turn out to be the
keystone in developing more sophisticated models about the world and
reevaluating less sophisticated models.
Jim Bromer
-------------------------------------------
agi
Archives: http://www.listbox.com/member/archive/303/=now
RSS Feed: http://www.listbox.com/member/archive/rss/303/
Modify Your Subscription: http://www.listbox.com/member/?&;
Powered by Listbox: http://www.listbox.com
-------------------------------------------
agi
Archives: http://www.listbox.com/member/archive/303/=now
RSS Feed: http://www.listbox.com/member/archive/rss/303/
Modify Your Subscription:
http://www.listbox.com/member/?member_id=8660244&id_secret=98558129-0bdb63
Powered by Listbox: http://www.listbox.com
