A `natural logic' inference system using the Lambek calculus (Q851198)
From MaRDI portal
scientific article
Language | Label | Description | Also known as |
---|---|---|---|
English | A `natural logic' inference system using the Lambek calculus |
scientific article |
Statements
A `natural logic' inference system using the Lambek calculus (English)
0 references
17 November 2006
0 references
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.
0 references
natural logic
0 references
Lambek calculus
0 references
normalization
0 references
inference system for natural language
0 references
Curry-Howard correspondence
0 references