A `natural logic' inference system using the Lambek calculus (Q851198)

In the paper the construction of a special inference system for natural language is presented. The proposed system, \({\mathcal L}\)-based Order Calculus (\({\mathcal L}\)-OC), is an improvement of the system offered by \textit{Y. Fyodorov, Y. Winter} and \textit{N. Francez} [Log. J. IGPL 11, No.~4, 385--417 (2003; Zbl 1076.03529)], in which the Ajdukiewicz-Bar Hillel AB calculus has been replaced by the Lambek calculus \({\mathcal L}.\) The system \({\mathcal L}\)-OC, as opposed to the system by Fyodorov et al., derives inferences using proof terms representing syntactic derivations via the Curry-Howard correspondence. This system also includes an abstraction rule and standard \(\beta/\eta\)-normalization axioms. Moreover, it enables the formulation of non-logical axioms about complex expressions. The proposed inference system is illustrated by examples of using the system for deriving inferences in natural language.