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:
The views and opinions expressed in this page are strictly those of the page author.
The contents of this page have not been reviewed or approved by the University of Minnesota.