A Tableau Prover for Natural Logic and Language

Proceedings of the 2015 Conference on Empirical Methods in Natural Language Processing, pages 2492–2502, Lisbon, Portugal, 17-21 September 2015. c⃝2015 Association for Computational Linguistics. A Tableau Prover for Natural Logic and Language Lasha Abzianidze TiLPS, Tilburg University, the Netherlands L.Abzianidze@uvt.nl Abstract Modeling the entailment relation over sen- tences is one of the generic problems of natural language understanding. In or- der to account for this problem, we de- sign a theorem prover for Natural Logic, a logic whose terms resemble natural lan- guage expressions. The prover is based on an analytic tableau method and employs syntactically and semantically motivated schematic rules. Pairing the prover with a preprocessor, which generates formulas of Natural Logic from linguistic expressions, results in a proof system for natural lan- guage. It is shown that the system obtains a comparable accuracy (≈81%) on the un- seen SICK data while achieving the state- of-the-art precision (≈98%). 1 Introduction A problem of recognizing textual entailments (RTE)—given two text fragments T (for a text) and H (for a hypothesis), determine whether T entails, contradicts or is neutral to H—is consid- ered as a complex and, at the same time, funda- mental problem for several NLP tasks (Dagan et al., 2005). For more than a decade, RTE chal- lenges have been held, where systems are compet- ing to each other with respect to human annotated RTE test data; but there are few systems that try to solve RTE problems by computing meanings of linguistic expressions and employing inference engines similar to proof procedures of formal log- ics. Moreover, those few systems are usually used in combination with shallow classifiers since the systems’ performances alone are poor. The current paper advocates that purely deduc- tive inference engines over linguistic representa- tions backed up with a simple lexical knowledge base could be solely and successfully used for the RTE task. Our work builds on the theory of an analytic tableau system for Natural Logic (Natural Tableau) introduced by Muskens (2010). The the- ory offers to employ a tableau method—a proof procedure used for many formal logics—for the version of Natural Logic that employs Lambda Logical Forms (LLFs)—certain terms of simply typed λ-calculus—as Logical Forms (LFs) of lin- guistic expressions. The merits of the current ap- proach are several and they can be grouped in two categories: virtues attributed to the tableau prover are (i) the high precision for the RTE task charac- teristic to proof procedures, (ii) the transparency of the reasoning process, and (iii) ability for solv- ing problems with several premises; and those concerning LLFs are (iv) an evidence for LFs that are reminiscent of Surface Forms but still retaining complex semantics, and (v) an automatized way of obtaining LLFs from wide-coverage texts. The rest of the paper is organized as follows. First, Natural Tableau is introduced, and then a method of obtaining LLFs from raw text is de- scribed. We outline the architecture of an imple- mented theorem prover that is based on the the- ory of Natural Tableau. …

Content truncated to 500 words