טכניון מכון טכנולוגי לישראל
הטכניון מכון טכנולוגי לישראל - בית הספר ללימודי מוסמכים  
M.Sc Thesis
M.Sc StudentZamansky )Lifshits( Anna
SubjectA 'Natural Logic' Inference System Based on the Lambek
Calculus
DepartmentDepartment of Computer Science
Supervisor Professor Emeritus Nissim Francez


Abstract

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.