The calculus DNL results from the non-associative Lambek calculus NL by splitting the product functor into the right (⊳) and left (⊲) product interacting respectively with the right (/) and left (\) residuation. Unlike NL, sequent antecedents in the Gentzen-style axiomatics of DNL are not phrase structures (i.e., bracketed strings) but functor-argument structures. DNL− is a weaker variant of DNL restricted to fa-structures of order ≤¬ 1. When axiomatized by means of introduction/elimination rules for / and \, it shows a perfect analogy to NL which DNL lacks.
JavaScript is turned off in your web browser. Turn it on to take full advantage of this site, then refresh the page.