A Natural Proof System for Natural Language

Venue:
TbiLLAI 2019 in Tbilisi, Georgia

Abstract

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 Natural Language Inference.

Schedule

Day 1 - Natural Language Inference & Tableau Method

The task of Recognizing Textual Entailment/Natural Language Inference, NLI datasets, monotonicity reasoning, and semantic tableau methods for propositional and first-order logics

[Handouts]

Day 2 - Natural Tableau System

Lambda logical forms (LLFs), a tableau system for natural logic, tableau rules, natural tableau proofs.

[Handouts]

Day 3 - Natural Language Inference with Natural Theorem Prover

Obtaining LLFs, linguistically motivated rules, the theorem provers for natural logic and natural language, the SICK and FraCaS datasets, evaluating performance of the prover

[Handouts]

References

- Abzianidze, L. (2017):
*LangPro: Natural Language Theorem Prover*. EMNLP. - Abzianidze, L. (2016):
*Natural Solution to FraCaS Entailment Problems*. *SEM. - Abzianidze, L. (2015):
*A Tableau Prover for Natural Logic and Language*. EMNLP. - Muskens, R. (2010):
*An Analytic Tableau System for Natural Logic*. LNCS, Springer. - LangPro: GitHub repository; online demo