Natural theorem proving for natural language: theory and application

Presented by: Lasha Abzianidze

Duration: 2 hours

On: 12 Feb, 2020

Location: Gothenburg

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.