Any technology that scales ought to have some reasonable amount of redundancy. Reasoning is like a welding machine transforming data into proofs. Mathematics is at the heart of everything I do and has never failed me. There is no principle to tell whether to use top-down or bottom-up reasoning. A reasoner that can not give a proof is not a reasoner.