If we assume Montague's belief that there is ¿no important theoretical difference between natural languages and the artificial languages of logicians¿, then there should exist a proof system for natural languages too, like it is for various logics. But is such a natural proof system sensible? In my talk, I will present a version of a natural proof system that is specially designed to account for natural language inference (NLI) in a systematic way. The proof system, called the Natural Tableau, is based on a semantic tableau method and operates on terms of higher-order logic, which represent a more natural way of modelling linguistic semantics. A Natural Tableau-based theorem prover is able to model both shallow and logical reasoning, demonstrated on standard NLI benchmarks. The prover can also tackle the problem of knowledge sparsity with supervised knowledge induction.