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.
