It seems to me there is great potential for cross-fertilization between the fields of Automated Theorem Proving and AGI …

This is especially clear when one looks at an AGI approach like OpenCog, in which probabilistic/heuristic logic plays a key role (the Probabilistic Logic Networks framework) …

There is a stream of work in ATP called “lean theorem proving” which involves creating really really simple theorem provers and seeing how well they can do. The answer is, sometimes pretty damn well, though not quite as well as the best theorem provers around…

It seems to me that integrating an appropriate lean theorem prover into OpenCog’s URE Rule Engine, and then figuring out how to use it together with PLN, would be a very interesting project and approach…

I note that in common PLN inferences, the majority of inference steps are actually just standard predicate logic steps … only a minority of steps are actually probabilistic/heuristic (though these are important ones)! This suggests that such integration could have practical near-term value…

The lean theorem prover Nanocop (http://www.leancop.de/papers/nanocop_ijcar16.pdf ) seems like a natural one to explore in this light, as unlike its predecessors such as leancop, it does not require any assumption that formulas are placed in DNF or CNF …