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.
