[ux266478]

> An outer shell to prolog would be a theorem solver for example, because Prolog is a very rudimentary one.

I think it's the wrong way to look at it. It's not that Prolog is a rudimentary theorem solver, it's that theorem provers are a specialized use-case of deductive proofs, so a computational foundation of FOL makes them trivial to write as programs. A pile of bricks and a jar of mortar isn't a rudimentary house, so to speak.