On 10/06/2017 02:10 AM, Linas Vepstas wrote:
it would be nice to have a fast crisp prover so that the system could
jump to conclusions, and pln more slowly in the background.
Yes, even for our rule engine alone there is a benefit to that. On top
of being faster to evaluate, crisp rules tend to have less premises than
their probabilistic counterparts.
Then the question is how to set the TV of these conclusions. If the
axioms are crisps with (stv 1 1) or (stv 0 1), then the conclusions
would be (stv 1 1) or (stv 0 1). But if the axioms are non-crisp, then I
guess the crisp rules could set (stv 1 Epsilon) or (stv 0 Epsilon), just
to express that something is possibly true or false. Or else we can
create a new TV type for it.
Nil
On Oct 4, 2017 5:45 PM, "'Nil Geisweiller' via opencog"
<[email protected] <mailto:[email protected]>> wrote:
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)
<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 [email protected]
<mailto:opencog%[email protected]>.
To post to this group, send email to [email protected]
<mailto:[email protected]>.
Visit this group at https://groups.google.com/group/opencog
<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
<https://groups.google.com/d/msgid/opencog/a261e2b5-7d6e-74f9-fe87-cd83304adb2a%40gmail.com>.
For more options, visit https://groups.google.com/d/optout
<https://groups.google.com/d/optout>.
--
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]
<mailto:[email protected]>.
To post to this group, send email to [email protected]
<mailto:[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/CAHrUA343%2BH5CT5zGobgT5hq9sy_iLPSGJUh52WcsgHUPUZNqcw%40mail.gmail.com
<https://groups.google.com/d/msgid/opencog/CAHrUA343%2BH5CT5zGobgT5hq9sy_iLPSGJUh52WcsgHUPUZNqcw%40mail.gmail.com?utm_medium=email&utm_source=footer>.
For more options, visit https://groups.google.com/d/optout.
--
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/8762676a-e52c-e3b4-9edb-bcd2c21e9aa0%40gmail.com.
For more options, visit https://groups.google.com/d/optout.
