M.Sc Thesis | |

M.Sc Student | Zamansky )Lifshits( Anna |
---|---|

Subject | A 'Natural Logic' Inference System Based on the Lambek Calculus |

Department | Department of Computer Science |

Supervisor | PROFESSOR EMERITUS Nissim Francez |

Most of the literature in natural reasoning assumes a model-theoretic perspective and uses translation into some formal language, e.g. first order logic, as an intermediate step for computing inferences. However, information contained in natural language structures is partially lost during translation and the intermediate language in use is sometimes not powerful enough to express

the complex semantics of natural language expressions.

The general goal of a `Natural Logic' inference system is giving a systematic account of natural reasoning using linguistic structures as the vehicle of inference instead of employing logical forms.

This thesis develops a `Natural Logic' inference system based on a modification of the (associative) Lambek calculus (L). The proposed inference system manipulates natural language syntactic representations with no intermediate translation to logical formulae.

The main part of the system used for deriving inferences is the L-based Order Calculus, which manipulates order statements between proof terms, representing Lambek derivation trees of natural language expressions via the Curry-Howard isomorphism.

Our work extends the system of Fyodorov et al., which is based on the simpler Ajdukiewicz-Bar Hillel Calculus. In our work we overcome some limitations of the system of Fyodorov et al. and enable it to deal with new kinds of inferences, such as inferences involving sentences with extraction, pied piping etc.

Basing the inference system on the Lambek calculus brings about a certain complication - the emergence of proof terms which are not in normal form. We augment the proposed Lambek based Order Calculus with normalization axioms as a remedy for this complication and demonstrate that they enable the system to derive new kinds of inferences.

Finally, we present a terminating proof search procedure.