Natural Logic and Natural Deduction for Reasoning about Natural Language

  • Ghadah Binhadba

Student thesis: Phd


One way of measuring a natural language processing system’s semantic capacity is by demonstrating that it can handle natural language inference (NLI). Automating the task of NLI requires natural language text to be converted into a meaning representa- tion (MR) on which inference procedures can be applied. Finding a balance between the expressive power of a MR and the inferential capabilities that could be conducted using such representation is a challenge. In that respect, the aim of this thesis is to rea- son about deep semantic phenomena (such as defaults, monotonicity, quantifiers and propositional attitudes) and thus construct a MR that is able to preserve the subtle se- mantic distinctions people make when reasoning about such phenomena. For decades, the best way for obtaining such semantically deep MRs was by translating NL texts into some formal language such as first-order logical formulas. However, such transla- tions have proven difficult. Alternatively, and motivated by the success of natural logic systems on the pairwise entailments tasks, in which MRs are close to NL texts’ sur- face form, we have investigated the use of a first-order logic theorem prover (to allow reasoning over multi-premises tasks) and have adapted it to work on representations that were built based on syntactical analysis (dependency trees) of NL texts. To en- sure the right depth of representation, we have investigated the literature to learn about the intended semantic phenomena and hence model them in our MR accordingly. To measure such an approach’s performance, we have implemented an inference system that consists of three parts: a dependency grammar to generate syntactical trees, a tree normalizer to build the desired MRs (namely inference friendly forms) and a theorem prover (CSATCHMO+) along with some necessary background information. To our knowledge, there is not much work that has been done in this line of research (com- bining theorem proving with a version of natural logic). Therefore, we have tested our system’s performance on the part of a test-set that has a clear representation of semantic phenomena (The FraCas test-set) and compared it to the literature’s related systems. Overall, the current findings encourage further investigation extending to other phenomena, as we obtained a comparable result when compared to the related natural logic systems and an only just better result than a natural logic theorem prover.
Date of Award31 Dec 2021
Original languageEnglish
Awarding Institution
  • The University of Manchester
SupervisorAllan Ramsay (Supervisor)


  • Natural Deduction
  • Natural Logic
  • Theorem Proving

Cite this