On 10/04/2017 11:02 AM, Linas Vepstas wrote> And can implement
algorithms in the graph database-agnostic way and
use all the industrial power of the best database available.
Scientists do use commercial off-the-shelf computers for HPC, why
not to use industrial software? And similar things we can say about
use of external reasoners (linear logic, Coq, Isabelle, etc.).
If you can attach coq to tinkerpop and make it work ... sure. But you
would probably have to completely rewrite both coq and gremlin in order
to do this. And that is a huge amount of work.
I never tried Coq or Isabelle, but the provers I've tried (E and
Vampire) were using resolution
https://en.wikipedia.org/wiki/Resolution_(logic), which doesn't work for
a para-consistent logic like PLN, at least not out-of-the-box. On top of
that PLN is probabilistic (or even meta-probabilistic we could say).
These make it difficult or at best unnatural to use traditional
automatic theorem provers. Maybe there's an easy way, or a more general
framework that I missed, but that was my impression when I studied the
domain.
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 opencog+unsubscr...@googlegroups.com.
To post to this group, send email to opencog@googlegroups.com.
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/a261e2b5-7d6e-74f9-fe87-cd83304adb2a%40gmail.com.
For more options, visit https://groups.google.com/d/optout.
