Typelogical Proof Nets in Python - Graphical Lambek-Grishin Calculus

Abstract

The aim of this thesis is to investigate a graphical method for Lambek-Grishin calculus. Graphical calculus is a good alternative to sequent calculus and natural deduction for use in automated deduction. The first part of the thesis presents the graphical calculus, reiterating previous work on the subject. After this introduction the methods' relation to sequent calculus is explained, in the form of proof terms. All this is implemented as a theorem prover in Python, which can be found in the appendix.