The full generality of Coq might not be needed. I've coded some fairly large systems in ASP, so I feel very comfortable with it. Its a constraint-solving system, and if you've never worked with a constraint system, it can be weird and confusing to learn how to use it. It took me weeks and lots of baby examples before I finally "got it", after which its "obvious".
The nature of constraint systems is that they are neither forward nor backward chainers: they are solvers. They use the Davis-Putnam algo -- this is boat-loads faster than backward/forward chaining, since it automatically prunes all possible branches that cannot be true. If reduces the problem to just one tightly connected network, and then all possible truth-value assignments can be explored exhaustively. This makes it blindlngly fast - literally thousands or millions or billions of times faster than backward/forward chaining. It revolutionized the entire industry. I've used it to simulate 32-bit cpus: so you could explore e.g. 2^64 or 2^80 possiblities in milliseconds because it could prune effectively all of that combinatorial explosion to a tight nucleus of a few hundred or a few thousand possibilities, which can be exhaustively explored. I assume that the theorem provers use similar algos, if not exactly the same algo. This is one reason that its probably a waste of time to try to write a crisp backward-forward chainer for PLN -- chaining is essentially an obsolete technology, for crisp logic. I suppose I'm overstating this, but really, based on everything I've read, the bad-old days of prolog and circuit simulators are over, and there's no point in going back there again. --linas On Mon, Oct 9, 2017 at 12:57 PM, Nil Geisweiller <[email protected]> wrote: > On 10/08/2017 11:43 AM, Linas Vepstas wrote: > >> So, the question is: what's the base tech? Starting with SAT solvers >> seems like too low a level. I like answer-set programming (ASP) because it >> explicitly deals with first-order logic and therefore is a natural fit for >> PLN. (and of course, the ASP solvers are now blazingly fast). A third >> possibility would be a theorem prover, like Coq or whatever, but these >> might be a poor fit for PLN. I dunno >> > > They might all be OK, depending on the task. The problem I'm seeing is how > to turn a backward chainer query *with variables* into theorem(s) in these > formalisms. > > I guess I would know how to turn > > Evaluation P A > > where P and A are fully defined into a Coq theorem, but what if A is > replaced by X > > Evaluation P X > > and we want to find inference chains instantiating as many X so that P(X). > > Can these tools do that? > > I suppose ASP can. But can a general automatic prover like Coq can? I > don't know. > > I would be tempted to try first with a crisped version of PLN itself, as > this would require almost no effort. > > Of course existing tools can be a lot more efficient than crisp-PLN, at > least for some tasks, I doubt for everything though. For that, ultimately > nothing is gonna beat meta-learning I believe, so that would be my only > reserve for spending time on these other tools. But I agree that it's a > very interesting pursue. > > Nil > -- *"The problem is not that artificial intelligence will get too smart and take over the world," computer scientist Pedro Domingos writes, "the problem is that it's too stupid and already has." * -- 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 post to this group, send email to [email protected]. Visit this group at https://groups.google.com/group/opencog. To view this discussion on the web visit https://groups.google.com/d/msgid/opencog/CAHrUA36UGdEOtSWdo4%2BDtPcXV6k2inDkmEMtxpv_Wuo%3DJhkmsg%40mail.gmail.com. For more options, visit https://groups.google.com/d/optout.
