A Natural Proof System for Natural Language
Lecturers: Lasha Abzianidze and Reinhard Muskens
Venue: ESSLLI 2019 in Riga, Latvia
Natural language inference requires high reasoning capacity in order to recognize semantic relations between natural language expressions. The course is built around this highly interdisciplinary problem. It introduces a computational theory of reasoning, called Natural Tableau, that combines the idea of a Natural Logic, (logic using natural language as its vehicle of reasoning), with the semantic tableau method, a proof calculus that can be interpreted as search for a certain situation. The course aims at not only introducing the theory of Natural Tableau but also at showing how it can be put to use in a downstream application such as Recognizing Textual Entailment. During the course attendees will have the opportunity to run an implemented theorem prover on natural language sentences and examine the resulting reasoning procedures based on natural language phrases.
Day 1 - Natural Language Inference
The task of Recognizing Textual Entailment/Natural Language Inference, NLI datasets, monotonicity reasoning, and the NatLog system.
[Handouts] [Slides]
Day 2 - Semantic Tableau Method
Tableau methods for propositional and first-order logics, simple type theory tableau method for natural logic.
[Handouts] [Slides] (some slides were moved for the next day)
Day 3 - Natural Tableau System
Tableau method for natural logic; rules for monotonicity and other algebraic properties; making tableau more natural, i.e. Natural Tableau, by extending the type system and the entry format.
[Handouts] [Slides]
Day 4 - Wide-Coverage Theorem Prover for Natural Language
From CCG derivations to LLFs, linguistically motivated rules, theorem provers for natural logic and natural language.
[Handouts] [Slides]
Day 5 - Natural Language Inference with Natural Theorem Prover
The SICK and FraCaS data; data-driven adaptation and development of LangPro; Evaluation and analyses; demo of adding a new tableau rule to the prover.
[Handouts] [Slides]
[Updated rules file] [Problem file] [Derivation file]