Hi Ivan,
What you describe in the first paragraph sounds like what SAT solvers do.
The actual algorithm doesn't "start from falsehood", nor does it chain; it
picks it's own starting point and runs in the sequence that it wants to. It
quickly returns a yes/no answer as to whether a collection of statements is
satisfiable or not.
Negation in SAT solvers is very interesting -- if you have a variable x,
and you have expressions that contain not-x then SAT solvers work best if
you use a new variable, call it nx, and then, only at the very end, check
to see if nx is equal to not-x. If you declare that nx equals not-x at the
very beginning, the algo runs thousands/millions of times slower. It takes
a while to understand this.
If you can formulate your axioms (or their negations) as prolog, then I
recommend the U. Potsdam ASP solver. It's excellent (or at least, was, when
I used it a decade ago.)
In many ways, prolog statements are "just like" the "jigsaw pieces" that I
keep talking about -- given a set of jigsaw pieces, they can either be
assembled, or not. ("satisfied" or not). Atomese does have a "jigsaw
constraint satisfaction" solver: this is Link Grammar. It's fairly general;
the "best API" is a work-in-progress. It runs just as fast as SAT solvers,
mostly because it uses SAT-like algorithms.
I have not attempted a prolog-to-link-grammar converter or bridge. That
would be interesting and educational.
Performance: well, that depends very strongly on the actual dataset. It is
"well known" that SAT solvers solve certain problems in N logN time.
Others in N^2 or N^3. It is "well known" that "most typical" user problems
can be solved in linear or polynomial time. It is also known that you can
write out problems that require N-factorial time. It depends strongly on
the actual problem. Thus, SAT solvers have a reputation for being
"blindingly fast" for "most user problems", especially when compared to
chaining.
A standard beginner mistake is to use not-x instead of introducing a new
variable nx -- this mistake will convert linear runtime problems into
N-factorial problems. The books and tutorials all mention this mistake at
the very beginning, but it is hard to understand, until you actually play
with it for a few weeks. Then, one day, you go "ah ha!". The meta-theory
behind this is the theory of "intuitionistic logic" vs. "classical logic".
Roughly speaking, the law of the excluded middle converts polynomial-time
problems into factorial-time problems.
Anyway, all of the above deals with "crisp logic", true/false problems.
Most of what I work on involves probabilities and counting, where most of
the above ideas offer little benefit.
--linas
On Thu, Jul 20, 2023 at 2:56 PM Ivan V. <[email protected]> wrote:
> Linas,
>
> The basic idea is this: I define some set of axioms, and I define a
> falsehood as a starting point. Chaining forward on, from falsehood I derive
> all the contradictory formulas. What I want is to pass an arbitrary
> formula, and check if it is contradictory. (This could also be implemented
> by a normal theorem constructor and passing a negated arbitrary formula to
> check if it is valid.)
>
> The question is: is there an automation in OC that will simply output an
> yes/no answer, or do I have to do every chaining step manually until I
> reach the passed formula or I eventually give up? I may be interested in
> automating this process if it can be shown that it does its computation in
> polynomial time in the worst case scenario.
>
> ivan v.
>
> čet, 20. srp 2023. u 13:36 Дмитрий Радомский <[email protected]>
> napisao je:
>
>> Comrade, if you are interested in strong artificial intelligence, then
>> write. I know your technology with perceptrons, I'm not interested in it.
>> Write the contacts of people who want agi and are willing to pay for it.
>>
>> чт, 20 июл. 2023 г., 14:10 Linas Vepstas <[email protected]>:
>>
>>> Hi Ivan,
>>>
>>> What is an anti-axiom?
>>>
>>> Atomese is designed to "represent anything", and so, in principle, you
>>> can represent "anti-axioms" (whatever those are).
>>>
>>> The query engine (aka "pattern matcher") can be used to perform simple
>>> forward chaining: so, if you have a rule that accepts anti-axioms as input,
>>> and produces more as output, then you can chain away as desired. It is (by
>>> definition) SMT, simply because it can chain "anything". (The unifier can
>>> also "unify anything".)
>>>
>>> However, when academics say "SMT", they usually envision something very
>>> different: a highly optimized SAT solver that has a custom API that allows
>>> "theories" to be defined (and thus, "solved"). This is "easy" to do in
>>> principle, but hard to do in practice, since the theories themselves might
>>> be hard to solve efficiently. Consider, for example, linear algebra: sounds
>>> easy, but in real life, there are fancy algorithms that solve linear
>>> programming problems. Attaching existing linear programming or integer
>>> programming codes to a SAT solver is hard/impossible.
>>>
>>> To conclude, yes, Atomese can do SMT, but what it does does not conform
>>> to the conventional academic definition of SMT.
>>>
>>> SAT itself is a collection of algorithms that are highly optimized to
>>> solve certain kinds of boolean problems. The AtomSpace does not have a
>>> built-in SAT solver, due to a lack of interest in such a capability. I
>>> think I know how well you can program, and I think you could add this
>>> yourself, if you were interested. It might take you several months, maybe a
>>> bit more. I suspect you are not interested in this :-/
>>>
>>> Performance: you can use the query engine to do forward chaining. With
>>> some cleverness, you can go backwards, too. Performance is roughly a
>>> thousand steps per second, but that depends strongly on the number of
>>> rules, the size of the dataset, the complexity of the rules, etc. All the
>>> usual caveats of chaining apply: if you have a combinatorial explosion,
>>> then you have a combinatorial explosion, and you are out of luck.
>>>
>>> Some kinds of combinatorial explosion in some kinds of chaining problems
>>> are "easy" to avoid. If you can express your problem as a graph, and that
>>> graph factors into a tangle, plus many trees attached to that tangle, then
>>> you can prune the trees, solve the tangle, and then re-attach the trees.
>>> This is what SAT solvers do. SMT is "hard" because the trees get tangled
>>> into the central tangle, and so you don't get any performance advantage.
>>> You end up having to brute-force an NP problem.
>>>
>>> I'm still very excited by hypervector computing, but I do not have any
>>> words of wisdom to impart.
>>>
>>> -- Linas
>>>
>>> On Wed, Jul 19, 2023 at 5:33 PM Ivan V. <[email protected]> wrote:
>>>
>>>> Respected OC community,
>>>>
>>>> If I understood correctly, OpenCog can be used an an SMT solver.
>>>> Considering this feature, how far OpenCog is from solving satisfiability
>>>> problem for propositional logic in polynomial time complexity?
>>>>
>>>> In explanation, I'm having a hunch about anti-axioms which derive all
>>>> the contradictory anti-theorems. If, and only if a propositional logic
>>>> formula belongs to such a set of anti-theorems, then it is not satisfiable.
>>>> Can such anti-axioms be defined in OpenCog, maybe in URE?
>>>>
>>>> Did anyone try to measure actual processing time of such an approach?
>>>> If not, what obstacles do you see in this approach?
>>>>
>>>> Any thoughts would be greatly appreciated.
>>>>
>>>> Finest regards,
>>>> ivan v.
>>>>
>>>> --
>>>> You received this message because you are subscribed to the Google
>>>> Groups "opencog" group.
>>>> To unsubscribe from this group and stop receiving emails from it, send
>>>> an email to [email protected].
>>>> To view this discussion on the web visit
>>>> https://groups.google.com/d/msgid/opencog/f40317fb-fbe1-41d7-bf19-c2c4fa48d1d8n%40googlegroups.com
>>>> <https://groups.google.com/d/msgid/opencog/f40317fb-fbe1-41d7-bf19-c2c4fa48d1d8n%40googlegroups.com?utm_medium=email&utm_source=footer>
>>>> .
>>>>
>>>
>>>
>>> --
>>> Patrick: Are they laughing at us?
>>> Sponge Bob: No, Patrick, they are laughing next to us.
>>>
>>>
>>> --
>>> You received this message because you are subscribed to the Google
>>> Groups "opencog" group.
>>> To unsubscribe from this group and stop receiving emails from it, send
>>> an email to [email protected].
>>> To view this discussion on the web visit
>>> https://groups.google.com/d/msgid/opencog/CAHrUA36%3DOdvD29a%3De2j6Jhui2_gt%3D%3DB3G0Z8m688-x-bexQV3w%40mail.gmail.com
>>> <https://groups.google.com/d/msgid/opencog/CAHrUA36%3DOdvD29a%3De2j6Jhui2_gt%3D%3DB3G0Z8m688-x-bexQV3w%40mail.gmail.com?utm_medium=email&utm_source=footer>
>>> .
>>>
>> --
>> You received this message because you are subscribed to the Google Groups
>> "opencog" group.
>> To unsubscribe from this group and stop receiving emails from it, send an
>> email to [email protected].
>> To view this discussion on the web visit
>> https://groups.google.com/d/msgid/opencog/CAAT0KVZE41Gucwwu9NgDz4f5mUr2e3TZEMGiUGA7%3Do2%3D9HT-oA%40mail.gmail.com
>> <https://groups.google.com/d/msgid/opencog/CAAT0KVZE41Gucwwu9NgDz4f5mUr2e3TZEMGiUGA7%3Do2%3D9HT-oA%40mail.gmail.com?utm_medium=email&utm_source=footer>
>> .
>>
> --
> You received this message because you are subscribed to the Google Groups
> "opencog" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/opencog/CAB5%3Dj6UyxAe70LFYcs9OM6GwczpRpJBx1RF6n1R266ufMVcktA%40mail.gmail.com
> <https://groups.google.com/d/msgid/opencog/CAB5%3Dj6UyxAe70LFYcs9OM6GwczpRpJBx1RF6n1R266ufMVcktA%40mail.gmail.com?utm_medium=email&utm_source=footer>
> .
>
--
Patrick: Are they laughing at us?
Sponge Bob: No, Patrick, they are laughing next to us.
--
You received this message because you are subscribed to the Google Groups
"opencog" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/opencog/CAHrUA36oygRZ52zFZRGBHD3RFOwjw6SF9kq0VwDOdfd%3DyU%3DfWw%40mail.gmail.com.
