A forward chaining theorem prover for the extended Lambek calculus

Abstract

Natural Language Processing is one of the main branches of Arti?cial Intelligence, in which Lambek calculus is used to make deductive proofs about properties of language structures, which are presented as symbols. It can be done automatically with the implementation of an algorithm. This thesis constructs such an algorithm and presents a usable Python program that follows this algorithm to form proofs with the deductive rules of Lambek calculus. The construction of the algorithm was based on an extended form of Lambek calculus, in which the range of provable theorems more closely represents natural language than the system without any extensions. Forward chaining was used, so the tree structure of a linguistic input is formed automatically as well. It is not yet veri?ed whether this algorithm can form every possible proof, so a formal analysis and proof concerning this is recommended as further research.