Hi Jon,
you've come to the right place, yes we are super psyched about combining
AI and ATP, even though it's been underexplored in the context of
OpenCog, we've only scratched the surface! Personally the furthest I've
gone is proving some trivial SUMO theorems, see
https://github.com/opencog/pln/tree/master/examples/pln/sumo. Beside
that we've (me with Ben's input) done some really cool experiments on
inference control meta-reasoning, basically using reasoning (or rather
an efficient specialized form thereof tailored for pattern mining) to
speed up reasoning! See
https://github.com/opencog/pln/tree/master/examples/pln/inference-control-meta-learning.
On 1/6/21 1:47 PM, Jon P wrote:
Fifthly I am then quite excited in the abstract about where this
system is headed. For example an AI which can formally reason about
code it is writing and can prove mathematical statements could be very
powerful. I think there is some nice approach to the control problem
here, something like "new code can only be run if it is proven to obey
the same constraints that currently running code is bound by." This
maybe creates a way of limiting what an AI can do no matter how clever
it becomes.
If you don't know the Goedel Machine yet I think you'll quite like it
http://people.idsia.ch/~juergen/goedelmachine.html
Needless to say OpenCog incorporates principles of the Goedel Machine,
in fact the first time I read and understood OpenCog's design I
exclaimed to Ben "[OpenCog] is a workable Goedel Machine!!!".
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 view this discussion on the web visit
https://groups.google.com/d/msgid/opencog/a0824a3b-ffa7-2e87-b947-ba4cd32debed%40gmail.com.
