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
--
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/9e6bc02e-7eca-512f-1c17-eb8b01c78563%40gmail.com.
For more options, visit https://groups.google.com/d/optout.
