While working with proof trees and proof searching techniques, it is always important to know specific properties about the calculus with which you are working. With better knowledge of the structure of the calculus you can exploit certain properties. This can lead to, among others, smaller proofs, less backtracking in proof searching and better understanding of why a proof does not exist.
During our semester we have shown many things about the LK and LJ calculi, however we have not discussed in detail the problems of permutability and decidability. During my lecture I will be discussing these two topics as well as proof search.
I will stay closely focused on the intuitionistic calculus since this is the more `problematic' of the two. The LJ calculus I discuss will closely model that of what we are used to, however I will also be examining slight variations. I will also briefly touch on how these topics relate to classical logic.
The sources I will be using as the bases of my discussion are as follows: