A forward chaining theorem prover for the extended Lambek calculus
Summary
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.